Skip to content

Commit 5900232

Browse files
Fix last merge
The broken test always failed for CVC4, but the exception used to be thrown later. With the new changes we immediately throw an IllegalArgument exception when str.range is called with a bound that is not a single ASCII character. This commit will fix the test to catch the new exception.
1 parent 3a6bce9 commit 5900232

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -180,13 +180,13 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti
180180
assertThatFormula(smgr.in(x, smgr.intersection(smgr.range('a', 'z'), regexAllChar)))
181181
.isSatisfiable();
182182

183-
BooleanFormula inRange = smgr.in(x, smgr.range('a', 'Δ'));
184-
BooleanFormula inRange2 = smgr.in(x, smgr.intersection(smgr.range('a', 'Δ'), regexAllChar));
185183
if (solverToUse() == Solvers.CVC4) {
186184
// CVC4 has issues with range and special Unicode characters when solving constraints
187-
assertThrows(AssertionError.class, () -> assertThatFormula(inRange).isSatisfiable());
188-
assertThrows(AssertionError.class, () -> assertThatFormula(inRange2).isSatisfiable());
185+
assertThrows(IllegalArgumentException.class, () -> smgr.range('a', 'Δ'));
189186
} else {
187+
BooleanFormula inRange = smgr.in(x, smgr.range('a', 'Δ'));
188+
BooleanFormula inRange2 = smgr.in(x, smgr.intersection(smgr.range('a', 'Δ'), regexAllChar));
189+
190190
assertThatFormula(inRange).isSatisfiable();
191191
assertThatFormula(inRange2).isSatisfiable();
192192
}

0 commit comments

Comments
 (0)