Skip to content

Commit a8f965c

Browse files
daniel-rafflerbaierd
authored andcommitted
SolverThreadLocalityTest: Don't catch InvalidConfigurationExceptions when trying to create a new solver context. See #345 (comment)
1 parent 57d1f00 commit a8f965c

File tree

1 file changed

+3
-12
lines changed

1 file changed

+3
-12
lines changed

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

+3-12
Original file line numberDiff line numberDiff line change
@@ -73,15 +73,7 @@ public void nonlocalContextTest()
7373
requireIntegers();
7474
assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5);
7575

76-
Future<SolverContext> result =
77-
executor.submit(
78-
() -> {
79-
try {
80-
return factory.generateContext();
81-
} catch (InvalidConfigurationException e) {
82-
throw new RuntimeException(e);
83-
}
84-
});
76+
Future<SolverContext> result = executor.submit(() -> factory.generateContext());
8577

8678
try (SolverContext newContext = result.get()) {
8779
FormulaManager newMgr = newContext.getFormulaManager();
@@ -289,7 +281,8 @@ public <T> void nonlocalInterpolationTest() throws InterruptedException, Executi
289281

290282
@SuppressWarnings("resource")
291283
@Test
292-
public void wrongContextTest() throws InterruptedException, SolverException {
284+
public void wrongContextTest()
285+
throws InterruptedException, SolverException, InvalidConfigurationException {
293286
assume()
294287
.that(solverToUse())
295288
.isNoneOf(
@@ -333,8 +326,6 @@ public void wrongContextTest() throws InterruptedException, SolverException {
333326
prover.push(formula);
334327
assertThat(prover).isUnsatisfiable();
335328
}
336-
} catch (InvalidConfigurationException e) {
337-
throw new RuntimeException(e);
338329
}
339330
}
340331
}

0 commit comments

Comments
 (0)