From 0aba52f1ae71a729db4a5b17bdea790a0b0080dc Mon Sep 17 00:00:00 2001
From: Karlheinz Friedberger <kfriedberger@gmail.com>
Date: Sat, 3 Feb 2024 13:05:57 +0100
Subject: [PATCH] #292: re-enable tests that were broken by a regression in Z3.
The new version of Z3 works fine on those tests.
---
src/org/sosy_lab/java_smt/test/ModelTest.java | 4 +---
src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java | 3 +--
2 files changed, 2 insertions(+), 5 deletions(-)
diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java
index ca880c17a3..b89f14a658 100644
--- 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
index 15fd10d636..98bd7e8d4b 100644
--- 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");