Hi,
on the following formula, z3 throws an assertion violation:
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (< 0 b a c))
(minimize a)
(minimize b)
(minimize c)
ASSERTION VIOLATION
File: ../src/opt/opt_context.cpp
Line: 1667
r1 == r2
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Revision: cdf3c48
Hi,
on the following formula, z3 throws an assertion violation:
OS: Ubuntu 18.04
Revision: cdf3c48