allow more local bug detection.
@@ -938,12 +938,11 @@ public class InterpolatingProverTest extends SolverBasedTest0 {
}
/* This is a testcase that failed with Princess and seq interpolants. */
- @SuppressWarnings("unused")
@Test
public <T> void bigSeqInterpolationTest() throws InterruptedException, SolverException {
requireBitvectors();
requireInterpolation();
- try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
+
int bvWidth = 32;
BitvectorFormula bv0 = bvmgr.makeBitvector(bvWidth, 0);
BitvectorFormula bv1 = bvmgr.makeBitvector(bvWidth, 1);
@@ -996,10 +995,11 @@ public class InterpolatingProverTest extends SolverBasedTest0 {
bvmgr.equal(c, bmgr.ifThenElse(bvmgr.lessOrEquals(p3, t2, true), bv1, bv0)),
bvmgr.equal(c, bv0));
+ try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
T id1 = prover.push(f2);
T id2 = prover.push(f1);
- boolean check = prover.isUnsat();
- assertWithMessage("formulas must be contradicting").that(check).isTrue();
+ assertThat(prover).isUnsatisfiable();
+ @SuppressWarnings("unused")
List<BooleanFormula> interpolants = prover.getSeqInterpolants0(ImmutableList.of(id1, id2));
}
}
