Skip to content

Commit 61acda9

Browse files
committed
fix test for CVC4 with exception
1 parent 6a448ef commit 61acda9

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -184,8 +184,8 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti
184184
BooleanFormula inRange2 = smgr.in(x, smgr.intersection(smgr.range('a', 'Δ'), regexAllChar));
185185
if (solverToUse() == Solvers.CVC4) {
186186
// CVC4 has issues with range and special Unicode characters when solving constraints
187-
assertThrows(SolverException.class, () -> assertThatFormula(inRange).isSatisfiable());
188-
assertThrows(SolverException.class, () -> assertThatFormula(inRange2).isSatisfiable());
187+
assertThrows(AssertionError.class, () -> assertThatFormula(inRange).isSatisfiable());
188+
assertThrows(AssertionError.class, () -> assertThatFormula(inRange2).isSatisfiable());
189189
} else {
190190
assertThatFormula(inRange).isSatisfiable();
191191
assertThatFormula(inRange2).isSatisfiable();

0 commit comments

Comments
 (0)