1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/sygus-dt.sy b/test/regress/regress1/sygus/sygus-dt.sy
new file mode 100644
index 000000000..d496e3fdc
--- /dev/null
+++ b/test/regress/regress1/sygus/sygus-dt.sy
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(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)