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

(set-logic LIA)

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

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

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


(check-synth)