[553] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/qe/qe.cpp
Line: 710
!m.is_not(f) && !m.is_and(f) && !m.is_or(f)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[554] % cat small.smt2
(set-option :rewriter.elim_and true)
(set-option :model_evaluator.array_equalities false)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (exists ((c Real)) (<= c b a)))
(check-sat)
[555] %