1 files changed, 37 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy
new file mode 100644
index 000000000..261666dd4
--- /dev/null
+++ b/test/regress/regress1/sygus/tester.sy
@@ -0,0 +1,37 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic SLIA)
+(declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool))))
+
+(define-fun isA ((i DT)) Bool ((_ is A) i) )
+(define-fun isB ((i DT)) Bool ((_ is B) i) )
+
+(synth-fun add ((x1 DT)) DT
+	(
+		(Start DT (ntDT))
+		(ntDT DT
+			( x1 x2
+				(JSBool ntBool)
+				(A ntInt)
+				(ite ntBool ntDT ntDT)
+			)
+		)
+		(ntBool Bool
+			(
+				(isA ntDT)
+				(isB ntDT)
+				(jsBool ntDT)
+			)
+		)
+		(ntInt Int
+			(1
+				(a ntDT)
+				(+ ntInt ntInt)
+			)
+		)
+	)
+)
+(constraint (= (add (A 6)) (A 7)))
+(constraint (= (add (B "j")) (B "j")))
+(check-synth)