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