From 9507fccfc18573a1eb0203873b39b9d47d759d64 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Wed, 15 Jan 2020 19:46:00 +0100
Subject: [PATCH] ExprEngine: Quick hacks for old Z3 compatibility

---
 lib/exprengine.cpp | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 3e36e1357..56d2cfbca 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -599,7 +599,11 @@ struct ExprData {
     }
 
     z3::expr addFloat(const std::string &name) {
+#ifdef OLD_Z3
+        z3::expr e = context.real_val(name.c_str());
+#else
         z3::expr e = context.fpa_const(name.c_str(), 11, 53);
+#endif
         valueExpr.emplace(name, e);
         return e;
     }
@@ -617,7 +621,11 @@ struct ExprData {
         if (b->binop == "/")
             return op1 / op2;
         if (b->binop == "%")
+#ifdef OLD_Z3
+            return op1;
+#else
             return op1 % op2;
+#endif
         if (b->binop == "==")
             return int_expr(op1) == int_expr(op2);
         if (b->binop == "!=")
@@ -646,7 +654,11 @@ struct ExprData {
             throw VerifyException(nullptr, "Can not solve expressions, operand value is null");
         if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
             if (intRange->name[0] != '$')
+#ifdef OLD_z3
+                return context.int_val((long long)(intRange->minValue));
+#else
                 return context.int_val(int64_t(intRange->minValue));
+#endif
             auto it = valueExpr.find(v->name);
             if (it != valueExpr.end())
                 return it->second;