1 2 3 4 5 6 7 8 9 10 11 12 13 14
; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none (set-logic LRA) (synth-fun f ((x Real)) Real) (declare-var x Real) (constraint (and (< 0 (f x)) (< (f x) 1))) (check-synth) ; any number between 0 and 1 is a solution, e.g. (f x) = (/ 1 (+ 1 1))