; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic LIA)
(define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
(synth-fun f1 ((x Int)) Int
     (
     (Start Int (
            (letf x CInt CInt)
            )
     )
     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))

     )
)
(synth-fun f2 ((x Int)) Int
     (
     (Start Int (x
            (letf x Start CInt)
            )
     )
     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))

     )
)
(declare-var x1 Int)
(declare-var x2 Int)
(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8))))
(check-synth)