From f4a3ceb60e4c140eacb2e1bd084d3557b847efb0 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 8 Jun 2020 10:06:49 +0200
Subject: [PATCH] Skipping tests that fail for z3 version 4.8.8 (Issue reported
 at https://github.com/Z3Prover/z3/issues/4465)

---
 .../SparseMaPcaaMultiObjectiveModelCheckerTest.cpp           | 5 +++++
 src/test/storm/solver/Z3LpSolverTest.cpp                     | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
index f7966411e..1fcd25efa 100755
--- a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
@@ -83,6 +83,11 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) {
     std::vector<storm::RationalNumber> lb(2,-eps), ub(2,eps);
     auto bloatingBox = storm::storage::geometry::Hyperrectangle<storm::RationalNumber>(lb,ub).asPolytope();
 
+    if (storm::test::z3AtLeastVersion(4,8,8)) {
+        // TODO: z3 v4.8.8 is known to be broken here. Check if this is fixed in future versions >4.8.8
+        GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
+    }
+    
     EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asExplicitParetoCurveCheckResult<double>().getUnderApproximation()->convertNumberRepresentation<storm::RationalNumber>()));
     EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<double>().getOverApproximation()->convertNumberRepresentation<storm::RationalNumber>()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues));
 
diff --git a/src/test/storm/solver/Z3LpSolverTest.cpp b/src/test/storm/solver/Z3LpSolverTest.cpp
index 8205cb286..dc9be4ac7 100644
--- a/src/test/storm/solver/Z3LpSolverTest.cpp
+++ b/src/test/storm/solver/Z3LpSolverTest.cpp
@@ -129,6 +129,11 @@ TEST(Z3LpSolver, MILPOptimizeMin) {
     ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5)));
     ASSERT_NO_THROW(solver.update());
 
+    if (storm::test::z3AtLeastVersion(4,8,8)) {
+        // TODO: z3 v4.8.8 is known to be broken here. Check if this is fixed in future versions >4.8.8
+        GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
+    }
+    
     ASSERT_NO_THROW(solver.optimize());
     ASSERT_TRUE(solver.isOptimal());
     ASSERT_FALSE(solver.isUnbounded());