* test/unit/context/context_black.h: added a test for Clark's fix to bug #45.

* test/unit/context/cdlist_black.h: comment fix

diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 560c70722937278d6ba607342589a2065aa78997..6029c7ff0eb6c47c61cb4de612ef5501ea0d22c9 100644 (file)
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -35,7 +35,7 @@ public:
   }
 
   // test at different sizes.  this triggers grow() behavior differently.
-  // grow() is completely broken in revision 256; fix forthcoming by Tim
+  // grow() was completely broken in revision 256
   void testCDList10() { listTest(10); }
   void testCDList15() { listTest(15); }
   void testCDList20() { listTest(20); }

diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 548b28d6492bbc52dc65868971f76d1c9cedef32..c9b47e40051bc3464d78ad4c55b7189cc80426b6 100644 (file)
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -37,6 +37,10 @@ public:
     d_context = new Context;
   }
 
+  void tearDown() {
+    delete d_context;
+  }
+
   void testIntCDO() {
     // Test that push/pop maintains the original value
     CDO<int> a1(d_context);
@@ -62,7 +66,12 @@ public:
 #endif /* CVC4_ASSERTIONS */
   }
 
-  void tearDown() {
-    delete d_context;
+  void testDtor() {
+    // Destruction of ContextObj was broken in revision 324 (bug #45) when
+    // at a higher context level with an intervening modification.
+    // (The following caused a "pure virtual method called" error.)
+    CDO<int> i(d_context);
+    d_context->push();
+    i = 5;
   }
 };