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;