Skip to content

Commit

Permalink
use common code to disable a quantifier-based test for Princess.
Browse files Browse the repository at this point in the history
  • Loading branch information
kfriedberger committed Aug 27, 2023
1 parent 6eeb747 commit 3797fa7
Showing 1 changed file with 6 additions and 8 deletions.
14 changes: 6 additions & 8 deletions src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -454,19 +454,17 @@ public void testBVExistsArrayConjunct3() throws SolverException, InterruptedExce
public void testLIAExistsArrayDisjunct1() throws SolverException, InterruptedException {
// (exists x . b[x] = 0) OR (forall x . b[x] = 1) is SAT

// Princess can not solve this test since version 2023-06-19. Bug is reported.
// TODO enable this test with the next update of Princess.
assume()
.withMessage("Solver %s does not solve this formula", solverToUse())
.that(solverToUse())
.isNotEqualTo(Solvers.PRINCESS);

requireIntegers();
BooleanFormula f =
bmgr.or(
qmgr.exists(ImmutableList.of(x), a_at_x_eq_0),
qmgr.forall(ImmutableList.of(x), a_at_x_eq_1));
assertThatFormula(f).isSatisfiable();
try {
// Princess fails this
assertThatFormula(f).isSatisfiable();
} catch (SolverException e) {
throw handleSolverException(e);
}
}

@Test
Expand Down

0 comments on commit 3797fa7

Please sign in to comment.