From c3e798968c0a93ffa0e8727952cd2af2c04281b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Mon, 21 Dec 2020 13:23:08 +0100
Subject: [PATCH] ExprEngine; Fix floating point comparison

---
 lib/exprengine.cpp      |  7 +++++++
 test/testexprengine.cpp | 19 +++++++++++++++++--
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 74a7b36ac..44de43c41 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1215,6 +1215,13 @@ public:
         }
 
         if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) {
+            if (floatRange->name[0] != '$')
+#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
+                return context.fpa_val(static_cast<double>(floatRange->minValue));
+#else
+                return context.real_val(floatRange->name.c_str());
+#endif
+
             auto it = valueExpr.find(v->name);
             if (it != valueExpr.end())
                 return it->second;
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 2d94376c8..d86006956 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -105,6 +105,7 @@ private:
         TEST_CASE(functionCall5);
 
         TEST_CASE(functionCallContract1);
+        TEST_CASE(functionCallContract2);
 
         TEST_CASE(int1);
 
@@ -151,6 +152,7 @@ private:
             }
             replace(line, "(fp.gt ", "(> ");
             replace(line, "(fp.lt ", "(< ");
+            replace(line, "(fp #b0 #b10000000010 #x899999999999a)", "12.3");
             int par = 0;
             for (char pos : line) {
                 if (pos == '(')
@@ -751,8 +753,8 @@ private:
     }
 
     void floatValue3() {
-        const char code[] = "void foo(float f) { return f > 12.0; }";
-        const char expected[] = "(> $1 |12.0|)\n"
+        const char code[] = "void foo(float f) { return f > 12.3; }";
+        const char expected[] = "(> $1 12.3)\n"
                                 "z3::sat\n";
         ASSERT_EQUALS(expected, expr(code, ">"));
     }
@@ -805,6 +807,19 @@ private:
                       functionCallContractExpr(code, s));
     }
 
+    void functionCallContract2() {
+        const char code[] = "void foo(float x);\n"
+                            "void bar(float x) { foo(x); }";
+
+        Settings s;
+        s.functionContracts["foo(x)"] = "x < 12.3";
+
+        ASSERT_EQUALS("checkContract:{\n"
+                      "(ite (< $2 12.3) false true)\n"
+                      "}\n",
+                      functionCallContractExpr(code, s));
+    }
+
 
     void int1() {
         ASSERT_EQUALS("(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n"