1 2 3 4 5 6 7 8 9 10 11 12
; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --sygus-qe-preproc (set-logic LIA) (synth-fun f ((x Int)) Int) (declare-var x Int) (declare-var y Int) (constraint (=> (or (= y 2) (= y 3)) (> (f x) y))) (check-synth)