1 files changed, 15 insertions, 0 deletions
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 2c2c0018..af4f7b88 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -275,6 +275,21 @@ namespace klee {
     return op1;
   }
 
+  ExprVisitor::Action ExprCmbnVisitor::visitExprPost(const Expr& e) {
+    if (e.getKind() != Expr::Read)
+      return ExprVisitor::Action::doChildren();
+    const auto load = dyn_cast<ReadExpr>(&e);
+
+    const auto orig = load->updates.root;
+    if (orig->name.substr(0, 4) != "out!")
+      return ExprVisitor::Action::doChildren();
+    const auto a = this->arrayCache.CreateArray(
+      orig->name + '!' + this->revision,
+      orig->size, 0, 0, orig->domain, orig->range);
+    return ExprVisitor::Action::changeTo(
+      ReadExpr::create({a, load->updates.head}, load->index));
+  }
+
   bool isSymArg(std::string name) {
     return (name.size() == 5 // string::starts_with requires C++20
             && name[0] == 'a' && name[1] == 'r' && name[2] == 'g'