1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/strings-double-rec.sy b/test/regress/regress1/sygus/strings-double-rec.sy
new file mode 100644
index 000000000..ea9caadea
--- /dev/null
+++ b/test/regress/regress1/sygus/strings-double-rec.sy
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic SLIA)
+ 
+(synth-fun f ((name String)) String
+    ((Start String (name "A" "B" "" (str.++ Start1 Start2)))
+     (Start1 String (name "A" "B" ""))
+     (Start2 String (name "B" "A" (str.++ Start2 Start)))
+))
+
+
+(declare-var name String)
+ 
+(constraint (= (f "BB") "AAAAAAAAAAAA"))
+ 
+(check-synth)