1 files changed, 27 insertions, 0 deletions
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 2b781b95c..66d6a6542 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -296,6 +296,10 @@ ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
   d_pScope->addToChain(this);
 }
 
+void ContextObj::enqueueToGarbageCollect() {
+  Assert(d_pScope != NULL);
+  d_pScope->enqueueToGarbageCollect(this);
+}
 
 ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
   if(preNotify) {
@@ -354,6 +358,29 @@ std::ostream& operator<<(std::ostream& out,
   return out << " --> NULL";
 }
 
+Scope::~Scope() {
+  // Call restore() method on each ContextObj object in the list.
+  // Note that it is the responsibility of restore() to return the
+  // next item in the list.
+  while (d_pContextObjList != NULL) {
+    d_pContextObjList = d_pContextObjList->restoreAndContinue();
+  }
+
+  if (d_garbage) {
+    while (!d_garbage->empty()) {
+      ContextObj* obj = d_garbage->back();
+      d_garbage->pop_back();
+      obj->deleteSelf();
+    }
+  }
+}
+
+void Scope::enqueueToGarbageCollect(ContextObj* obj) {
+  if (!d_garbage) {
+    d_garbage.reset(new std::vector<ContextObj*>);
+  }
+  d_garbage->push_back(obj);
+}
 
 } /* CVC4::context namespace */
 } /* CVC4 namespace */