qe z3str3 incorrect answer on BV formula

[muchang]

Hi,
For this formula:

(assert (forall ((a (_ BitVec 2)))
  (exists ((b (_ BitVec 2))) (and (= a #b00) (distinct a b)))))
(check-sat-using qe)

Z3 smt.string_solver=z3str3 incorrectly gives sat, while this formula should be unsat.

OS: Ubuntu 18.04
Commit: 006caea

[mtrberzi]

@NikolajBjorner would appreciate your insight with this one. This doesn't look like it should be a z3str3 bug because there are no string terms. But running with smt.string_solver=seq produces unsat. So I'm not sure what here should be going to the string solver.

[NikolajBjorner]

It is most likely duplicate of another qe reported bug that uses strings (that I closed)
The behavior of z3str3 is unique in the way it manages priority queues and possibly also assumptions. I would look into assumption management first, but overall I don't consider these bugs important because QE is not something that one can reasonably expect for strings without any serious work on QE methods for monoids. It is basically identifying some anomaly by sweeping over exposed option combinations. There are certainly useful bugs uncovered this way, but you would do well by tempering it with focus on bugs/features that really matter to use scenarios.

[NikolajBjorner]

Note, that I have not marked this as z3str3, nor assigned it to you.

[sdingcn]

Hi,

The following one might be a duplicate case of the above one.

The following formula should be unsat, but Z3 with smt.string_solver=auto gives sat. This could at least be reproduced on this commit: 7fe8298.

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (not (exists ((d Real)) (=> (not (<= 0 d b)) (>= c 1) (<= c 0) (<= 0 a)))))
(check-sat-using (then qe smt))