ExprEngine: Fixed float value

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;

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 code[] = "void foo(float f) { return f > 12.3; }";
-        const char expected[] = "(> $1 |12.0|)\n"
+        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"