diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index f688407a46b..3f225ffa7ba 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -138,6 +138,7 @@
 #include "symboldatabase.h"
 #include "tokenize.h"
 
+#include <cassert>
 #include <limits>
 #include <memory>
 #include <iostream>
@@ -2646,19 +2647,41 @@ static std::string execute(const Token *start, const Token *end, Data &data)
                         data.assignStructMember(tok2, &*structVal, memberName, memberValue);
                         continue;
                     }
+
+                    // Assign a pointer value
                     if (lhs->isUnaryOp("*") && lhs->astOperand1()->varId()) {
                         const Token *varToken = tok2->astOperand1()->astOperand1();
+                        // Get value of the pointer
                         ExprEngine::ValuePtr val = data.getValue(varToken->varId(), varToken->valueType(), varToken);
-                        if (val && val->type == ExprEngine::ValueType::ArrayValue) {
-                            // Try to assign "any" value
-                            auto arrayValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(val);
-                            arrayValue->assign(std::make_shared<ExprEngine::IntRange>("0", 0, 0), std::make_shared<ExprEngine::BailoutValue>());
+                        if (!val || (val->type != ExprEngine::ValueType::ArrayValue &&
+                                     val->type != ExprEngine::ValueType::AddressOfValue))
+                            throw ExprEngineException(tok2, "Unhandled assignment in loop");
+                        // Handle the value that we are pointing to
+                        int varid = varToken->varId();
+                        if (changedVariables.find(varid) != changedVariables.end())
                             continue;
+                        changedVariables.insert(varid);
+                        auto oldValue = data.getValue(varid, nullptr, nullptr);
+                        if (oldValue && oldValue->isUninit())
+                            call(data.callbacks, varToken, oldValue, &data);
+                        if (val->type == ExprEngine::ValueType::ArrayValue) {
+                            // Unknown pointer, array or struct
+                            auto arrayValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(val);
+                            assert(arrayValue);
+                            data.assignValue(tok2, varid, val);
+                        } else if (val->type == ExprEngine::ValueType::AddressOfValue) {
+                            // Address of a known variable
+                            auto addressOf = std::dynamic_pointer_cast<ExprEngine::AddressOfValue>(val);
+                            assert(addressOf);
+                            data.assignValue(tok2, varid, val);
                         }
+                        continue;
                     }
+
                     if (!lhs->variable())
                         throw ExprEngineException(tok2, "Unhandled assignment in loop");
-                    // give variable "any" value
+
+                    // Give variable "any" value
                     int varid = lhs->varId();
                     if (changedVariables.find(varid) != changedVariables.end())
                         continue;
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 774df1d0cf6..cd3ae9b57cb 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -50,6 +50,7 @@ class TestExprEngine : public TestFixture {
         TEST_CASE(expr9);
         TEST_CASE(exprAssign1);
         TEST_CASE(exprAssign2); // Truncation
+        TEST_CASE(exprAssign3);
         TEST_CASE(exprNot);
 
         TEST_CASE(getValueConst1);
@@ -78,6 +79,8 @@ class TestExprEngine : public TestFixture {
         TEST_CASE(while3);
         TEST_CASE(while4);
         TEST_CASE(while5);
+        TEST_CASE(while6);
+        TEST_CASE(while7);
 
         TEST_CASE(array1);
         TEST_CASE(array2);
@@ -355,7 +358,11 @@ class TestExprEngine : public TestFixture {
     }
 
     void exprAssign2() {
-        ASSERT_EQUALS("2", getRange("void f(unsigned char x) { x = 258; int a = x }", "a=x"));
+        ASSERT_EQUALS("2", getRange("void f(unsigned char x) { x = 258; int a = x; }", "a=x"));
+    }
+
+    void exprAssign3() {
+        ASSERT_EQUALS("1", getRange("void f(unsigned char *a) { *a = 1; }", "*a=1"));
     }
 
     void exprNot() {
@@ -607,6 +614,27 @@ class TestExprEngine : public TestFixture {
         ASSERT(getRange(code, "x", 4).find("?") != std::string::npos);
     }
 
+    void while6() {
+        const char code[] = "void f(int *arr) {\n"
+                            "  while (cond)\n"
+                            "    *arr = 4;\n"
+                            "  arr[0] == 4;"
+                            "}";
+        ASSERT_EQUALS("(= 4 4)\n"
+                      "z3::sat\n", expr(code, "=="));
+    }
+
+    void while7() {
+        const char code[] = "void foo() {\n"
+                            "  int a = 2;\n"
+                            "  int *p = &a;\n"
+                            "  while (1) *p = 0;\n"
+                            "  return a == 2;\n"
+                            "}";
+        ASSERT_EQUALS("(= 0 2)\n"
+                      "z3::unsat\n", expr(code, "=="));
+    }
+
 
     void array1() {
         ASSERT_EQUALS("(= 5 0)\nz3::unsat\n",