Hi Z3 team,
On a small anonymized BV QE repro (~3.3KB, 73 lines), Z3 (4.8.17) with apply qe does not produce a usable result within 60 seconds. But when using other SMT solver, it can be solving immediately.
Environment
- Z3:
Z3 version 4.8.17 - 64 bit
- OS: Linux (x86_64)
Repro SMT2
Formula shape:
- 6 free
(_ BitVec 1) vars
- 14 existential BV vars (1/9/48 bits)
- QE request:
(assert (exists ...)) + (apply qe)
(set-logic BV)
; control variables (to keep after QE)
(declare-const cv0 (_ BitVec 1))
(declare-const cv1 (_ BitVec 1))
(declare-const cv2 (_ BitVec 1))
(declare-const ap0 (_ BitVec 1))
(declare-const ap1 (_ BitVec 1))
(declare-const ap2 (_ BitVec 1))
; eliminate data variables
(assert (exists (
(d0 (_ BitVec 1))
(d1 (_ BitVec 48))
(d2 (_ BitVec 1))
(d3 (_ BitVec 48))
(d4 (_ BitVec 1))
(d5 (_ BitVec 1))
(d6 (_ BitVec 48))
(d7 (_ BitVec 1))
(d8 (_ BitVec 1))
(d9 (_ BitVec 48))
(d10 (_ BitVec 1))
(d11 (_ BitVec 1))
(d12 (_ BitVec 9))
(d13 (_ BitVec 9))
)
(and
(and
(and
(and
(and
(and
(and
(and
(= d4 (_ bv0 1))
(= d10 (_ bv0 1))
(= d5 (_ bv0 1))
(= d7 (_ bv0 1))
(= d8 (_ bv1 1))
(= d11 (_ bv1 1))
(= d3 d9)
(= d2 (_ bv0 1))
(= d1 d6)
(= d0 (_ bv0 1)))
(not (= d13 (_ bv511 9)))
(= d12 d13))
(not (= d9 (_ bv1 48)))
(= ap0 (_ bv1 1)))
(not (and
(= d9 (_ bv1 48))
(= (_ bv1 1) d4)))
(= ap1 (_ bv0 1))
(=>
(= d9 (_ bv1 48))
(not (= (_ bv1 1) d4)))
(= ap2 (_ bv1 1))
(= cv0 (_ bv1 1)))
(not (and
(= d3 (_ bv1 48))
(= cv1 (_ bv1 1)))))
(not (and
(= d3 (_ bv1 48))
(not (= cv1 (_ bv1 1))))))
(not (and
(= d3 (_ bv1 48))
(= cv2 (_ bv1 1)))))
(not (and
(= d3 (_ bv1 48))
(not (= cv2 (_ bv1 1))))))
))
(apply qe)
(exit)Commands
Z3:
z3 -smt2 -in < repro.smt2
Observed:
- No correct/usable QE output within 60s timeout.
Question:
- Is this expected for BV QE in Z3 4.8.17, or am I missing recommended QE tactic/parameters for this formula class?
Hi Z3 team,
On a small anonymized BV QE repro (
~3.3KB, 73 lines), Z3 (4.8.17) withapply qedoes not produce a usable result within 60 seconds. But when using other SMT solver, it can be solving immediately.Environment
Z3 version 4.8.17 - 64 bitRepro SMT2
Formula shape:
(_ BitVec 1)vars(assert (exists ...))+(apply qe)Commands
Z3:
z3 -smt2 -in < repro.smt2Observed:
Question: