ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp Line: 404

Z3Prover / z3

The Z3 Theorem Prover

Other

9.96k stars 1.46k forks source link

ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp Line: 404 #7259

Closed merlinsun closed 2 weeks ago

merlinsun commented 2 weeks ago

Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/bf3615d4fbc017f0da036ac2fe3a3dce09922cd9 debug build

$ cat small.smt2 
(declare-fun v () (Array Bool Bool))
(assert (forall ((a Int) (va (Array Bool Bool))) (or (= a 0) (va (= v va)))))
(check-sat-using qsat)
$ z3 small.smt2 
ASSERTION VIOLATION
File: ../src/qe/qe_mbp.cpp
Line: 404
Failed to verify: !model.is_false(f)

NikolajBjorner commented 2 weeks ago

this has to be a duplicate of another similar bug for qe_qel and finite domain arrays.