Skip to content

Commit 3141539

Browse files
Princess: Update a test in FormulaClassifierTest
Princess no longer rewrites the formula and will now return the correct result
1 parent f87a843 commit 3141539

File tree

1 file changed

+1
-6
lines changed

1 file changed

+1
-6
lines changed

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

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -149,12 +149,7 @@ public void test_LRA_2() {
149149
+ "(exists ((a Real) (b Real)) (= (+ y y) (- a b))) "
150150
+ "))";
151151
classifier.visit(mgr.parse(query));
152-
if (solverToUse() == Solvers.PRINCESS) {
153-
// Princess rewrites the formula and uses '-1' for the negation -> Integer arithmetic
154-
assertThat(classifier.toString()).isEqualTo("LIRA");
155-
} else {
156-
assertThat(classifier.toString()).isEqualTo("LRA");
157-
}
152+
assertThat(classifier.toString()).isEqualTo("LRA");
158153
}
159154

160155
@Test

0 commit comments

Comments
 (0)