1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/issue3247.smt2 b/test/regress/regress1/sygus/issue3247.smt2
new file mode 100644
index 000000000..6784b8797
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3247.smt2
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inference --strings-exp
+(set-logic ALL)
+(declare-fun a () String) 
+(declare-fun b () String) 
+(declare-fun c () String)
+(declare-fun d () String)
+(declare-fun f () String)
+(declare-fun e () String)
+(assert
+  (not
+    (=
+      (str.contains
+        c
+        (str.replace d (str.substr b 0 (str.len d)) "A")
+      )
+      (str.contains c "A")
+    )
+  )
+)
+(assert (= a (str.++ c f)))
+(assert (= b (str.++ d e)))
+(check-sat)