From 1c12b4fd78c39dbbe696e3e15680088b5741db03 Mon Sep 17 00:00:00 2001
From: Georgy Komarov <jubnzv@gmail.com>
Date: Sat, 26 Dec 2020 23:29:50 +0300
Subject: [PATCH] ExprEngine: Handling cases when for condition is always false
 (#2984)

---
 lib/exprengine.cpp      |  4 ++++
 test/testexprengine.cpp | 17 +++++++++++++++++
 2 files changed, 21 insertions(+)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index d646ec5b8..c1095a8c4 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -2669,6 +2669,10 @@ static std::string execute(const Token *start, const Token *end, Data &data)
                 data.assignValue(tok, varid, loopValues);
                 tok = tok->linkAt(1);
                 loopValues->loopScope = tok->next()->scope();
+                // Check whether the condition expression is always false
+                if (tok->next() && (initValue > lastValue)) {
+                    tok = tok->next()->link();
+                }
                 continue;
             }
         }
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index daabd2bf9..42fbc5dd2 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -79,6 +79,7 @@ private:
         TEST_CASE(switch2);
 
         TEST_CASE(for1);
+        TEST_CASE(forAlwaysFalse1);
 
         TEST_CASE(while1);
         TEST_CASE(while2);
@@ -660,6 +661,22 @@ private:
                       expr(code, "=="));
     }
 
+    void forAlwaysFalse1() {
+        const char code[] = "int f() {\n"
+                            "  int a = 19;\n"
+                            "  for (int i = 0; i < 0; i++)\n"
+                            "    a += 8;\n"
+                            "  for (int i = 0; i < 1; i++)\n"
+                            "    a += 23;\n"
+                            "  for (int i = 100; i >= 1; i--)\n"
+                            "    a += 23;\n"
+                            "  return a == 42;\n"
+                            "}";
+        const char expected[] = "(and (>= $4 (- 2147483648)) (<= $4 2147483647))\n"
+                                "(= (+ $4 23) 42)\n"
+                                "z3::sat\n";
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
 
     void while1() {
         const char code[] = "void f(int y) {\n"