diff options
Diffstat (limited to 'test/regress/regress2')
3 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/regress2/strings/issue6057-replace-re-all-simplified.smt2 b/test/regress/regress2/strings/issue6057-replace-re-all-simplified.smt2 new file mode 100644 index 000000000..83860ef86 --- /dev/null +++ b/test/regress/regress2/strings/issue6057-replace-re-all-simplified.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun literal_5 () String) +(assert (not (= + literal_5 + (str.replace_re_all + literal_5 + (re.++ (re.* re.allchar) (str.to_re "\u{5c}\u{3c}\u{53}\u{43}\u{52}\u{49}\u{50}\u{54}") (re.* re.allchar)) + literal_5)))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress2/strings/issue6057-replace-re-all.smt2 b/test/regress/regress2/strings/issue6057-replace-re-all.smt2 new file mode 100644 index 000000000..9819b75dd --- /dev/null +++ b/test/regress/regress2/strings/issue6057-replace-re-all.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun literal_0 () String) +(assert (and (str.<= (str.++ literal_0 "\u{2f}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2f}\u{74}\u{79}\u{70}\u{65}\u{2f}\u{6e}\u{75}\u{6d}\u{65}\u{72}\u{69}\u{63}\u{61}\u{6c}\u{2f}\u{65}\u{64}\u{69}\u{74}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2e}\u{68}\u{74}\u{6d}\u{6c}") +(str.replace_re_all (str.replace_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}" (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) literal_0) (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) (str.replace_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}" (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) literal_0))) +(str.<= (str.++ literal_0 "\u{2f}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2f}\u{74}\u{79}\u{70}\u{65}\u{2f}\u{6e}\u{75}\u{6d}\u{65}\u{72}\u{69}\u{63}\u{61}\u{6c}\u{2f}\u{65}\u{64}\u{69}\u{74}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2e}\u{68}\u{74}\u{6d}\u{6c}") (str.replace_re_all (str.replace_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}" (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) literal_0) (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) (str.replace_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}" (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) literal_0))))) +(assert (not (str.<= "\u{2f}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2f}\u{74}\u{79}\u{70}\u{65}\u{2f}\u{6e}\u{75}\u{6d}\u{65}\u{72}\u{69}\u{63}\u{61}\u{6c}\u{2f}\u{65}\u{64}\u{69}\u{74}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2e}\u{68}\u{74}\u{6d}\u{6c}" "\u{2f}\u{65}\u{76}\u{69}\u{6c}"))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress2/strings/replace_re.smt2 b/test/regress/regress2/strings/replace_re.smt2 index 1f9b2a2ee..a58314150 100644 --- a/test/regress/regress2/strings/replace_re.smt2 +++ b/test/regress/regress2/strings/replace_re.smt2 @@ -40,3 +40,11 @@ (set-info :status unsat) (check-sat) (pop) + +(push) +(assert (= "FOO" (str.replace_re x (re.union (str.to_re "A") (str.to_re "ABC")) "FOO"))) +(assert (not (= x "FOO"))) +(assert (> (str.len x) 1)) +(set-info :status unsat) +(check-sat) +(pop) |