[566] % z3release small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 213
UNEXPECTED CODE WAS REACHED.
Z3 4.8.11.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[567] %
[567] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/util/parray.h
Line: 335
i < size(r)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[568] %
[568] % cat small.smt2
(declare-const a Real)
(declare-const b Bool)
(declare-const c Bool)
(assert (= 0 1))
(assert (or (not b) (not c) (= a 4.0)))
(assert (or b (not c) (= a 1.0)))
(assert (or (not b) c (= a 3.0)))
(assert (or b c (= a 0.0)))
(apply recover-01)
[569] %