diff --git a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java index d58b7b51e0..293ebdbfbc 100644 --- a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java @@ -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