1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/double.sy b/test/regress/regress1/sygus/double.sy
new file mode 100644
index 000000000..f3fea3122
--- /dev/null
+++ b/test/regress/regress1/sygus/double.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic SLIA)
+(declare-datatype Ex ((Ex2 (ex Int))))
+
+(synth-fun double ((x1 Ex)) Int
+	(
+		(Start Int (ntInt))
+		(ntInt Int
+			(
+				(ex ntEx)
+				(+ ntInt ntInt)
+			)
+		)
+		(ntEx Ex
+			( 
+				x1
+				(Ex2 ntInt)
+			)
+		)
+	)
+)
+(constraint (= (double (Ex2 1)) 2))
+(constraint (= (double (Ex2 4)) 8))
+(check-synth)