From bf951ea5e65a6f03af23319f2ffd7e8e51eb2a98 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Sun, 13 Dec 2020 19:53:29 +0100
Subject: [PATCH] Bug hunting; Fix for '*x=y'

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

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 72c0fd83c..f688407a4 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1787,6 +1787,10 @@ static void assignExprValue(const Token *expr, ExprEngine::ValuePtr value, Data
             auto val = std::dynamic_pointer_cast<ExprEngine::AddressOfValue>(pval);
             if (val)
                 data.assignValue(expr, val->varId, value);
+        } else if (pval && pval->type == ExprEngine::ValueType::ArrayValue) {
+            auto arrayValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(pval);
+            auto indexValue = std::make_shared<ExprEngine::IntRange>("0", 0, 0);
+            arrayValue->assign(indexValue, value);
         } else if (pval && pval->type == ExprEngine::ValueType::BinOpResult) {
             auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(pval);
             if (b && b->binop == "+") {
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 81c9372fb..774df1d0c 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -84,6 +84,7 @@ private:
         TEST_CASE(array3);
         TEST_CASE(array4);
         TEST_CASE(array5);
+        TEST_CASE(array6);
         TEST_CASE(arrayInit1);
         TEST_CASE(arrayInit2);
         TEST_CASE(arrayUninit);
@@ -593,8 +594,8 @@ private:
                             "    *len = 0;\n"
                             "  *len == 0;\n"
                             "}";
-        // Currently the *len gets a BailoutValue in the loop
-        ASSERT_EQUALS("", expr(code, "=="));
+        ASSERT_EQUALS("(= 0 0)\n"
+                      "z3::sat\n", expr(code, "=="));
     }
 
     void while5() {
@@ -652,6 +653,16 @@ private:
                       trackExecution(code));
     }
 
+    void array6() {
+        const char code[] = "void foo(int *x) {\n"
+                            "  *x = 2;\n"
+                            "  if (*x == 21) {}"
+                            "}";
+        ASSERT_EQUALS("(= 2 21)\n"
+                      "z3::unsat\n",
+                      expr(code, "=="));
+    }
+
     void arrayInit1() {
         ASSERT_EQUALS("0", getRange("inf f() { char arr[10] = \"\"; return arr[4]; }", "arr[4]"));
     }