1 2 3 4 5 6
; COMMAND-LINE: --solve-real-as-int ; EXPECT: sat (set-logic ALL) (set-info :status sat) (assert (forall ((x Real) (y Real)) (=> (< x y) (exists ((z Real)) (and (< x z) (< z (+ y 2)))))) ) (check-sat)