Incorrect Behavior for tactic solver for timeout

Question

I am trying to use tactic solver in Z3, to solver a problem of some X constraints as opposed to general purpose solver.

I am using the following tactics -

simplify purify-arith elim-term-ite reduce-args propagate-values solve-eqs symmetry-reduce smt sat sat-preprocess

I apply the tactics one after another to the problem by using Z3_tactic_and_then API. Also I am using this technique in order to configure the time-out for the solver.

Now, for the same problem if I use a general solver, it times out for the query for the specified time-out. However, if I use the mentioned tactics for the solver, then it does not time-out in the given time. It runs much longer.

For example, I specified a timeout of 180*1000 milliseconds, but it timed out in 730900 milliseconds. I tried to remove a few tactics mentioned above, but the behaviour was still the same.

Z3 version 4.1

Answer 1

Unfortunately, not every tactic respects the timeout. The tactic smt is a big "offender". This tactic wraps a very old solver implemented in Z3. Unfortunately, this solver cannot be interrupted during some expensive computations because it would leave the system in a corrupted state. That is, Z3 would crash in future operations. When this solver was implemented, a very simplistic design was used. If we want to interrupt the process: kill it. Of course, this is not acceptable when using Z3 embedded in bigger applications. New code is usually much more responsive to timeouts, and we try to avoid this kind of poor design.