Improve handling of constant array in Z3

1 files changed, 15 insertions, 0 deletions

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>