(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(assert (not (exists ((g Real))
(= (and (< 0.0 b)) (= (= 0.0 a) (not (= (<= g a) (<= e d)))))))
)
(assert (not (= (<= 0.0 c) (or (< (* c f) (/ 0 0))))))
(check-sat)
z3 returns unknown for this formula which is unsatisfiable. Z3 seems to need quite some memory for this formula. Solving it ~100 times in a row occasionally results in an out of memory error or a segfault.
OS: Ubuntu 19.04
Revision: 60c504f
z3 returns
unknownfor this formula which is unsatisfiable. Z3 seems to need quite some memory for this formula. Solving it ~100 times in a row occasionally results in an out of memory error or a segfault.OS: Ubuntu 19.04
Revision: 60c504f