[igornotarobot]

> Of course decidability is desirable, but efficient sound procedures in the undecidable case would still solve many practical problems. I realize they are not as "nice" from a theoretical/academic standpoint, though.

This is interesting, because undecidability of SMT theories is a very practical issue. Actually, many people in academia have this point of view that solving many practical problems is useful. It helps us to drive research progress, but it is a completely useless metric for industry. What is better: (1) a tool that wins a competition by solving X out of Y benchmarks, (2) or a tool that solves your problem? In academia, (1) is a clear winner, as it gives you a free way to publish a paper, modulo peer review. In industry, you don't care about (1), because you have exactly 1 (one!) benchmark that is important for you, that is, case (2).

Imagine a compiler that works on 85% of syntactically-correct (and well-typed) programs, and you never know when it would hang on your code. This is exactly the behavior of SMT solvers when you start using quantifiers. By knowing the internals of SMT and its techniques, you can quite often work around these problems. However, TLA+ users do not want to know the guts of SMT; why would they? This is why Apalache implements a quantifier-free encoding. Sometimes, it hits us badly, but it is somewhat more predictable. Ivy does it differently, by providing the user with a language that is actually quite close to the theories implemented in z3. While it gives the user a finer control over the SMT constraints, the user has to understand first-order logic much better than in case of Apalache.