; EXPECT: unsat ; COMMAND-LINE: --cegqi-si=all --no-dump-synth (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)