OxO4

That actually depends on the logic being used. Some of the logics supported by Z3 are not even decidable. In fact, even solving quantifier-free bit-vector formulas is NEXPTIME-complete [0] when using a binary encoding.

[0] http://smt2012.loria.fr/paper7.pdf

Out of curiosity, what made you choose Z3 over other SMT solvers? Also, if you have benchmarks that you can publish, it would be really great if you could submit them to SMT-LIB/SMT-COMP [0] such that they can be used to improve SMT solvers.

[0] https://smt-comp.github.io/news/2019-01-24.html

I agree that there may be edge cases where it doesn't make sense to make software open source (although I also think that the majority of software used at IRS, NSA, CIA, and FBI could be open source). However, I strongly believe that if the code is not published, it should at least be available to the government itself, s.t. if a vendor goes out of business or the government wants to change vendors they can do so without issues.

All of those companies are problematic to a certain degree. Personally, whether I'd have an issue with working for one of those companies also depends on what I am working on. Let's say that one of those companies pays you to work on an open source project. Would that really be that bad ethically? What if you worked on Facebook's security team securing the users' data? Is that really worse than working for LinkedIn implementing some new dark pattern to get the users to receive more email spam? At the end of the day, you'll have to make compromises, unfortunately.

> the keys leave imprints on the monitor after the lid has been closed

Same with my Late 2013 MacBook Pro.

> the keyboard with it's rickety keys

I haven't used the XPS keyboards extensively but they seem to get good reviews and in my limited experience, I definitely prefer them to the new MacBook keyboards (which I've used quite a bit).

> I eat tramadol just to handle the back-pain from carrying it around in my rucksack

The XPS 13 is actually lighter than the MacBook Pro 13 and the new MacBook Air. The XPS 15 is half a pound heavier than the MacBook Pro 15, which should be barely noticeable when carried in a backpack. I am not quite following.

AFAIK newer Macs with a T2 security chip block OSs other than macOS and Windows 10 [0] (at least on the internal drive).

[0] https://www.phoronix.com/scan.php?page=news_item&px=Apple-T2...

Note that this option may have some limitations depending on the country: Turkey blocks the IMEI of unregistered devices after 120 days, so if you plan to travel there multiple times, you may be out of luck (AFAIK only residents can register their device). So it is definitely worth checking the rules before traveling to a country.

Presumably, this could all be done without extending the footprint of the rails already present just by increasing the number of trains, cars per train, speed of the trains, or improving the design of the cars. Really, the beauty of public transportation is that you can get much higher density (and speed) than individual transportation if done correctly.

Fun fact: European driver-side mirrors actually have a larger FOV than their US counterparts. It took me a while to get used to that when I moved to the US. I ended up buying some small blind spot mirrors that can be stuck onto the car's mirrors. I've been pretty happy with that solution (in combination with looking over my shoulder).

Actually, the Dell XPS 15 has a 15" screen and a tenkeyless keyboard as well.

I can confirm that this worked for me. Thanks a lot!

So because of one example, you are attributing criminal behavior to a whole group of people? Sounds like textbook racism to me.

50 million people? Germany has a total population of 80 million, so something is definitely off with your numbers. What kind of "social issues" have immigrants caused in Sweden?

Nit: They are not making people disappear but they send them back in time. But I also had to immediately think of them when I saw the title.

Yes, pumped-storage hydroelectricity is used extensively [0].

[0] https://en.wikipedia.org/wiki/Pumped-storage_hydroelectricit...

That is a very American perspective. American companies are not trustworthy either given what NSA and other American institutions have been doing. As a customer, you just get to choose your butcher but nothing more. The only solution in the long run is to design open hardware and use open software.

If you google for the paper, then a direct link to the full paper comes up, which works for me: http://ceepr.mit.edu/files/papers/2018-005.pdf

This reminds me of: "Kill one man, and you are a murderer. Kill millions of men, and you are a conqueror. Kill them all, and you are a god." - Jean Rostand

Minor comment: Stanford is $16,329 _per quarter_, not semester.

Why not take a class about compilers and implement something like that as a class project?

Not at all. If you do basic coordination of who is editing which section when, merge conflicts are exceedingly rare. I've collaborated on multiple 10-ish page documents (research papers) with 3+ people using LaTeX+git and it has worked just fine.

The one in the video (IST) is actually very nice, there is lots of space (especially compared to the rest of the airport, which is usually very crowded), free food and drinks (including alcohol and decent, non-drip coffee).

LastPass currently does not support U2F officially [0]. How are you using U2F with LastPass?

[0] https://lastpass.com/support.php?cmd=showfaq&id=8126

How about:

https://en.wikipedia.org/wiki/Dnepropetrovsk_maniacs

https://en.wikipedia.org/wiki/Armin_Meiwes

It would be even better if there was a way to pay $2.50 that get distributed among the creators of the consumed content.

As a European, I've never seen high speed trains that require metal detectors and/or luggage inspection. Which country was that?

Obama did not do the same thing [1].

[1] https://www.washingtonpost.com/news/fact-checker/wp/2017/01/...

As a current Apple user with similar needs, I've been looking into alternatives myself. The Lenovo ThinkPad P50 [1] is looking great. Can be configured with a Xeon quad-core CPU, up to 64GB of ECC (!) RAM, 2 x 1TB PCIe-NVMe SSD and an NVIDIA Quadro M2000M (performance similar to a GTX 960M or 950M [2]). I've been considering to get a Xeon/64GB non-ECC RAM/512GB PCIe-NVMe SSD/Quadro M2000M configuration myself for around $2,600 (before taxes), which is much cheaper than Apple's offerings.

The Dell Inspiron 7510 can be specced similarly [3] and looks also interesting but apparently throttles the GPU under load [4], which is a huge no-go for me (I had a laptop that throttled under load at some point and it was a pain).

[1] http://shop.lenovo.com/us/en/laptops/thinkpad/p-series/p50/

[2] http://www.notebookcheck.net/NVIDIA-Quadro-M2000M.151581.0.h...

[3] http://www.dell.com/us/business/p/precision-m7510-workstatio...

[4] http://www.notebookcheck.net/Dell-Precision-7510-4K-IGZO-Mob...

Or the Adventure Time episode "Scamps" [0].

[0] http://adventuretime.wikia.com/wiki/Scamps

Whenever I compared prices, SkyScanner hasn't been cheaper than Google Flights for me (domestic flights in the US and flights to Europe) and their website is much, much slower than Google Flights. Do you remember what kind of flights were cheaper?