[fooker]

I know, my PhD was about verifying software correctness with SMT solvers.

The reason we don't do this in production is that the solvers take an unpredictable amount of time. A small problem can take forever and a large problem can be instant. You can't gave that in a compiler.

There are enough people at Apple who know about SAT solvers. :)

[agent281]

On the other hand, they might know about SAT solvers, but not have enough time to actually experiment with it and integrate one into the language. Especially if there are other high priority issues.