From b320eb38d272df29a733fa486c7988629677bd53 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 11 Nov 2019 10:58:46 +0100
Subject: [PATCH] z3LpSolverTest: Skipping a test if not supported by installed
 z3 version.

---
 src/test/storm/solver/Z3LpSolverTest.cpp | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

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