From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 14 Mar 2010 01:55:36 +0000 (+0000)
Subject: * test/unit/context/context_black.h: added a test for Clark's fix to bug #45.
X-Git-Tag: cvc5-1.0.0~9177
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb21cdc3a551fa46b5e77345bb5cbcb55cba2fa6;p=cvc5.git

* 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 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;
   }
 };