Skip to content

Commit 1e3ef7e

Browse files
Princess: Remove Princess from the blacklist in the testDivisionByZero test
1 parent 11d1c9b commit 1e3ef7e

File tree

1 file changed

+0
-8
lines changed

1 file changed

+0
-8
lines changed

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

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -206,14 +206,6 @@ public void testDivisionByZero() throws SolverException, InterruptedException {
206206
.that(solverToUse())
207207
.isNoneOf(Solvers.YICES2, Solvers.OPENSMT);
208208

209-
if (formulaType.isRationalType()) {
210-
// Division by zero does not work for rationals with Princess.
211-
assume()
212-
.withMessage("Solver %s does not support division by zero", solverToUse())
213-
.that(solverToUse())
214-
.isNotEqualTo(Solvers.PRINCESS);
215-
}
216-
217209
T a = nmgr.makeVariable("a");
218210
T b = nmgr.makeVariable("b");
219211
T zero = nmgr.makeNumber(0);

0 commit comments

Comments
 (0)