1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy
new file mode 100755
index 000000000..e842477e8
--- /dev/null
+++ b/test/regress/regress0/sygus/sygus-dt.sy
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-dump-synth
+
+(set-logic LIA)
+
+(declare-datatypes () ((List (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)
+\ No newline at end of file