diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 8563721b96..d99ef39c4c 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -18,6 +18,7 @@
 #include "klee/Statistics/TimerStatIncrementer.h"
 
 #include "CoreStats.h"
+#include <cstring>
 
 namespace klee {
 llvm::cl::OptionCategory
@@ -384,7 +385,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
 // transparently avoid screwing up symbolics (if the byte is symbolic
 // then its concrete cache byte isn't being used) but is just a hack.
 
-void AddressSpace::copyOutConcretes(const Assignment &assignment) {
+void AddressSpace::copyOutConcretes() {
   for (const auto &object : objects) {
     auto &mo = object.first;
     auto &os = object.second;
@@ -392,7 +393,7 @@ void AddressSpace::copyOutConcretes(const Assignment &assignment) {
             dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
       if (!mo->isUserSpecified && !os->readOnly &&
           sizeExpr->getZExtValue() != 0) {
-        copyOutConcrete(mo, os.get(), assignment);
+        copyOutConcrete(mo, os.get());
       }
     }
   }
@@ -407,27 +408,19 @@ ref<ConstantExpr> toConstantExpr(ref<Expr> expr) {
 }
 
 void AddressSpace::copyOutConcrete(const MemoryObject *mo,
-                                   const ObjectState *os,
-                                   const Assignment &assignment) const {
-  if (ref<ConstantExpr> addressExpr =
-          dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
-    auto address =
-        reinterpret_cast<std::uint8_t *>(addressExpr->getZExtValue());
-    AssignmentEvaluator evaluator(assignment, false);
-    if (ref<ConstantExpr> sizeExpr =
-            dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
-      size_t moSize = sizeExpr->getZExtValue();
-      std::vector<uint8_t> concreteStore(moSize);
-      for (size_t i = 0; i < moSize; i++) {
-        auto byte = evaluator.visit(os->readValue8(i));
-        concreteStore[i] = cast<ConstantExpr>(byte)->getZExtValue(Expr::Int8);
-      }
-      std::memcpy(address, concreteStore.data(), moSize);
+                                   const ObjectState *os) const {
+
+  if (auto addressExpr = dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
+    if (auto sizeExpr = dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
+      auto address =
+          reinterpret_cast<std::uint8_t *>(addressExpr->getZExtValue());
+      auto size = sizeExpr->getZExtValue();
+      std::memcpy(address, os->valueOS.concreteStore->data(), size);
     }
   }
 }
 
-bool AddressSpace::copyInConcretes(const Assignment &assignment) {
+bool AddressSpace::copyInConcretes() {
   for (auto &obj : objects) {
     const MemoryObject *mo = obj.first;
 
@@ -436,8 +429,7 @@ bool AddressSpace::copyInConcretes(const Assignment &assignment) {
 
       if (ref<ConstantExpr> arrayConstantAddress =
               dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
-        if (!copyInConcrete(mo, os.get(), arrayConstantAddress->getZExtValue(),
-                            assignment))
+        if (!copyInConcrete(mo, os.get(), arrayConstantAddress->getZExtValue()))
           return false;
       }
     }
@@ -447,24 +439,17 @@ bool AddressSpace::copyInConcretes(const Assignment &assignment) {
 }
 
 bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os,
-                                  uint64_t src_address,
-                                  const Assignment &assignment) {
-  AssignmentEvaluator evaluator(assignment, false);
+                                  uint64_t src_address) {
   auto address = reinterpret_cast<std::uint8_t *>(src_address);
-  size_t moSize =
-      cast<ConstantExpr>(evaluator.visit(mo->getSizeExpr()))->getZExtValue();
-  std::vector<uint8_t> concreteStore(moSize);
-  for (size_t i = 0; i < moSize; i++) {
-    auto byte = evaluator.visit(os->readValue8(i));
-    concreteStore[i] = cast<ConstantExpr>(byte)->getZExtValue(8);
-  }
-  if (memcmp(address, concreteStore.data(), moSize) != 0) {
+  size_t moSize = cast<ConstantExpr>(mo->getSizeExpr())->getZExtValue();
+
+  if (memcmp(address, os->valueOS.concreteStore->data(), moSize) != 0) {
     if (os->readOnly) {
       return false;
     } else {
       ObjectState *wos = getWriteable(mo, os);
       for (size_t i = 0; i < moSize; i++) {
-        wos->write(i, ConstantExpr::create(address[i], Expr::Int8));
+        wos->write8(i, address[i]);
       }
     }
   }
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 520e1bd16d..f3ad08f5bf 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -13,7 +13,6 @@
 #include "Memory.h"
 
 #include "klee/ADT/ImmutableMap.h"
-#include "klee/Expr/Assignment.h"
 #include "klee/Expr/Expr.h"
 #include "klee/System/Time.h"
 
@@ -139,10 +138,9 @@ class AddressSpace {
   /// actual system memory location they were allocated at.
   /// Returns the (hypothetical) number of pages needed provided each written
   /// object occupies (at least) a single page.
-  void copyOutConcretes(const Assignment &assignment);
+  void copyOutConcretes();
 
-  void copyOutConcrete(const MemoryObject *mo, const ObjectState *os,
-                       const Assignment &assignment) const;
+  void copyOutConcrete(const MemoryObject *mo, const ObjectState *os) const;
 
   /// \brief Obtain an ObjectState suitable for writing.
   ///
@@ -164,7 +162,7 @@ class AddressSpace {
   ///
   /// \retval true The copy succeeded.
   /// \retval false The copy failed because a read-only object was modified.
-  bool copyInConcretes(const Assignment &assignment);
+  bool copyInConcretes();
 
   /// Updates the memory object with the raw memory from the address
   ///
@@ -175,7 +173,7 @@ class AddressSpace {
   /// externally
   /// @return
   bool copyInConcrete(const MemoryObject *mo, const ObjectState *os,
-                      uint64_t src_address, const Assignment &assignment);
+                      uint64_t src_address);
 };
 } // namespace klee
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 8d6d5032e2..3099d9bf3d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1140,7 +1140,7 @@ void Executor::initializeGlobalObjects(ExecutionState &state) {
       if (v.isConstant()) {
         os->setReadOnly(true);
         // initialise constant memory that may be used with external calls
-        state.addressSpace.copyOutConcrete(mo, os, {});
+        state.addressSpace.copyOutConcrete(mo, os);
       }
     }
   }
@@ -5252,15 +5252,26 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
                                                 // uniqueness
         ref<Expr> arg = *ai;
         if (auto pointer = dyn_cast<PointerExpr>(arg)) {
-          arg = pointer->getValue();
-        }
-        arg = optimizer.optimizeExpr(arg, true);
-        ref<ConstantExpr> ce = evaluator.visit(arg);
-        ce->toMemory(&args[wordIndex]);
-        if (ExternalCalls == ExternalCallPolicy::All) {
+          ref<ConstantExpr> base = evaluator.visit(pointer->getBase());
+          ref<ConstantExpr> value = evaluator.visit(pointer->getValue());
+          value->toMemory(&args[wordIndex]);
+          ref<ConstantPointerExpr> const_pointer =
+              ConstantPointerExpr::create(base, value);
+          ObjectPair op;
+          if (state.addressSpace.resolveOne(const_pointer, nullptr, op) &&
+              !op.second->readOnly) {
+            auto *os = state.addressSpace.getWriteable(op.first, op.second);
+            os->flushToConcreteStore(model);
+          }
+          addConstraint(state, EqExpr::create(const_pointer->getValue(), arg));
+          wordIndex += (value->getWidth() + 63) / 64;
+        } else {
+          arg = optimizer.optimizeExpr(arg, true);
+          ref<ConstantExpr> ce = evaluator.visit(arg);
+          ce->toMemory(&args[wordIndex]);
           addConstraint(state, EqExpr::create(ce, arg));
+          wordIndex += (ce->getWidth() + 63) / 64;
         }
-        wordIndex += (ce->getWidth() + 63) / 64;
       } else {
         ref<Expr> arg = toUnique(state, *ai);
         if (ConstantExpr *ce = dyn_cast<ConstantExpr>(arg)) {
@@ -5296,7 +5307,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
   solver->getInitialValues(state.constraints.cs(), arrays, values,
                            state.queryMetaData);
   Assignment assignment(arrays, values);
-  state.addressSpace.copyOutConcretes(assignment);
+  state.addressSpace.copyOutConcretes();
 #ifndef WINDOWS
   // Update external errno state with local state value
   ObjectPair result;
@@ -5364,7 +5375,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
     return;
   }
 
-  if (!state.addressSpace.copyInConcretes(assignment)) {
+  if (!state.addressSpace.copyInConcretes()) {
     terminateStateOnExecError(state, "external modified read-only object",
                               StateTerminationType::External);
     return;
@@ -5374,7 +5385,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
   // Update errno memory object with the errno value from the call
   int error = externalDispatcher->getLastErrno();
   state.addressSpace.copyInConcrete(result.first, result.second,
-                                    (uint64_t)&error, assignment);
+                                    (uint64_t)&error);
 #endif
 
   Type *resultType = target->inst()->getType();
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index a13fb97fee..b015df271d 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -21,7 +21,9 @@
 #include "CodeLocation.h"
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/Expr.h"
+#include "klee/Expr/SourceBuilder.h"
 #include "klee/Solver/Solver.h"
+#include "klee/Support/Casting.h"
 #include "klee/Support/ErrorHandling.h"
 
 #include "llvm/IR/Function.h"
@@ -33,6 +35,7 @@
 #include <algorithm>
 #include <cassert>
 #include <cstddef>
+#include <cstdint>
 
 namespace klee {
 llvm::cl::opt<MemoryType> MemoryBackend(
@@ -508,6 +511,10 @@ void ObjectState::print() const {
   baseOS.print();
 }
 
+void ObjectState::flushToConcreteStore(Assignment &assignment) {
+  valueOS.flushToConcreteStore(assignment);
+}
+
 /***/
 
 ObjectStage::ObjectStage(const Array *array, ref<Expr> defaultValue, bool safe,
@@ -517,6 +524,10 @@ ObjectStage::ObjectStage(const Array *array, ref<Expr> defaultValue, bool safe,
       array->getSize(), defaultValue, MaxFixedSizeStructureSize));
   unflushedMask.reset(
       constructStorage(array->getSize(), false, MaxFixedSizeStructureSize));
+
+  if (auto const_size = dyn_cast<ConstantExpr>(size)) {
+    concreteStore.emplace(ConcreteStore(width, const_size->getZExtValue()));
+  }
 }
 
 ObjectStage::ObjectStage(ref<Expr> size, ref<Expr> defaultValue, bool safe,
@@ -525,16 +536,37 @@ ObjectStage::ObjectStage(ref<Expr> size, ref<Expr> defaultValue, bool safe,
   knownSymbolics.reset(constructStorage<ref<Expr>, OptionalRefEq<Expr>>(
       size, defaultValue, MaxFixedSizeStructureSize));
   unflushedMask.reset(constructStorage(size, false, MaxFixedSizeStructureSize));
+
+  if (auto const_size = dyn_cast<ConstantExpr>(size)) {
+    concreteStore.emplace(ConcreteStore(width, const_size->getZExtValue()));
+  }
 }
 
 ObjectStage::ObjectStage(const ObjectStage &os)
     : knownSymbolics(os.knownSymbolics->clone()),
-      unflushedMask(os.unflushedMask->clone()), updates(os.updates),
-      size(os.size), safeRead(os.safeRead), width(os.width) {}
+      concreteStore(os.concreteStore), unflushedMask(os.unflushedMask->clone()),
+      updates(os.updates), size(os.size), safeRead(os.safeRead),
+      width(os.width) {}
 
 /***/
 
 const UpdateList &ObjectStage::getUpdates() const {
+
+  if (auto sizeExpr = dyn_cast<ConstantExpr>(size)) {
+    if (concreteStore->set() == sizeExpr->getZExtValue()) {
+      std::unique_ptr<SparseStorage<ref<ConstantExpr>>> values(constructStorage(
+          sizeExpr, ConstantExpr::create(0, width), MaxFixedSizeStructureSize));
+      for (size_t i = 0; i < sizeExpr->getZExtValue(); ++i) {
+        values->store(i,
+                      ConstantExpr::create(concreteStore->readValue(i), width));
+      }
+      auto array =
+          Array::create(sizeExpr, SourceBuilder::constant(values->clone()),
+                        Expr::Int32, width);
+      updates = UpdateList(array, nullptr);
+    }
+  }
+
   if (auto sizeExpr = dyn_cast<ConstantExpr>(size)) {
     auto size = sizeExpr->getZExtValue();
     if (knownSymbolics->storage().size() == size) {
@@ -584,10 +616,29 @@ void ObjectStage::initializeToZero() {
   unflushedMask->reset();
 }
 
+void ObjectStage::flushToConcreteStore(Assignment &assignment) {
+  AssignmentEvaluator evaluator(assignment, false);
+  if (auto const_size = dyn_cast<ConstantExpr>(size)) {
+    for (size_t i = 0; i < const_size->getZExtValue(); ++i) {
+      if (concreteStore->isConcrete(i)) {
+        continue;
+      }
+      auto byte = evaluator.visit(readWidth(i));
+      // Write expr instead?
+      concreteStore->writeValue(i, cast<ConstantExpr>(byte)->getZExtValue());
+    }
+  }
+}
+
 void ObjectStage::flushForRead() const {
   for (const auto &unflushed : unflushedMask->storage()) {
     auto offset = unflushed.first;
-    auto value = knownSymbolics->load(offset);
+    ref<Expr> value;
+    if (concreteStore && concreteStore->isConcrete(offset)) {
+      value = ConstantExpr::create(concreteStore->readValue(offset), width);
+    } else {
+      value = knownSymbolics->load(offset);
+    }
     assert(value);
     updates.extend(ConstantExpr::create(offset, Expr::Int32), value);
   }
@@ -598,12 +649,20 @@ void ObjectStage::flushForWrite() {
   flushForRead();
   // The write is symbolic offset and might overwrite any byte
   knownSymbolics->reset(nullptr);
+  if (concreteStore) {
+    for (size_t i = 0; i < concreteStore->size(); ++i) {
+      concreteStore->unsetConcrete(i);
+    }
+  }
 }
 
 /***/
 
 ref<Expr> ObjectStage::readWidth(unsigned offset) const {
-  if (auto byte = knownSymbolics->load(offset)) {
+  if (concreteStore && offset < concreteStore->size() &&
+      concreteStore->isConcrete(offset)) {
+    return ConstantExpr::create(concreteStore->readValue(offset), width);
+  } else if (auto byte = knownSymbolics->load(offset)) {
     return byte;
   } else {
     assert(!unflushedMask->load(offset) &&
@@ -623,6 +682,18 @@ ref<Expr> ObjectStage::readWidth(ref<Expr> offset) const {
 }
 
 void ObjectStage::writeWidth(unsigned offset, uint64_t value) {
+
+  if (concreteStore && offset < concreteStore->size()) {
+    if (concreteStore->isConcrete(offset) &&
+        concreteStore->readValue(offset) == value) {
+      return;
+    }
+    concreteStore->writeValue(offset, value);
+    concreteStore->setConcrete(offset);
+    unflushedMask->store(offset, true);
+    return;
+  }
+
   auto byte = knownSymbolics->load(offset);
   if (byte) {
     auto ce = dyn_cast<ConstantExpr>(byte);
@@ -639,6 +710,11 @@ void ObjectStage::writeWidth(unsigned offset, ref<Expr> value) {
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
     writeWidth(offset, CE->getZExtValue(width));
   } else {
+    if (concreteStore && offset < concreteStore->size() &&
+        concreteStore->isConcrete(offset)) {
+      concreteStore->unsetConcrete(offset);
+      unflushedMask->store(offset, true);
+    }
     auto byte = knownSymbolics->load(offset);
     if (byte && byte == value) {
       return;
@@ -654,7 +730,23 @@ void ObjectStage::writeWidth(ref<Expr> offset, ref<Expr> value) {
 
   if (knownSymbolics->defaultV() && knownSymbolics->defaultV() == value &&
       knownSymbolics->storage().size() == 0 && updates.getSize() == 0) {
-    return;
+    if (concreteStore) {
+      if (auto ce = cast<ConstantExpr>(value)) {
+        auto ok = true;
+        for (size_t i = 0; i < concreteStore->size(); ++i) {
+          if (concreteStore->isConcrete(i) &&
+              concreteStore->readValue(i) != ce->getZExtValue()) {
+            ok = false;
+            break;
+          }
+        }
+        if (ok) {
+          return;
+        }
+      }
+    } else {
+      return;
+    }
   }
 
   flushForWrite();
@@ -665,23 +757,44 @@ void ObjectStage::writeWidth(ref<Expr> offset, ref<Expr> value) {
 void ObjectStage::write(const ObjectStage &os) {
   auto constSize = dyn_cast<ConstantExpr>(size);
   auto osConstSize = dyn_cast<ConstantExpr>(os.size);
-  if (constSize || osConstSize) {
-    size_t bound = 0;
-    if (osConstSize && constSize) {
-      bound = std::min(constSize->getZExtValue(), osConstSize->getZExtValue());
-    } else if (constSize) {
-      bound = constSize->getZExtValue();
+
+  assert(width == os.width);
+
+  if (constSize) {
+    if (osConstSize) {
+      size_t bound =
+          std::min(constSize->getZExtValue(), osConstSize->getZExtValue());
+      concreteStore.emplace(ConcreteStore(width, constSize->getZExtValue()));
+      for (size_t i = 0; i < bound; ++i) {
+        concreteStore->writeValue(i, os.concreteStore->readValue(i));
+        concreteStore->setConcrete(i);
+        knownSymbolics->store(i, os.knownSymbolics->load(i));
+        unflushedMask->store(i, os.unflushedMask->load(i));
+      }
     } else {
-      bound = osConstSize->getZExtValue();
-    }
-    for (size_t i = 0; i < bound; ++i) {
-      knownSymbolics->store(i, os.knownSymbolics->load(i));
-      unflushedMask->store(i, os.unflushedMask->load(i));
+      for (size_t i = 0; i < constSize->getZExtValue(); ++i) {
+        knownSymbolics->store(i, os.knownSymbolics->load(i));
+        unflushedMask->store(i, os.unflushedMask->load(i));
+      }
+      concreteStore.emplace(ConcreteStore(width, constSize->getZExtValue()));
     }
   } else {
-    knownSymbolics.reset(os.knownSymbolics->clone());
-    unflushedMask.reset(os.unflushedMask->clone());
+    if (osConstSize) {
+      for (size_t i = 0; i < osConstSize->getZExtValue(); ++i) {
+        if (os.concreteStore->isConcrete(i)) {
+          knownSymbolics->store(
+              i, ConstantExpr::create(os.concreteStore->readValue(i), width));
+        } else {
+          knownSymbolics->store(i, os.knownSymbolics->load(i));
+        }
+        unflushedMask->store(i, os.unflushedMask->load(i));
+      }
+    } else {
+      knownSymbolics.reset(os.knownSymbolics->clone());
+      unflushedMask.reset(os.unflushedMask->clone());
+    }
   }
+
   updates = UpdateList(updates.root, os.updates.head);
 }
 
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 2923bd5d53..f6e90ca48b 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -19,6 +19,7 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/SourceBuilder.h"
 
+#include <cassert>
 #include <cstddef>
 #include <cstdint>
 #include <memory>
@@ -210,6 +211,99 @@ class MemoryObject {
   bool equals(const MemoryObject &b) const { return compare(b) == 0; }
 };
 
+class ConcreteStore {
+  const Expr::Width width;
+  const size_t byteWidth = width / 8;
+  using bytes_ty = std::vector<uint8_t>;
+
+private:
+  std::vector<uint8_t> store;
+  std::vector<bool> mask;
+
+  size_t size_;
+  size_t set_;
+
+public:
+  // Mask is unset
+  ConcreteStore(Expr::Width width, size_t size)
+      : width(width), store(size * byteWidth, 0), mask(size, false),
+        size_(size), set_(0) {}
+
+  // Mask is set
+  ConcreteStore(Expr::Width width, size_t size, bytes_ty initialValue)
+      : width(width), store(size * byteWidth, 0), mask(size, true), size_(size),
+        set_(size) {
+    assert(initialValue.size() == byteWidth);
+    for (size_t i = 0; i < size; ++i) {
+      for (size_t j = 0; j < byteWidth; ++j) {
+        store[(i * byteWidth) + j] = initialValue[j];
+      }
+    }
+  }
+
+  bool writeBytes(size_t offset, bytes_ty value) {
+    assert(value.size() == byteWidth);
+    bool changed = false;
+    for (size_t i = 0; i < byteWidth; ++i) {
+      changed = changed || (store[(offset * byteWidth) + i] != value[i]);
+      store[(offset * byteWidth) + i] = value[i];
+    }
+    return changed;
+  }
+
+  bytes_ty readBytes(size_t offset) const {
+    bytes_ty value(byteWidth, 0);
+    for (size_t i = 0; i < byteWidth; ++i) {
+      value[i] = store[(offset * byteWidth) + i];
+    }
+    return value;
+  }
+
+  bool writeValue(size_t offset, uint64_t value) {
+    assert(byteWidth <= 8);
+    bytes_ty bytes(byteWidth, 0);
+    uint8_t *rawData = (uint8_t *)&value;
+    for (size_t i = 0; i < byteWidth; ++i) {
+      bytes[i] = rawData[i];
+    }
+    return writeBytes(offset, bytes);
+  }
+
+  uint64_t readValue(size_t offset) const {
+    assert(byteWidth <= 8);
+    uint64_t value = 0;
+    uint8_t *rawData = (uint8_t *)&value;
+    auto bytes = readBytes(offset);
+    for (size_t i = 0; i < byteWidth; ++i) {
+      rawData[i] = bytes[i];
+    }
+    return value;
+  }
+
+  bool isConcrete(size_t offset) const { return mask[offset]; }
+
+  void setConcrete(size_t offset) {
+    if (!mask[offset]) {
+      mask[offset] = true;
+      set_ += 1;
+    }
+  }
+
+  void unsetConcrete(size_t offset) {
+    if (mask[offset]) {
+      mask[offset] = false;
+      set_ -= 1;
+    }
+  }
+
+  const uint8_t *data() const { return store.data(); }
+  uint8_t *data() { return store.data(); }
+
+  size_t size() const { return size_; }
+
+  size_t set() const { return set_; }
+};
+
 class ObjectStage {
 private:
   using storage_ty = SparseStorage<ref<Expr>, OptionalRefEq<Expr>>;
@@ -218,6 +312,10 @@ class ObjectStage {
   /// if byte is known
   mutable std::unique_ptr<storage_ty> knownSymbolics;
 
+public:
+  std::optional<ConcreteStore> concreteStore;
+
+private:
   /// unflushedMask[byte] is set if byte is unflushed
   /// mutable because may need flushed during read of const
   mutable std::unique_ptr<bool_storage_ty> unflushedMask;
@@ -255,11 +353,11 @@ class ObjectStage {
   }
   void initializeToZero();
 
+  void flushToConcreteStore(Assignment &assignment);
+
 private:
   const UpdateList &getUpdates() const;
 
-  void makeConcrete();
-
   void flushForRead() const;
   void flushForWrite();
 };
@@ -329,6 +427,8 @@ class ObjectState {
   void write64(unsigned offset, uint64_t value);
   void print() const;
 
+  void flushToConcreteStore(Assignment &assignment);
+
 private:
   ref<Expr> read8(ref<Expr> offset) const;
   ref<Expr> readValue8(ref<Expr> offset) const;