Skip to content

Commit a723ab4

Browse files
Strings: Patch a bug in testConstStringReplaceAll
The test uses Strings.replaceAll and compares it to the result of str.replace_all in SMTLIB. However, the two functions behave different when the "matching" String is empty, and we need a special case for that.
1 parent 646db34 commit a723ab4

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1640,15 +1640,16 @@ public void testConstStringReplaceAll() throws SolverException, InterruptedExcep
16401640
.isNotEqualTo(Solvers.Z3);
16411641

16421642
for (int i = 0; i < WORDS.size(); i++) {
1643-
for (int j = 1; j < WORDS.size(); j++) {
1643+
for (int j = 0; j < WORDS.size(); j++) {
16441644
String word1 = WORDS.get(i);
16451645
String word2 = WORDS.get(j);
16461646
String word3 = "replacement";
16471647
StringFormula word1F = smgr.makeString(word1);
16481648
StringFormula word2F = smgr.makeString(word2);
16491649
StringFormula word3F = smgr.makeString(word3);
16501650

1651-
StringFormula result = smgr.makeString(word3.replaceAll(word2, word1));
1651+
StringFormula result =
1652+
smgr.makeString(word2.isEmpty() ? word3 : word3.replaceAll(word2, word1));
16521653
assertEqual(smgr.replaceAll(word3F, word2F, word1F), result);
16531654
}
16541655
}

0 commit comments

Comments
 (0)