(qe) unsoundness

[muchang]

Hi, For this case, Z3 gives an incorrect answer:

[1152] % z3-4.8.5 small.smt2
unsat
sat
[1153] % z3-4.8.6 small.smt2
unsat
sat
[1154] % z3-4.8.7 small.smt2
unsat
sat
[1155] % z3 small.smt2
unsat
sat
[1156] % cat small.smt2
(declare-fun a () Real)
(assert (forall ((b Real)) (= (= a b) (= b 0))))
(check-sat-using qe)
(check-sat)
[1157] %

OS: Ubuntu 18.04 Commit: 5b6255e

[merlinsun]

https://github.com/Z3Prover/z3/commit/2c8df54b70f5456efd0b2c3f4917d2b314098f19

$ z3 small.smt2
unsat
sat
$ cat small.smt2
(declare-fun a () (Array (_ BitVec 1) (_ BitVec 1)))
(assert (distinct false (exists ((r (Array (_ BitVec 1) (_ BitVec 1)))) (= a (store (store (store r (_ bv0 1) (_ bv0 1)) (_ bv1 1) (_ bv0 1)) (_ bv0 1) (_ bv1 1))))))
(check-sat-using (then qe smt))