z3 hangs on query involving maps and bitvectors

[ranjitjhala]

Hi z3 team -- my student @vrindisbacher came across the following two SMTLIB queries that seem to finish instantaneously with cvc5 but seem to make z3 hang indefinitely. I will ask John Regehr's help with using c-reduce to minimize the tests -- but maybe you have some idea?

There are two files.

The first test z3-slow-1.smt2.txt should work just by pure equality/congruence.

There is a lot of junk in it but we're just checking a VC of the form. (a = b) => (a = b)

(assert (= a b))
(assert (not (= a b)))
(check-sat)

except that that the a and b are blown out into gigantic terms involving map-set
and bitvector operations, with some additional booleans recording the equality...

The second is not so trivial, but both seem to finish swiftly with CVC5.

Any ideas on what might be happening?

z3-slow-1.smt2.txt
z3-slow-2.smt2.txt

[NikolajBjorner]

These should use relevancy=0. It helps for second case. The first is solved by sat.smt=true, which is a different solver.
Digging into why it diverges with the legacy solver is TBD.

[benjaminfjones]

Doing solver comparison for the first case, I found that the sat.smt=true option causes z3 (4.13.3) to return quickly on every subproblem, but z3 reports each one is SAT.

cvc5 (1.2.0) reports every problem is UNSAT.

Based on Ranjit's description, it seems UNSAT is the expected result.

[NikolajBjorner]

This is what I get:

C:\z3\release>z3 z3-slow-2.smt2.txt sat.smt=true
unsat
unsat
unsat
unsat

C:\z3\release>z3 z3-slow-1.smt2.txt sat.smt=true
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat

what benchmarks are you using?

[NikolajBjorner]

Does this declaration

(define-fun b$36$$35$$35$35 () Bool (= ((as mktuple8 (Tuple8 (Array Int (_ BitVec 32)) (Tuple2 (_ BitVec 32) (_ BitVec 32)) (Tuple2 Bool Bool) (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (Array (_ BitVec 32) (_ BitVec 32)) Int)) a0 ((as mktuple2 (Tuple2 (_ BitVec 32) (_ BitVec 32))) a1 a2) ((as mktuple2 (Tuple2 Bool Bool)) a3 a4) a5 a6 a7 a8 a9) ((as mktuple8 (Tuple8 (Array Int (_ BitVec 32)) (Tuple2 (_ BitVec 32) (_ BitVec 32)) (Tuple2 Bool Bool) (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (Array (_ BitVec 32) (_ BitVec 32)) Int)) (tuple8$36$0 reftgen$36$cpu$36$1) (ite (or (= (tuple8$36$7 reftgen$36$cpu$36$1) 0) (not (tuple2$36$1 (tuple8$36$2 reftgen$36$cpu$36$1)))) ((as mktuple2 (Tuple2 (_ BitVec 32) (_ BitVec 32))) (bvsub (ite (or (= (tuple8$36$7 reft

mean that you are effectively introducing a definition of a tuple type?

There appears to be two alternate definitions depending on scopes.
If you introduced the definitions as define-fun within the scopes they would automatically expand.
The simplifier, should just reduce the goals to "false", which is what happens in the new solver. The legacy solver doesn't eliminate a1, ..a9, however, as it doesn't have the incremental equality solver pre-processor.
But if you are using these a1..a9 as definitions in the first place (you can just introduce a single variable and then use accessors if you want), there would be fewer ways for pre-processing to miss out.

[benjaminfjones]

@NikolajBjorner In my comment above I was testing both benchmarks that Ranjit attached. This is z3 4.13.3 on Linux:

❯ uname -a
Linux hostname 5.10.230-202.885.amzn2int.x86_64 #1 SMP Tue Dec 3 16:44:20 UTC 2024 x86_64 x86_64 x86_64 GNU/Linux

❯ z3 --version
Z3 version 4.13.3 - 64 bit

❯ z3 z3-slow-1.smt2 sat.smt=true
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat

❯ z3 z3-slow-2.smt2 sat.smt=true
sat
sat
sat
sat

On macOS arm64, I was able to test both 4.13.3 and 4.13.4. Z3 reports different results for both of Ranjit's benchmarks on these two versions:

❯ ~/src/z3_versions/z3-4.13.3-arm64-osx-13.7/bin/z3 z3-slow-1.smt2 sat.smt=true

sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat

❯ ~/src/z3_versions/z3-4.13.3-arm64-osx-13.7/bin/z3 z3-slow-2.smt2 sat.smt=true

sat
sat
sat
sat

❯ ~/src/z3_versions/z3-4.13.4-arm64-osx-13.7.1/bin/z3 z3-slow-1.smt2 sat.smt=true
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat
unsat

❯ ~/src/z3_versions/z3-4.13.4-arm64-osx-13.7.1/bin/z3 z3-slow-2.smt2 sat.smt=true
unsat
unsat
unsat
unsat

[NikolajBjorner]

Yes, bugs were fixed for 13.4. The tactic for removing unconstrained sub-terms was buggy.
Generally, sat.smt=true isn't mainstream ready. In this case it was solved by pre-processing.

[vrindisbacher]

Does this declaration

(define-fun b$36$$35$$35$35 () Bool (= ((as mktuple8 (Tuple8 (Array Int (_ BitVec 32)) (Tuple2 (_ BitVec 32) (_ BitVec 32)) (Tuple2 Bool Bool) (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (Array (_ BitVec 32) (_ BitVec 32)) Int)) a0 ((as mktuple2 (Tuple2 (_ BitVec 32) (_ BitVec 32))) a1 a2) ((as mktuple2 (Tuple2 Bool Bool)) a3 a4) a5 a6 a7 a8 a9) ((as mktuple8 (Tuple8 (Array Int (_ BitVec 32)) (Tuple2 (_ BitVec 32) (_ BitVec 32)) (Tuple2 Bool Bool) (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (Array (_ BitVec 32) (_ BitVec 32)) Int)) (tuple8$36$0 reftgen$36$cpu$36$1) (ite (or (= (tuple8$36$7 reftgen$36$cpu$36$1) 0) (not (tuple2$36$1 (tuple8$36$2 reftgen$36$cpu$36$1)))) ((as mktuple2 (Tuple2 (_ BitVec 32) (_ BitVec 32))) (bvsub (ite (or (= (tuple8$36$7 reft

mean that you are effectively introducing a definition of a tuple type?

There appears to be two alternate definitions depending on scopes. If you introduced the definitions as define-fun within the scopes they would automatically expand. The simplifier, should just reduce the goals to "false", which is what happens in the new solver. The legacy solver doesn't eliminate a1, ..a9, however, as it doesn't have the incremental equality solver pre-processor. But if you are using these a1..a9 as definitions in the first place (you can just introduce a single variable and then use accessors if you want), there would be fewer ways for pre-processing to miss out.

I went ahead and introduced a single tuple variable rather than building one from a1..a9 and it does seem to make a huge difference (solved almost instantly). Thanks for that tip!

For the other one, sat.smt = true seems to be the trick (as you said). I was reading this documentation and it seems like when z3 is used in incremental mode it doesn't do any pre-processing of formulas. Is that correct?

If so, I'm assuming the patch is to use sat.smt = true when using incremental solving (once it's mainstream ready)? Is there any down side to it?

[NikolajBjorner]

Is there any down side to it?

It uses an entirely different backend solver. It is not generally tuned as the legacy solver and I often find performance gaps.