1 2 3 4 5 6 7 8 9 10 11 12 13 14
; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs ; EXPECT: unsat (set-logic QF_LRA) (declare-fun x () Real) (declare-fun y () Real) (declare-fun z () Real) ; Both strict and non-strict inequalities. (assert (< y 0)) (assert (>= y x)) (assert (>= y (- x))) (check-sat)