* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"

  data into a CDMap.  Such a key doesn't disappear from the map on pop,
  but rather returns to its "initializing" state, set by
  insertAtContextLevelZero().  This can be used for lazy assignment,
  among other things, and has been added to support some exploratory
  coding by Tim in arithmetic.

* Made internal CDOmap<> copy constructor private (it should always have
  been).  This is necessary to avoid CxxTest (or others) doing nasty
  generic programming things that cause context invariants to be broken.

* Added unit testing for this feature, and in general beef up the unit
  testing for CDMap<>.

* src/expr/node_manager.cpp: Better output for unhandled cases in getType().

1 files changed, 519 insertions, 2 deletions

diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 93316da76..b4370e93c 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -32,7 +32,7 @@ public:
 
   void setUp() {
     d_context = new Context;
-    //Debug.on("cdmap");
+    //Debug.on("context");
     //Debug.on("gc");
     //Debug.on("pushpop");
   }
@@ -44,12 +44,20 @@ public:
   void testSimpleSequence() {
     CDMap<int, int> map(d_context);
 
+    TS_ASSERT(map.find(3) == map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+
     map.insert(3, 4);
 
     TS_ASSERT(map.find(3) != map.end());
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
 
     {
       d_context->push();
@@ -58,6 +66,8 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) == map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
 
       map.insert(5, 6);
       map.insert(9, 8);
@@ -66,6 +76,10 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       {
         d_context->push();
@@ -74,6 +88,10 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
         map.insert(1, 2);
 
@@ -81,6 +99,11 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         {
           d_context->push();
@@ -89,13 +112,38 @@ public:
           TS_ASSERT(map.find(5) != map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) == map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
 
+          map.insertAtContextLevelZero(23, 317);
           map.insert(1, 45);
 
           TS_ASSERT(map.find(3) != map.end());
           TS_ASSERT(map.find(5) != map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 45);
+          TS_ASSERT(map[23] == 317);
+
+          map.insert(23, 324);
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 45);
+          TS_ASSERT(map[23] == 324);
 
           d_context->pop();
         }
@@ -104,6 +152,12 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
 
         d_context->pop();
       }
@@ -112,6 +166,11 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) != map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(map[23] == 317);
 
       d_context->pop();
     }
@@ -120,6 +179,9 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) != map.end());
+    TS_ASSERT(map[3] == 4);
+    TS_ASSERT(map[23] == 317);
   }
 
   // no intervening find() in this one
@@ -144,6 +206,10 @@ public:
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(7) == map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[5] == 6);
 
         {
           d_context->push();
@@ -167,6 +233,8 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
 
     {
       d_context->push();
@@ -175,6 +243,8 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) == map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
 
       map.insert(5, 6);
       map.insert(9, 8);
@@ -183,6 +253,10 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       {
         d_context->push();
@@ -191,13 +265,24 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
+        map.insertAtContextLevelZero(23, 317);
         map.insert(1, 2);
 
         TS_ASSERT(map.find(3) != map.end());
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
 
         map.obliterate(5);
 
@@ -205,6 +290,11 @@ public:
         TS_ASSERT(map.find(5) == map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
 
         {
           d_context->push();
@@ -213,6 +303,11 @@ public:
           TS_ASSERT(map.find(5) == map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 317);
 
           d_context->pop();
         }
@@ -221,6 +316,22 @@ public:
         TS_ASSERT(map.find(5) == map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
+
+        map.obliterate(23);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) == map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         d_context->pop();
       }
@@ -229,6 +340,9 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[9] == 8);
 
       d_context->pop();
     }
@@ -237,6 +351,8 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
   }
 
   void testObliteratePrimordial() {
@@ -248,6 +364,7 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map[3] == 4);
 
     {
       d_context->push();
@@ -256,6 +373,7 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) == map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
 
       map.insert(5, 6);
       map.insert(9, 8);
@@ -264,6 +382,9 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       {
         d_context->push();
@@ -272,13 +393,19 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
-
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
         map.insert(1, 2);
 
         TS_ASSERT(map.find(3) != map.end());
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         map.obliterate(3);
 
@@ -286,6 +413,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         {
           d_context->push();
@@ -294,6 +424,9 @@ public:
           TS_ASSERT(map.find(5) != map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
 
           d_context->pop();
         }
@@ -302,6 +435,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         d_context->pop();
       }
@@ -310,6 +446,8 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       d_context->pop();
     }
@@ -329,6 +467,7 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map[3] == 4);
 
     {
       d_context->push();
@@ -337,6 +476,7 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) == map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
 
       map.insert(5, 6);
       map.insert(9, 8);
@@ -345,6 +485,9 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       {
         d_context->push();
@@ -353,6 +496,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
         map.insert(1, 2);
 
@@ -360,6 +506,10 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         map.obliterate(1);
 
@@ -367,6 +517,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
         {
           d_context->push();
@@ -375,6 +528,9 @@ public:
           TS_ASSERT(map.find(5) != map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) == map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
 
           d_context->pop();
         }
@@ -383,6 +539,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
         d_context->pop();
       }
@@ -391,6 +550,362 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map[3] == 4);
+  }
+
+  void testInsertAtContextLevelZero() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+
+        map.insertAtContextLevelZero(23, 317);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
+
+        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
+                         AssertionException);
+        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472),
+                         AssertionException);
+        map.insert(23, 472);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 472);
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 472);
+
+          TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                           AssertionException);
+          map.insert(23, 1024);
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 1024);
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        std::cout << "map[23] is " << map[23] << std::endl;
+        TS_ASSERT(map[23] == 472);
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) != map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(map[23] == 317);
+
+      TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                       AssertionException);
+      map.insert(23, 477);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) != map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(map[23] == 477);
+
+      d_context->pop();
+    }
+
+    TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                     AssertionException);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) != map.end());
+    TS_ASSERT(map[3] == 4);
+    TS_ASSERT(map[23] == 317);
+  }
+
+  void testObliterateInsertedAtContextLevelZero() {
+    cout << "\nobliteratCL0\n";
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+
+        map.insertAtContextLevelZero(23, 317);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
+
+        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
+                         AssertionException);
+        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472),
+                         AssertionException);
+        map.insert(23, 472);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 472);
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 472);
+
+          TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                           AssertionException);
+          map.insert(23, 1024);
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 1024);
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 472);
+
+        map.obliterate(23);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+
+      // reinsert as a normal map entry
+      map.insert(23, 477);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) != map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(map[23] == 477);
 
       d_context->pop();
     }
@@ -399,5 +914,7 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
   }
 };