diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 0b66e6b4c..2fdc57234 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -554,6 +554,18 @@ static z3::expr getExpr(ExprEngine::ValuePtr v, ExprData &exprData)
         return getExpr(b.get(), exprData);
     }
 
+    if (auto c = std::dynamic_pointer_cast<ExprEngine::ConditionalValue>(v)) {
+        if (c->values.size() == 1)
+            return ::getExpr(c->values[0].second, exprData);
+
+        return z3::ite(::getExpr(c->values[1].first, exprData),
+                       ::getExpr(c->values[1].second, exprData),
+                       ::getExpr(c->values[0].second, exprData));
+    }
+
+    if (v->type == ExprEngine::ValueType::UninitValue)
+        return exprData.c.int_val(0);
+
     throw std::runtime_error("Internal error: Unhandled value type");
 }
 #endif
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 15da29fb6..a682685b7 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -197,7 +197,11 @@ private:
     void array3() {
         const char code[] = "void f(unsigned char x) { int arr[10]; arr[4] = 43; return arr[x] == 12; }";
         ASSERT_EQUALS("?,43", getRange(code, "arr[x]"));
-        // TODO: ASSERT_EQUALS("", expr(code, "=="));
+        ASSERT_EQUALS("(declare-fun v0 () Int)\n"
+                      "(assert (<= v0 255))\n"
+                      "(assert (>= v0 0))\n"
+                      "(assert (= (ite (= v0 4) 43 0) 12))\n",
+                      expr(code, "=="));
     }
 
     void array4() {