From 13b5bcbfd933461526f08c6ad759af9e129d6764 Mon Sep 17 00:00:00 2001
From: Timotej Kapus <timotej.kapus13@imperial.ac.uk>
Date: Fri, 16 Mar 2018 10:42:12 +0000
Subject: Improve handling of constant array in Z3

---
 lib/Expr/ExprUtil.cpp | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'lib/Expr')

diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index ed60a4a9..2106b226 100644
--- a/lib/Expr/ExprUtil.cpp
+++ b/lib/Expr/ExprUtil.cpp
@@ -104,6 +104,21 @@ public:
     : objects(_objects) {}
 };
 
+ExprVisitor::Action ConstantArrayFinder::visitRead(const ReadExpr &re) {
+  const UpdateList &ul = re.updates;
+
+  // FIXME should we memo better than what ExprVisitor is doing for us?
+  for (const UpdateNode *un = ul.head; un; un = un->next) {
+    visit(un->index);
+    visit(un->value);
+  }
+
+  if (ul.root->isConstantArray()) {
+    results.insert(ul.root);
+  }
+
+  return Action::doChildren();
+}
 }
 
 template<typename InputIterator>
-- 
cgit 1.4.1