From 229e39e7de28bb9f8059dec6c0518a916e10020e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Sun, 20 Dec 2020 16:36:22 +0100 Subject: [PATCH] Revert "ExprEngine: Fixed float value" This reverts commit 1f9edc6a66de1d6d218eeee95f1ca8e17130f6a9. --- lib/exprengine.cpp | 7 ------- test/testexprengine.cpp | 18 ++---------------- 2 files changed, 2 insertions(+), 23 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index fc78d3bcc..ff7c20533 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -1211,13 +1211,6 @@ public: } if (auto floatRange = std::dynamic_pointer_cast(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 52d0a94b3..f868f1fdd 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -103,7 +103,6 @@ private: TEST_CASE(functionCall5); TEST_CASE(functionCallContract1); - TEST_CASE(functionCallContract2); TEST_CASE(int1); @@ -716,8 +715,8 @@ private: } void floatValue3() { - const char code[] = "void foo(float f) { return f > 12.3; }"; - const char expected[] = "(> $1 (/ 123.0 10.0))\n" + const char code[] = "void foo(float f) { return f > 12.0; }"; + const char expected[] = "(> $1 |12.0|)\n" "z3::sat\n"; ASSERT_EQUALS(expected, expr(code, ">")); } @@ -770,19 +769,6 @@ 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"