Skip to content

Commit a58cc80

Browse files
Princess: Fix the broken test
Princess will rewrite "floor" as an epsilon term. We'll have to match it in the visitor and restore the original call to get this to work
1 parent 2347d94 commit a58cc80

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -126,11 +126,11 @@ public void forallFloorIsLessThanValueTest() throws SolverException, Interrupted
126126
public void visitFloorTest() {
127127
requireRationals();
128128
requireRationalFloor();
129-
// TODO Princess will rewrite floor. Add backtranslation in the visitor
129+
// TODO Princess will rewrite floor. Add back translation in the visitor
130130
assume()
131131
.withMessage("We don't support \"floor\" in the Princess visitor")
132132
.that(solverToUse())
133-
.isEqualTo(Solvers.PRINCESS);
133+
.isNotEqualTo(Solvers.PRINCESS);
134134

135135
IntegerFormula f = rmgr.floor(rmgr.makeVariable("v"));
136136
assertThat(mgr.extractVariables(f)).hasSize(1);

0 commit comments

Comments
 (0)