(rewriter.elim_and, model_evaluator.array_equalities) Assertion violation at ../src/qe/qe.cpp Line: 710

[muchang]

[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] % 

Commit: 8abb644

[NikolajBjorner]

Though, I pushed a fix for this it is borderline won't fix given that this could be deemed parameter abuse.