From bb21cdc3a551fa46b5e77345bb5cbcb55cba2fa6 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 14 Mar 2010 01:55:36 +0000
Subject: [PATCH] * test/unit/context/context_black.h: added a test for Clark's
 fix to bug #45. * test/unit/context/cdlist_black.h: comment fix

---
 test/unit/context/cdlist_black.h  |  2 +-
 test/unit/context/context_black.h | 13 +++++++++++--
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 560c70722..6029c7ff0 100644
--- 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 548b28d64..c9b47e400 100644
--- 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;
   }
 };
-- 
2.30.2