From 1f9edc6a66de1d6d218eeee95f1ca8e17130f6a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Sun, 20 Dec 2020 15:20:21 +0100
Subject: [PATCH] ExprEngine: Fixed float value

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

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index ff7c20533..fc78d3bcc 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1211,6 +1211,13 @@ public:
         }
 
         if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) {
+            if (std::isdigit(floatRange->name[0]))
+#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
+                return context.fpa_val(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 f868f1fdd..52d0a94b3 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -103,6 +103,7 @@ private:
         TEST_CASE(functionCall5);
 
         TEST_CASE(functionCallContract1);
+        TEST_CASE(functionCallContract2);
 
         TEST_CASE(int1);
 
@@ -715,8 +716,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 (/ 123.0 10.0))\n"
                                 "z3::sat\n";
         ASSERT_EQUALS(expected, expr(code, ">"));
     }
@@ -769,6 +770,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 >= 0.5";
+
+        ASSERT_EQUALS("checkContract:{\n"
+                      "(ite (>= $2 (/ 1.0 2.0)) false true)\n"
+                      "}\n",
+                      functionCallContractExpr(code, s));
+    }
+
 
     void int1() {
         ASSERT_EQUALS("(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n"