ASSERTION VIOLATION, File: ../src/qe/qsat.cpp, Line: 580

[merlinsun]

Hi,
For this instance, z3 14312ef debug build

$ cat small.smt2 
(declare-fun a () Bool)
(assert (forall ((e Int)) (or a (= 1 e) (= e 0))))
(check-sat)
(check-sat)
$ z3 small.smt2 
sat
Asserting this expression twice in a row:
 a
ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 580
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a