; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)

;; f1 is x plus 2 ;; f2 is 2x plus 5

(define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))

(synth-fun f1 ((x Int)) Int
     ((Start Int) (Intx Int) (CInt Int))
     (
     (Start Int (
            (let0 Intx CInt CInt)
            )
     )
     (Intx Int (x))
     (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) (Intx Int) (CInt Int))
     (
     (Start Int (x
            (let0 Intx Start CInt)
            )
     )
     (Intx Int (x))
     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
     )
)


(declare-var x Int)

(constraint (= (+ (f1 x) (f2 x)) (+ (+ x x) (+ x 8))))
(constraint (= (- (f2 x) (f1 x)) (+ x 2)))

(check-synth)