; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --decision=justification

(set-logic LIA)

(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
(define-fun g ((x Int)) List (cons (+ x 1) nil))
(define-fun i () List (cons 3 nil))

(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) (nil) (tail Start)))
                             (StartInt Int (x 0 1 (+ StartInt StartInt)))))

(declare-var x Int)

(constraint (= (f x) (cons x nil)))
(check-synth)