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");