Intermediate check-sat impacts badly subsequent check-sat

[daniel-larraz]

Consider these two SMTLIB scripts: test1.txt, test2.txt

test1.txt contains only one check-sat command at the bottom of the file. Despite the size of the problem, z3 (4.11.2) can solve the query immediately.

test2.txt is a copy of test1.txt that additionally contains the following commands in lines 66-72:

(push 1)

(assert (not N.res.glocal_1@1))

(check-sat)

(pop 1)

When I run z3 on test2.txt, z3 solves the first check-sat query immediately, but then, z3 gets stuck solving the check-sat query at the bottom of the file.

I tried to run cvc5, Yices 2, and MathSAT on these two files, and all of them solved test2.txt in the same amount of time that took them to solve test1.txt, which was my expectation.

Could you please check if there is any issue with z3? Is there an explanation for this behavior?

Thank you, Daniel

[daniel-larraz]

It seems that just including (push 1) is enough to trigger the undesired behavior. The assert, check-sat, and pop commands are not required. I originally found this problem using a check-sat-assuming command without push/pop, so it is hard to pinpoint exactly the issue.

[NikolajBjorner]

A lot of useful pre-processing gets disabled in incremental mode. Pre-processing in this case solves a lot of your equalities and produces a trivial problem. You can use tactics to retain benefits of non-incremental solving

(check-sat-using (and-then simplify solve-eqs elim-uncnstr simplify smt))

[daniel-larraz]

@NikolajBjorner , thank you so much for the explanation!

[NikolajBjorner]

Systematic incremental pre-processing happens to be on a current agenda. It is in preliminary form. It can be enabled for the curious/brave/foolish: z3 test2.txt -v:10 sat.smt=true -st