Why it is slower to get query result from z3 java API then get from z3 directly?

Question

Just noticed that for some benchmarks, it is really slow to get query result from z3 via java API. However, if I just dumped the query into smt2 format, and run z3 in the command line directly, it takes less than a second. Wonder why?

Answer 1

I noticed that your problem contains a (push) command, removing this changes the performance dramatically. When Z3 first sees a (push), it switches to a different solver that supports incrementality and that can have a dramatic impact on the performance. By setting the verbosity to 15 via -v:15, the first line of Z3s output tells you which solver it is using, e.g., when the push command is present it says

(combined-solver "using solver 2 (without a timeout)")

and when it is not, then it says

(combined-solver "using solver 1")

For the given example, solver 2 happens to be significantly faster.