Add regression for issue 6191 (#6264)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1a773de0a61e3d738615f460631dae7a3c4d5c3e..232a7f7ab6051e993dcb1000c2aa8b30e2cf376d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2039,6 +2039,7 @@ set(regress_1_tests
   regress1/strings/issue6075-repl-len-one-rr.smt2
   regress1/strings/issue6132-non-unique-skolem.smt2
   regress1/strings/issue6142-repl-inv-rew.smt2
+  regress1/strings/issue6191-replace-all.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue6191-replace-all.smt2 b/test/regress/regress1/strings/issue6191-replace-all.smt2
new file mode 100644 (file)
index 0000000..cd4428d
--- /dev/null
+++ b/test/regress/regress1/strings/issue6191-replace-all.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --strings-exp --no-strings-lazy-pp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x_9 () String)                                                        
+(declare-fun literal_19 () String)                                                 
+(declare-fun x_20 () String)                                                       
+(assert (= literal_19 "\u{3c}\u{64}\u{69}\u{76}"))                                 
+(assert (= x_9 (str.replace_all x_9 x_20 x_9)))                                    
+(assert (= "\u{3c}\u{2" x_20))                                                     
+(assert (str.<= "\u{3c}\u{" literal_19))                                           
+(check-sat)