`apply qe` on a small BV formula does not produce output within 60s

[jwimd]

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?