Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.

1 files changed, 1 insertions, 6 deletions

diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index e2937ccb2..db02ce207 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -14,7 +14,6 @@
  ** Black box testing of CVC4::BooleanSimplification.
  **/
 
-#include "context/context.h"
 #include "util/language.h"
 #include "expr/node.h"
 #include "expr/kind.h"
@@ -26,12 +25,10 @@
 #include <set>
 
 using namespace CVC4;
-using namespace CVC4::context;
 using namespace std;
 
 class BooleanSimplificationBlack : public CxxTest::TestSuite {
 
-  Context* d_context;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
@@ -70,8 +67,7 @@ class BooleanSimplificationBlack : public CxxTest::TestSuite {
 public:
 
   void setUp() {
-    d_context = new Context();
-    d_nm = new NodeManager(d_context, NULL);
+    d_nm = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     a = d_nm->mkSkolem("a", d_nm->booleanType());
@@ -116,7 +112,6 @@ public:
 
     delete d_scope;
     delete d_nm;
-    delete d_context;
   }
 
   void testNegate() {