6 files changed, 171 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/cube-nia.sy b/test/regress/regress1/sygus/cube-nia.sy
new file mode 100644
index 000000000..da7d98e66
--- /dev/null
+++ b/test/regress/regress1/sygus/cube-nia.sy
@@ -0,0 +1,27 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic NIA)
+
+(synth-fun cube ((x Int)) Int
+  (
+    (Start Int (ntInt))
+  
+    (ntBool Bool
+      ( 
+        (> ntInt ntInt)
+        (= ntInt ntInt)
+      )
+    )
+    (ntInt Int
+      (1 x
+        (* ntInt ntInt)
+        (ite ntBool ntInt ntInt)
+      )
+    )
+  )
+)
+
+(constraint (= (cube 1) 1))
+(constraint (= (cube 2) 8))
+(check-synth)
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)
diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy
new file mode 100644
index 000000000..d1541fa87
--- /dev/null
+++ b/test/regress/regress1/sygus/extract.sy
@@ -0,0 +1,19 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic ALL_SUPPORTED)
+(declare-datatype Ex ((Ex2 (ex Int))))
+
+(synth-fun ident ((x1 Ex)) Int
+	(
+		(Start Int (ntInt))
+		(ntInt Int
+			(
+				(ex ntEx)
+ 			)
+		)
+		(ntEx Ex ( x1 ) )
+	)
+)
+(constraint (= (ident (Ex2 1)) 1))
+(check-synth)
diff --git a/test/regress/regress1/sygus/issue2914.sy b/test/regress/regress1/sygus/issue2914.sy
new file mode 100644
index 000000000..0f125a870
--- /dev/null
+++ b/test/regress/regress1/sygus/issue2914.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic SLIA)
+(declare-datatype JSIdentifier ((JSString (jsString String)) (Error )))
+
+(synth-fun substring ((x1 String) (x3 Int))String
+	((Start String (ntString))
+		(ntInt Int
+			(0 x3)
+		)
+		(ntJSIdentifier JSIdentifier
+			( 
+				Error
+			)
+		)
+		(ntString String
+			(x1
+				(str.substr ntString ntInt ntInt)
+				(jsString ntJSIdentifier)
+				(str.++ ntString ntString)
+			)
+		)
+	)
+)
+(constraint (= (substring "ey" 1) "e"))
+(check-synth)
diff --git a/test/regress/regress1/sygus/issue2935.sy b/test/regress/regress1/sygus/issue2935.sy
new file mode 100644
index 000000000..5616d19f5
--- /dev/null
+++ b/test/regress/regress1/sygus/issue2935.sy
@@ -0,0 +1,36 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic SLIA)
+(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String)) ))
+
+(synth-fun f ((x1_ JSIdentifier)(x2_ String)) JSIdentifier
+	((Start JSIdentifier (ntJSIdentifier))
+		(ntInt Int
+			(1
+				(+ ntInt ntInt)
+				(jsInt ntJSIdentifier)
+			)
+		)
+		(ntString String
+			(x2_
+				(str.substr ntString ntInt ntInt)
+				(jsString ntJSIdentifier)
+			)
+		)
+		(ntBool Bool
+			( 
+				(= ntString ntString)
+			)
+		)
+		(ntJSIdentifier JSIdentifier
+			( x1_  
+			(ite ntBool ntJSIdentifier ntJSIdentifier)
+			(JSString ntString)
+			)
+		)
+	)
+)
+(constraint (= (f (JSString "") "") (JSString "")))
+(constraint (= (f (JSString "M") "W") (JSString "M")))
+(constraint (= (f (JSString "Moon") "") (JSString "on")))
+(check-synth)
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)