#292: re-enable tests that were broken by a regression in Z3.

The new version of Z3 works fine on those tests.
sosy-lab · Feb 3, 2024 · 0aba52f · 0aba52f
1 parent b10a31e
commit 0aba52f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 5 deletions.
diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java
@@ -2210,9 +2210,7 @@ public void arrayTest5()
     assume()
         .withMessage("Solver is quite slow for this example")
         .that(solverToUse())
-        .isNoneOf(Solvers.PRINCESS, Solvers.Z3);
-    // TODO regression:
-    //  the Z3 library was able to solve this in v4.11.2, but no longer in v4.12.1-glibc_2.27.
+        .isNotEqualTo(Solvers.PRINCESS);
 
     BooleanFormula formula =
         context

diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
@@ -378,9 +378,8 @@ public void testStringCompare() throws SolverException, InterruptedException {
     assume()
         .withMessage("Solver is quite slow for this example")
         .that(solverToUse())
-        .isNoneOf(Solvers.Z3, Solvers.CVC5);
+        .isNotEqualTo(Solvers.CVC5);
     // TODO regression:
-    // - the Z3 library was able to solve this in v4.11.2, but no longer in v4.12.1-glibc_2.27.
     // - CVC5 was able to solve this in v1.0.2, but no longer in v1.0.5
 
     StringFormula var1 = smgr.makeVariable("0");