I think the major issue I have with Z3 is that if your input constraints are large and non-decomposable, then the resulting output is functionally undebuggable. There's a bit of handwaving from Z3folk about using assert_and_track() along with pseudoboolean proxies. But, there's a lot of pitfalls using these techniques. Combining bitvectors and pseudobooleans (y'know — the common case) under implication can either weaken or strengthen the constraints which literally changes the behavior of the given constraint problem. That means that any attempt to add tracing to the problem to debug your constraints can lead Z3 to change its behavior (because the underlying problem is different).
I really like Z3, and I like the convenience of Z3, but ... dang ... it'd be nice if you could trace internal statements.
Oh! Another pet-peeve is that there's no (sane) way to print large expressions. Once an expression gets large, Z3 begins dumping opaque internal variables (K!##). There is no way to get Z3 to unmunge these variables — that information is forever lost to you.
Interestingly, Knuth swapped dancing links for dancing cells and implemented a bunch of SAT solvers (and counting solutions to polyomino tiling problems) using zero suppressed binary decision diagrams. So algorithms X has newer and more efficient successors.
I really like Z3, and I like the convenience of Z3, but ... dang ... it'd be nice if you could trace internal statements.
Oh! Another pet-peeve is that there's no (sane) way to print large expressions. Once an expression gets large, Z3 begins dumping opaque internal variables (K!##). There is no way to get Z3 to unmunge these variables — that information is forever lost to you.