From 5701f6d3687740f53ad06e27fd9dd883ad6d08a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Sun, 20 Dec 2020 19:04:46 +0100
Subject: [PATCH] ExprEngine: Added ifIntRangeAlwaysFalse and
 ifIntRangeAlwaysTrue tests

---
 lib/exprengine.cpp      |  3 +++
 test/testexprengine.cpp | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index ff7c20533..694415fdb 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -2504,6 +2504,9 @@ static std::string execute(const Token *start, const Token *end, Data &data)
             if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(condValue)) {
                 canBeFalse = b->isEqual(&data, 0);
                 canBeTrue = b->isTrue(&data);
+            } else if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(condValue)) {
+                canBeFalse = i->isEqual(&data, 0);
+                canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared<ExprEngine::IntRange>("0", 0, 0)).isTrue(&data);
             }
 
             Data &thenData(data);
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index f868f1fdd..2d94376c8 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -65,6 +65,8 @@ private:
         TEST_CASE(ifelse1);
         TEST_CASE(ifif);
         TEST_CASE(ifreturn);
+        TEST_CASE(ifIntRangeAlwaysFalse);
+        TEST_CASE(ifIntRangeAlwaysTrue);
 
         TEST_CASE(istream);
 
@@ -487,6 +489,40 @@ private:
                       expr(code, "=="));
     }
 
+    void ifIntRangeAlwaysFalse() {
+        const char code[] = "void foo(unsigned char x) {\n"
+                            "  if (x > 0)\n"
+                            "      return;\n"
+                            "  if (x) {\n"  // <-- condition should be "always false".
+                            "      x++;\n"
+                            "  }\n"
+                            "  return x == 0;\n" // <- sat
+                            "}";
+        ASSERT_EQUALS("(<= $1 0)\n"
+                      "(= $1 0)\n"
+                      "(and (>= $1 0) (<= $1 255))\n"
+                      "(= $1 0)\n"
+                      "z3::sat\n",
+                      expr(code, "=="));
+    }
+
+    void ifIntRangeAlwaysTrue() {
+        const char code[] = "void foo(unsigned char x) {\n"
+                            "  if (x < 1)\n"
+                            "      return;\n"
+                            "  if (x) {\n"  // <-- condition should be "always true".
+                            "      x++;\n"
+                            "  }\n"
+                            "  return x == 0;\n" // <- unsat
+                            "}";
+        ASSERT_EQUALS("(>= $1 1)\n"
+                      "(distinct $1 0)\n"
+                      "(and (>= $1 0) (<= $1 255))\n"
+                      "(= (+ $1 1) 0)\n"
+                      "z3::unsat\n",
+                      expr(code, "=="));
+    }
+
     void istream() {
         const char code[] = "void foo(const std::string& in) {\n"
                             "    std::istringstream istr(in);\n"