Skip to content

Commit c66f368

Browse files
committed
improve tests.
1 parent 8a44e21 commit c66f368

File tree

1 file changed

+7
-5
lines changed

1 file changed

+7
-5
lines changed

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

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,7 @@ public void testGetRationals() throws SolverException, InterruptedException {
185185
/** Test that different names are no problem for Bools in the model. */
186186
@Test
187187
public void testGetBooleans() throws SolverException, InterruptedException {
188-
// Some names are specificly chosen to test the Boolector model
188+
// Some names are specifically chosen to test the Boolector model
189189
for (String name : VARIABLE_NAMES) {
190190
testModelGetters(bmgr.makeVariable(name), bmgr.makeBoolean(true), true, name);
191191
}
@@ -1208,7 +1208,7 @@ public void testGetArrays4() throws SolverException, InterruptedException {
12081208
ImmutableList.of(BigInteger.valueOf(5)));
12091209
}
12101210

1211-
@Test(expected = IllegalArgumentException.class)
1211+
@Test
12121212
@SuppressWarnings("CheckReturnValue")
12131213
public void testGetArrays4invalid() throws SolverException, InterruptedException {
12141214
requireParser();
@@ -1230,7 +1230,9 @@ public void testGetArrays4invalid() throws SolverException, InterruptedException
12301230
assertThat(prover).isSatisfiable();
12311231

12321232
try (Model m = prover.getModel()) {
1233-
m.evaluate(amgr.makeArray("arr", ARRAY_TYPE_INT_INT));
1233+
assertThrows(
1234+
IllegalArgumentException.class,
1235+
() -> m.evaluate(amgr.makeArray("arr", ARRAY_TYPE_INT_INT)));
12341236
}
12351237
}
12361238
}
@@ -2311,15 +2313,15 @@ public void modelAfterSolverCloseTest() throws SolverException, InterruptedExcep
23112313
public void testGenerateModelsOption() throws SolverException, InterruptedException {
23122314
try (ProverEnvironment prover = context.newProverEnvironment()) { // no option
23132315
assertThat(prover).isSatisfiable();
2314-
assertThrows(IllegalArgumentException.class, () -> prover.getModel());
2316+
assertThrows(IllegalStateException.class, () -> prover.getModel());
23152317
}
23162318
}
23172319

23182320
@Test
23192321
public void testGenerateModelsOption2() throws SolverException, InterruptedException {
23202322
try (ProverEnvironment prover = context.newProverEnvironment()) { // no option
23212323
assertThat(prover).isSatisfiable();
2322-
assertThrows(IllegalArgumentException.class, () -> prover.getModelAssignments());
2324+
assertThrows(IllegalStateException.class, () -> prover.getModelAssignments());
23232325
}
23242326
}
23252327

0 commit comments

Comments
 (0)