5 files changed, 299 insertions, 62 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index d4de88daf..75f6eb2ae 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -71,6 +71,7 @@ class CDOmap : public ContextObj {
       }
       d_next->d_prev = d_prev;
       d_prev->d_next = d_next;
+      Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
       d_map->d_trash.push_back(this);
     } else {
       d_data = p->d_data;
@@ -155,7 +156,7 @@ public:
 
   CDMapData(Context* context) : ContextObj(context) {}
   CDMapData(const ContextObj& co) : ContextObj(co) {}
-  ~CDMapData() { destroy(); }
+  ~CDMapData() throw(AssertionException) { destroy(); }
 };
 
 /**
@@ -192,7 +193,7 @@ class CDMap : public ContextObj {
         i != d_trash.end();
         ++i) {
       Debug("gc") << "emptyTrash(): " << *i << std::endl;
-      //(*i)->deleteSelf();
+      (*i)->deleteSelf();
     }
     d_trash.clear();
   }
@@ -201,21 +202,26 @@ public:
 
   CDMap(Context* context) :
     ContextObj(context),
+    d_map(),
     d_first(NULL),
     d_context(context),
     d_trash() {
   }
 
   ~CDMap() throw(AssertionException) {
+    Debug("gc") << "cdmap " << this
+                << " disappearing, destroying..." << std::endl;
     destroy();
+    Debug("gc") << "cdmap " << this
+                << " disappearing, done destroying" << std::endl;
     for(typename table_type::iterator i = d_map.begin();
         i != d_map.end();
         ++i) {
       (*i).second->deleteSelf();
     }
-    //d_map.clear();
-    Debug("gc") << "cdmap gone, emptying trash" << std::endl;
+    Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl;
     emptyTrash();
+    Debug("gc") << "done emptying trash for " << this << std::endl;
   }
 
   // The usual operators of map
diff --git a/src/context/cdo.h b/src/context/cdo.h
index e03156e8a..ead43b2e8 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -66,11 +66,26 @@ class CDO : public ContextObj {
   CDO<T>& operator=(const CDO<T>& cdo);
 
 public:
+
   /**
    * Main constructor - uses default constructor for T to create the initial
    * value of d_data.
    */
-  CDO(Context* context) : ContextObj(context) {}
+  CDO(Context* context) :
+    ContextObj(context) {
+  }
+
+  /**
+   * Main constructor - uses default constructor for T to create the
+   * initial value of d_data.
+   *
+   * This version takes an argument that specifies whether this CDO<>
+   * was itself allocated in context memory.  If it was, it is linked
+   * with the current scope rather than scope 0.
+   */
+  CDO(bool allocatedInCMM, Context* context) :
+    ContextObj(allocatedInCMM, context) {
+  }
 
   /**
    * Constructor from object of type T.  Creates a ContextObj and sets the data
@@ -78,7 +93,24 @@ public:
    * current Scope.  If the Scope is popped, the value will revert to whatever
    * is assigned by the default constructor for T
    */
-  CDO(Context* context, const T& data) : ContextObj(context) {
+  CDO(Context* context, const T& data) :
+    ContextObj(context) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Constructor from object of type T.  Creates a ContextObj and sets the data
+   * to the given data value.  Note that this value is only valid in the
+   * current Scope.  If the Scope is popped, the value will revert to whatever
+   * is assigned by the default constructor for T.
+   *
+   * This version takes an argument that specifies whether this CDO<>
+   * was itself allocated in context memory.  If it was, it is linked
+   * with the current scope rather than scope 0.
+   */
+  CDO(bool allocatedInCMM, Context* context, const T& data) :
+    ContextObj(allocatedInCMM, context) {
     makeCurrent();
     d_data = data;
   }
@@ -86,7 +118,7 @@ public:
   /**
    * Destructor - call destroy() method
    */
-  ~CDO() throw() { destroy(); }
+  ~CDO() throw(AssertionException) { destroy(); }
 
   /**
    * Set the data in the CDO.  First call makeCurrent.
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 05024430c..d371dc39a 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -10,9 +10,13 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Implementation of base context operations.
  **/
 
 
+#include <iostream>
+#include <vector>
+
 #include "context/context.h"
 #include "util/Assert.h"
 
@@ -54,7 +58,7 @@ Context::~Context() throw(AssertionException) {
 
 
 void Context::push() {
-  // FIXME: TRACE("pushpop", indentStr, "Push", " {");
+  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push {" << std::endl;
 
   // Create a new memory region
   d_pCMM->push();
@@ -93,7 +97,7 @@ void Context::pop() {
     pCNO = pCNO->d_pCNOnext;
   }
 
-  //FIXME:  TRACE("pushpop", indentStr, "}", " Pop");
+  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop" << std::endl;
 }
 
 
@@ -124,16 +128,47 @@ void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
 }
 
 
-void ContextObj::update() {
+void ContextObj::update() throw(AssertionException) {
+  Debug("context") << "before update(" << this << "):" << std::endl
+                   << *getContext() << std::endl;
+
   // Call save() to save the information in the current object
   ContextObj* pContextObjSaved = save(d_pScope->getCMM());
 
+  Debug("context") << "in update(" << this << ") with restore "
+                   << pContextObjSaved << ": waypoint 1" << std::endl
+                   << *getContext() << std::endl;
+
   // Check that base class data was saved
-  Assert(pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
-         pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev &&
-         pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore &&
-         pContextObjSaved->d_pScope == d_pScope,
-         "save() did not properly copy information in base class");
+  Assert( ( pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
+            pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev &&
+            pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore &&
+            pContextObjSaved->d_pScope == d_pScope ),
+          "save() did not properly copy information in base class" );
+
+  // Link the "saved" object in place of this ContextObj in the scope
+  // we're moving it FROM.
+  Debug("context") << "in update(" << this
+                   << "): next() == " << next() << std::endl;
+  if(next() != NULL) {
+    Debug("context") << "in update(" << this
+                     << "): next()->prev() == " << next()->prev() << std::endl;
+    next()->prev() = &pContextObjSaved->next();
+    Debug("context") << "in update(" << this
+                     << "): next()->prev() is now "
+                     << next()->prev() << std::endl;
+  }
+  Debug("context") << "in update(" << this
+                   << "): prev() == " << prev() << std::endl;
+  Debug("context") << "in update(" << this
+                   << "): *prev() == " << *prev() << std::endl;
+  *prev() = pContextObjSaved;
+  Debug("context") << "in update(" << this
+                   << "): *prev() is now " << *prev() << std::endl;
+
+  Debug("context") << "in update(" << this << ") with restore "
+                   << pContextObjSaved << ": waypoint 3" << std::endl
+                   << *getContext() << std::endl;
 
   // Update Scope pointer to current top Scope
   d_pScope = d_pScope->getContext()->getTopScope();
@@ -144,18 +179,27 @@ void ContextObj::update() {
   // Insert object into the list of objects that need to be restored when this
   // Scope is popped.
   d_pScope->addToChain(this);
+
+  Debug("context") << "after update(" << this << ") with restore "
+                   << pContextObjSaved << ":" << std::endl
+                   << *getContext() << std::endl;
 }
 
 
-ContextObj* ContextObj::restoreAndContinue() {
+ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) {
   // Variable to hold next object in list
   ContextObj* pContextObjNext;
 
   // Check the restore pointer.  If NULL, this must be the bottom Scope
   if(d_pContextObjRestore == NULL) {
-    Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
-           "Expected bottom scope");
+    // might not be bottom scope, since objects allocated in context
+    // memory don't get linked to scope 0
+    //
+    // Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
+    //        "Expected bottom scope");
+
     pContextObjNext = d_pContextObjNext;
+
     // Nothing else to do
   } else {
     // Call restore to update the subclass data
@@ -169,13 +213,23 @@ ContextObj* ContextObj::restoreAndContinue() {
     next() = d_pContextObjRestore->d_pContextObjNext;
     prev() = d_pContextObjRestore->d_ppContextObjPrev;
     d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
+
+    // Re-link this ContextObj to the list in this scope
+    if(next() != NULL) {
+      next()->prev() = &next();
+    }
+    *prev() = this;
   }
+
   // Return the next object in the list
   return pContextObjNext;
 }
 
 
 void ContextObj::destroy() throw(AssertionException) {
+  Debug("context") << "before destroy " << this
+                   << " (level " << getLevel() << "):" << std::endl
+                   << *getContext() << std::endl;
   for(;;) {
     // If valgrind reports invalid writes on the next few lines,
     // here's a hint: make sure all classes derived from ContextObj in
@@ -184,12 +238,18 @@ void ContextObj::destroy() throw(AssertionException) {
     if(next() != NULL) {
       next()->prev() = prev();
     }
-    *(prev()) = next();
+    *prev() = next();
     if(d_pContextObjRestore == NULL) {
       break;
     }
+    Debug("context") << "in destroy " << this << ", restore object is "
+                     << d_pContextObjRestore << " at level "
+                     << d_pContextObjRestore->getLevel() << ":" << std::endl
+                     << *getContext() << std::endl;
     restoreAndContinue();
   }
+  Debug("context") << "after destroy " << this << ":" << std::endl
+                   << *getContext() << std::endl;
 }
 
 
@@ -198,11 +258,27 @@ ContextObj::ContextObj(Context* pContext) :
 
   Assert(pContext != NULL, "NULL context pointer");
 
+  Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
   d_pScope = pContext->getBottomScope();
   d_pScope->addToChain(this);
 }
 
 
+ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
+  d_pContextObjRestore(NULL) {
+
+  Assert(pContext != NULL, "NULL context pointer");
+
+  Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
+  if(allocatedInCMM) {
+    d_pScope = pContext->getTopScope();
+  } else {
+    d_pScope = pContext->getBottomScope();
+  }
+  d_pScope->addToChain(this);
+}
+
+
 ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
   if(preNotify) {
     pContext->addNotifyObjPre(this);
@@ -217,8 +293,44 @@ ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
     d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
   }
   if(d_ppCNOprev != NULL) {
-    *(d_ppCNOprev) = d_pCNOnext;
+    *d_ppCNOprev = d_pCNOnext;
+  }
+}
+
+
+std::ostream& operator<<(std::ostream& out,
+                         const Context& context) throw(AssertionException) {
+  const std::string separator(79, '-');
+
+  int level = context.d_scopeList.size() - 1;
+  typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
+  for(const_reverse_iterator i = context.d_scopeList.rbegin();
+      i != context.d_scopeList.rend();
+      ++i, --level) {
+    Scope* pScope = *i;
+    Assert(pScope->getLevel() == level);
+    Assert(pScope->getContext() == &context);
+    out << separator << std::endl
+        << *pScope << std::endl;
+  }
+  return out << separator << std::endl;
+}
+
+
+std::ostream& operator<<(std::ostream& out,
+                         const Scope& scope) throw(AssertionException) {
+  out << "Scope " << scope.d_level << ":";
+  ContextObj* pContextObj = scope.d_pContextObjList;
+  Assert(pContextObj == NULL ||
+         pContextObj->prev() == &scope.d_pContextObjList);
+  while(pContextObj != NULL) {
+    out << " <--> " << pContextObj;
+    Assert(pContextObj->d_pScope == &scope);
+    Assert(pContextObj->next() == NULL ||
+           pContextObj->next()->prev() == &pContextObj->next());
+    pContextObj = pContextObj->next();
   }
+  return out << " --> NULL";
 }
 
 
diff --git a/src/context/context.h b/src/context/context.h
index 0e2a9107f..ff650ce5d 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -18,13 +18,15 @@
 #ifndef __CVC4__CONTEXT__CONTEXT_H
 #define __CVC4__CONTEXT__CONTEXT_H
 
-#include "context/context_mm.h"
-#include "util/Assert.h"
-
+#include <iostream>
 #include <cstdlib>
 #include <cstring>
+#include <vector>
 #include <new>
 
+#include "context/context_mm.h"
+#include "util/Assert.h"
+
 namespace CVC4 {
 namespace context {
 
@@ -33,6 +35,14 @@ class Scope;
 class ContextObj;
 class ContextNotifyObj;
 
+/** Pretty-printing of Contexts (for debugging) */
+std::ostream&
+operator<<(std::ostream&, const Context&) throw(AssertionException);
+
+/** Pretty-printing of Scopes (for debugging) */
+std::ostream&
+operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
 /**
  * A Context encapsulates all of the dynamic state of the system.  Its main
  * methods are push() and pop().  A call to push() saves the current state,
@@ -78,6 +88,9 @@ class Context {
    */
   ContextNotifyObj* d_pCNOpost;
 
+  friend std::ostream&
+  operator<<(std::ostream&, const Context&) throw(AssertionException);
+
 public:
   /**
    * Constructor: create ContextMemoryManager and initial Scope
@@ -102,7 +115,7 @@ public:
   /**
    * Return the current Scope level.
    */
-  int getLevel() const { return ((int)d_scopeList.size()) - 1; }
+  int getLevel() const { return d_scopeList.size() - 1; }
 
   /**
    * Return the ContextMemoryManager associated with the context.
@@ -176,13 +189,16 @@ class Scope {
    */
   ContextObj* d_pContextObjList;
 
+  friend std::ostream&
+  operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
 public:
 
   /**
    * Constructor: Create a new Scope; set the level and the previous Scope
    * if any.
    */
-  Scope(Context* pContext, ContextMemoryManager* pCMM, int level) :
+  Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() :
     d_pContext(pContext),
     d_pCMM(pCMM),
     d_level(level),
@@ -193,38 +209,38 @@ public:
    * Destructor: Restore all of the objects in ContextObjList.  Defined inline
    * below.
    */
-  ~Scope() throw();
+  ~Scope() throw(AssertionException);
 
   /**
    * Get the Context for this Scope
    */
-  Context* getContext() const { return d_pContext; }
+  Context* getContext() const throw() { return d_pContext; }
 
   /**
    * Get the ContextMemoryManager for this Scope
    */
-  ContextMemoryManager* getCMM() const { return d_pCMM; }
+  ContextMemoryManager* getCMM() const throw() { return d_pCMM; }
 
   /**
    * Get the level of the current Scope
    */
-  int getLevel() const { return d_level; }
+  int getLevel() const throw() { return d_level; }
 
   /**
    * Return true iff this Scope is the current top Scope
    */
-  bool isCurrent() const { return this == d_pContext->getTopScope(); }
+  bool isCurrent() const throw() { return this == d_pContext->getTopScope(); }
 
   /**
-   * When a ContextObj object is modified for the first time in this Scope, it
-   * should call this method to add itself to the list of objects that will
-   * need to be restored.  Defined inline below.
+   * When a ContextObj object is modified for the first time in this
+   * Scope, it should call this method to add itself to the list of
+   * objects that will need to be restored.  Defined inline below.
    */
-  void addToChain(ContextObj* pContextObj);
+  void addToChain(ContextObj* pContextObj) throw(AssertionException);
 
   /**
-   * Overload operator new for use with ContextMemoryManager to allow creation
-   * of new Scope objects in the current memory region.
+   * Overload operator new for use with ContextMemoryManager to allow
+   * creation of new Scope objects in the current memory region.
    */
   static void* operator new(size_t size, ContextMemoryManager* pCMM) {
     return pCMM->newData(size);
@@ -232,9 +248,10 @@ public:
 
   /**
    * Overload operator delete for Scope objects allocated using
-   * ContextMemoryManager.  No need to do anything because memory is freed
-   * automatically when the ContextMemoryManager pop() method is called.
-   * Include both placement and standard delete for completeness.
+   * ContextMemoryManager.  No need to do anything because memory is
+   * freed automatically when the ContextMemoryManager pop() method is
+   * called.  Include both placement and standard delete for
+   * completeness.
    */
   static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
   static void operator delete(void* pMem) {}
@@ -245,9 +262,9 @@ public:
 };/* class Scope */
 
 /**
- * This is an abstract base class from which all objects that are context-dependent
- * should inherit.  For any data structure that you want to have be
- * automatically backtracked, do the following:
+ * This is an abstract base class from which all objects that are
+ * context-dependent should inherit.  For any data structure that you
+ * want to have be automatically backtracked, do the following:
  * 1. Create a class for the data structure that inherits from ContextObj
  * 2. Implement save()
  *    The role of save() is to create a new ContexObj object that contains
@@ -310,31 +327,34 @@ class ContextObj {
    * does the necessary bookkeeping to ensure that object can be restored to
    * its current state when restore is called.
    */
-  void update();
+  void update() throw(AssertionException);
 
   // The rest of the private methods are for the benefit of the Scope.  We make
   // Scope our friend so it is the only one that can use them.
 
   friend class Scope;
 
+  friend std::ostream&
+  operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
   /**
    * Return reference to next link in ContextObjList.  Used by
    * Scope::addToChain method.
    */
-  ContextObj*& next() { return d_pContextObjNext; }
+  ContextObj*& next() throw() { return d_pContextObjNext; }
 
   /**
    * Return reference to prev link in ContextObjList.  Used by
    * Scope::addToChain method.
    */
-  ContextObj**& prev() { return d_ppContextObjPrev; }
+  ContextObj**& prev() throw() { return d_ppContextObjPrev; }
 
   /**
    * This method is called by Scope during a pop: it does the necessary work to
    * restore the object from its saved copy and then returns the next object in
    * the list that needs to be restored.
    */
-  ContextObj* restoreAndContinue();
+  ContextObj* restoreAndContinue() throw(AssertionException);
 
 protected:
 
@@ -351,14 +371,10 @@ protected:
   virtual void restore(ContextObj* pContextObjRestore) = 0;
 
   /**
-   * This method checks if the object has been modified in this Scope yet.  If
-   * not, it calls update().
+   * This method checks if the object has been modified in this Scope
+   * yet.  If not, it calls update().
    */
-  void makeCurrent() {
-    if(!(d_pScope->isCurrent())) {
-      update();
-    }
-  }
+  inline void makeCurrent() throw(AssertionException);
 
   /**
    * Should be called from sub-class destructor: calls restore until restored
@@ -369,9 +385,59 @@ protected:
    */
   void destroy() throw(AssertionException);
 
+  /////
+  //
+  //  These next four accessors return properties of the Scope to
+  //  derived classes without giving them the Scope object directly.
+  //
+  /////
+
+  /**
+   * Get the Context with which this ContextObj was created.  This is
+   * part of the protected interface, intended for derived classes to
+   * use if necessary.
+   */
+  Context* getContext() const throw() {
+    return d_pScope->getContext();
+  }
+
+  /**
+   * Get the ContextMemoryManager with which this ContextObj was
+   * created.  This is part of the protected interface, intended for
+   * derived classes to use if necessary.  If a ContextObj-derived
+   * class needs to allocate memory somewhere other than the save()
+   * member function (where it is explicitly given a
+   * ContextMemoryManager), it can use this accessor to get the memory
+   * manager.
+   */
+  ContextMemoryManager* getCMM() const throw() {
+    return d_pScope->getCMM();
+  }
+
+  /**
+   * Get the level associated to this ContextObj.  Useful if a
+   * ContextObj-derived class needs to compare the level of its last
+   * update with another ContextObj.
+   */
+  int getLevel() const throw() {
+    return d_pScope->getLevel();
+  }
+
+  /**
+   * Returns true if the object is "current"-- that is, updated in the
+   * topmost contextual scope.  Useful if a ContextObj-derived class
+   * needs to determine if it has been modified in the current scope.
+   * Note that it is always safe to call makeCurrent() without first
+   * checking if the object is current, so this function need not be
+   * used under normal circumstances.
+   */
+  bool isCurrent() const throw() {
+    return d_pScope->isCurrent();
+  }
+
   /**
    * operator new using ContextMemoryManager (common case used by
-   * subclasses during save() ).  No delete is required for memory
+   * subclasses during save()).  No delete is required for memory
    * allocated this way, since it is automatically released when the
    * context is popped.  Also note that allocations using this
    * operator never have their destructor called, so any clean-up has
@@ -402,9 +468,17 @@ public:
   ContextObj(Context* context);
 
   /**
+   * Create a new ContextObj.  This constructor takes an argument that
+   * specifies whether this ContextObj is itself allocated in context
+   * memory.  If it is, it's invalid below the current scope level, so
+   * we don't put it in scope 0.
+   */
+  ContextObj(bool allocatedInCMM, Context* context);
+
+  /**
    * Destructor does nothing: subclass must explicitly call destroy() instead.
    */
-  virtual ~ContextObj() { Debug("contextgc") << "context obj dest" << std::endl; }
+  virtual ~ContextObj() {}
 
   /**
    * If you want to allocate a ContextObj object on the heap, use this
@@ -431,6 +505,7 @@ public:
    * ContextMemoryManager as an argument.
    */
   void deleteSelf() {
+    Debug("context") << "deleteSelf(" << this << ")" << std::endl;
     this->~ContextObj();
     ::operator delete(this);
   }
@@ -475,15 +550,16 @@ class ContextNotifyObj {
    * Return reference to next link in ContextNotifyObj list.  Used by
    * Context::addNotifyObj methods.
    */
-  ContextNotifyObj*& next() { return d_pCNOnext; }
+  ContextNotifyObj*& next() throw() { return d_pCNOnext; }
 
   /**
    * Return reference to prev link in ContextNotifyObj list.  Used by
    * Context::addNotifyObj methods.
    */
-  ContextNotifyObj**& prev() { return d_ppCNOprev; }
+  ContextNotifyObj**& prev() throw() { return d_ppCNOprev; }
 
 public:
+
   /**
    * Constructor for ContextNotifyObj.  Parameters are the context to
    * which this notify object will be added, and a flag which, if
@@ -504,11 +580,16 @@ public:
    * implemented by the subclass.
    */
   virtual void notify() = 0;
+
 };/* class ContextNotifyObj */
 
-// Inline functions whose definitions had to be delayed:
+inline void ContextObj::makeCurrent() throw(AssertionException) {
+  if(!(d_pScope->isCurrent())) {
+    update();
+  }
+}
 
-inline Scope::~Scope() throw() {
+inline Scope::~Scope() throw(AssertionException) {
   // 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.
@@ -517,9 +598,12 @@ inline Scope::~Scope() throw() {
   }
 }
 
-inline void Scope::addToChain(ContextObj* pContextObj) {
-  if(d_pContextObjList != NULL)
-    d_pContextObjList->prev() = &(pContextObj->next());
+inline void
+Scope::addToChain(ContextObj* pContextObj) throw(AssertionException) {
+  if(d_pContextObjList != NULL) {
+    d_pContextObjList->prev() = &pContextObj->next();
+  }
+
   pContextObj->next() = d_pContextObjList;
   pContextObj->prev() = &d_pContextObjList;
   d_pContextObjList = pContextObj;
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index ab81c7486..b0b015681 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -85,6 +85,9 @@ void* ContextMemoryManager::newData(size_t size) {
     AlwaysAssert(d_nextFree <= d_endChunk,
                  "Request is bigger than memory chunk size");
   }
+  Debug("context") << "ContextMemoryManager::newData(" << size
+                   << ") returning " << res << " at level "
+                   << d_chunkList.size() << std::endl;
   return res;
 }