1 2 3 4 5 6 7 8 9 10
; EXPECT: unsat (set-logic ALL) (set-option :incremental false) (declare-fun x () Real) (declare-fun y () Real) (declare-fun f (Real) Real) (assert (=> (> x y) (> (f x) (f y)))) (assert (= x 3)) (assert (= y 2)) (check-sat-assuming ( (not (> (f x) (f y))) ))