diff --git a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index 9dace3aae..f7966411e 100755 --- a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -53,6 +53,11 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { + + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } + storm::Environment env; env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa); @@ -84,6 +89,10 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } + storm::Environment env; env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa); @@ -139,6 +148,9 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) { + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } storm::Environment env; env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa); diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index d6fe12e73..7c3573076 100755 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -347,6 +347,9 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) { + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index fea9dbb53..1d3d7cc73 100755 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -17,6 +17,9 @@ #include "storm/environment/Environment.h" TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } storm::Environment env; env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa); @@ -47,6 +50,10 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } + storm::Environment env; env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa); @@ -66,6 +73,10 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) { + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } + storm::Environment env; env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa); diff --git a/src/test/storm/solver/Z3LpSolverTest.cpp b/src/test/storm/solver/Z3LpSolverTest.cpp index beb8866c1..8205cb286 100644 --- a/src/test/storm/solver/Z3LpSolverTest.cpp +++ b/src/test/storm/solver/Z3LpSolverTest.cpp @@ -15,22 +15,6 @@ #include <cmath> -// Early versions sometimes have buggy features. We therefore might disable some tests. -#include <z3.h> -bool z3AtLeastVersion(unsigned expectedMajor, unsigned expectedMinor, unsigned expectedBuildNumber) { - std::vector<unsigned> actual(4), expected({expectedMajor, expectedMinor, expectedBuildNumber, 0u}); - Z3_get_version(&actual[0], &actual[1], &actual[2], &actual[3]); - for (uint64_t i = 0; i < 4; ++i) { - if (actual[i] > expected[i]) { - return true; - } - if (actual[i] < expected[i]) { - return false; - } - } - return true; // Equal versions -} - TEST(Z3LpSolver, LPOptimizeMax) { storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; @@ -291,9 +275,8 @@ TEST(Z3LpSolver, Incremental) { ASSERT_TRUE(solver.isOptimal()); EXPECT_EQ(12.0, solver.getContinuousValue(x)); - - if (!z3AtLeastVersion(4,8,5)) { - GTEST_SKIP() << "Test disabled since the z3 version is too old."; + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; } solver.push(); ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y", 10)); diff --git a/src/test/storm_gtest.h b/src/test/storm_gtest.h index 92c93f7b2..9b56f32d3 100644 --- a/src/test/storm_gtest.h +++ b/src/test/storm_gtest.h @@ -49,6 +49,28 @@ namespace storm { } } +// Some tests have to be skipped for specific z3 versions because of a bug that was present in z3. +#ifdef STORM_HAVE_Z3 +#include <z3.h> +namespace storm { + namespace test { + inline bool z3AtLeastVersion(unsigned expectedMajor, unsigned expectedMinor, unsigned expectedBuildNumber) { + std::vector<unsigned> actual(4), expected({expectedMajor, expectedMinor, expectedBuildNumber, 0u}); + Z3_get_version(&actual[0], &actual[1], &actual[2], &actual[3]); + for (uint64_t i = 0; i < 4; ++i) { + if (actual[i] > expected[i]) { + return true; + } + if (actual[i] < expected[i]) { + return false; + } + } + return true; // Equal versions + } + } +} +#endif + #define STORM_SILENT_ASSERT_THROW(statement, expected_exception) \ storm::test::disableOutput(); \