; EXPECT: unsat
; COMMAND-LINE: --cegqi-si --no-dump-synth

(set-logic LIA)

(synth-fun f ((x Int) (y Int)) Bool)

(declare-var x Int)
(declare-var y Int)

(constraint (= (f x y) (>= (+ x y) 500)))


(check-synth)