diff --git a/src/test/storm/solver/Z3LpSolverTest.cpp b/src/test/storm/solver/Z3LpSolverTest.cpp index 3ef610380..c0c25e072 100644 --- a/src/test/storm/solver/Z3LpSolverTest.cpp +++ b/src/test/storm/solver/Z3LpSolverTest.cpp @@ -15,6 +15,22 @@ #include +// Early versions sometimes have buggy features. We therefore might disable some tests. +#include +bool z3AtLeastVersion(unsigned expectedMajor, unsigned expectedMinor, unsigned expectedBuildNumber) { + std::vector 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 solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; @@ -275,6 +291,10 @@ 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."; + } solver.push(); ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y", 10)); ASSERT_NO_THROW(solver.addConstraint("", y <= solver.getConstant(20)));