1 files changed, 26 insertions, 0 deletions
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)