Issue with tactic

[merlinsun]

Hi,
For this instance, z3 b0605a9 gives unsat with (check-sat-using qe).

$ z3 small.smt2
unsat
sat
$ cat small.smt2
(declare-fun a () Bool)
(declare-fun v () String)
(assert (forall ((v Int)) (exists ((V Bool)) (or a (= a (= 0 v))))))
(assert (forall ((a Int)) (= 0 (str.indexof v v))))
(check-sat-using qe)
(check-sat)

[merlinsun]

Another instance with smt.bv.eq_axioms:

$ cat small.smt2
(declare-const x Bool)
(set-option :smt.bv.eq_axioms false)
(declare-fun a () String)
(declare-fun va () Int)
(assert (forall ((V Int)) (= a (str.++ a))))
(assert (forall ((v Int)) (or x (= va v))))
(check-sat-using qe)
(check-sat)
$ z3 small.smt2
unsat
sat

[NikolajBjorner]

This is a duplicate of an old bug on qe