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

(set-logic LIA)

(synth-fun max2 ((x Int) (y Int)) Int
    ((Start Int ((Variable Int)
                 (Constant Int)
                 (+ Start Start)
                 (- Start Start)
                 (ite StartBool Start Start)))
     (StartBool Bool ((and StartBool StartBool)
                      (or  StartBool StartBool)
                      (not StartBool)
                      (<=  Start Start)
                      (=   Start Start)
                      (>=  Start Start)))))

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

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


(check-synth)