unit test fixes for new NodeManager constructor (related to previous two trunk commits)

19 files changed, 27 insertions, 27 deletions

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 06c8decfc..a324bbbf1 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -45,7 +45,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nodeManager = new NodeManager(d_ctxt);
+    d_nodeManager = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
   }
 
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 448933622..571be2789 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -70,7 +70,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     d_booleanType = new TypeNode(d_nm->booleanType());
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 5389e1308..6bd5aa1fd 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -46,7 +46,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nodeManager = new NodeManager(d_ctxt);
+    d_nodeManager = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
     d_realType = new TypeNode(d_nodeManager->realType());
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 49c9b7952..320d4ddbe 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -50,7 +50,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     specKind = AND;
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index af79f5ff2..e6ebc6724 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -42,7 +42,7 @@ public:
 
   void setUp() {
     d_context = new Context;
-    d_nodeManager = new NodeManager(d_context);
+    d_nodeManager = new NodeManager(d_context, NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
   }
 
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 62fdeb45b..95d3271f2 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -40,7 +40,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context();
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
   }
 
diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index 4e7c198ee..e97407dfc 100644
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -43,7 +43,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nodeManager = new NodeManager(d_ctxt);
+    d_nodeManager = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
     d_realType = new TypeNode(d_nodeManager->realType());
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 74413796a..9d6311acb 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -43,7 +43,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context();
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
   }
 
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 2e1a6d3f4..af9b7bd0f 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -67,7 +67,7 @@ protected:
 //        cerr << "Testing good input: <<" << goodInput << ">>" << endl;
 //        istringstream stream(goodInputs[i]);
         Parser *parser =
-          ParserBuilder(*d_exprManager,"test")
+          ParserBuilder(d_exprManager,"test")
             .withStringInput(goodInput)
             .withInputLanguage(d_lang)
             .build();
@@ -94,7 +94,7 @@ protected:
 //      Debug.on("parser");
 
     Parser *parser =
-      ParserBuilder(*d_exprManager,"test")
+      ParserBuilder(d_exprManager,"test")
         .withStringInput(badInput)
         .withInputLanguage(d_lang)
         .withStrictMode(strictMode)
@@ -116,7 +116,7 @@ protected:
 //        istringstream stream(context + goodBooleanExprs[i]);
 
         Parser *parser =
-          ParserBuilder(*d_exprManager,"test")
+          ParserBuilder(d_exprManager,"test")
             .withStringInput(goodExpr)
             .withInputLanguage(d_lang)
             .build();
@@ -153,7 +153,7 @@ protected:
 //      cout << "Testing bad expr: '" << badExpr << "'\n";
 
       Parser *parser =
-        ParserBuilder(*d_exprManager,"test")
+        ParserBuilder(d_exprManager,"test")
           .withStringInput(badExpr)
           .withInputLanguage(d_lang)
           .withStrictMode(strictMode)
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 06259ddb0..06b09f2ce 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -92,7 +92,7 @@ public:
     /* fs.close(); */
 
     checkEmptyInput(
-      ParserBuilder(*d_exprManager,filename)
+      ParserBuilder(d_exprManager,filename)
         .withInputLanguage(LANG_CVC4)
                     );
 
@@ -108,7 +108,7 @@ public:
     fs.close();
 
     checkTrueInput(
-      ParserBuilder(*d_exprManager,filename)
+      ParserBuilder(d_exprManager,filename)
         .withInputLanguage(LANG_CVC4)
                    );
 
@@ -117,7 +117,7 @@ public:
 
   void testEmptyStringInput() {
     checkEmptyInput(
-      ParserBuilder(*d_exprManager,"foo")
+      ParserBuilder(d_exprManager,"foo")
         .withInputLanguage(LANG_CVC4)
         .withStringInput("")
                     );
@@ -125,7 +125,7 @@ public:
 
   void testTrueStringInput() {
     checkTrueInput(
-      ParserBuilder(*d_exprManager,"foo")
+      ParserBuilder(d_exprManager,"foo")
         .withInputLanguage(LANG_CVC4)
         .withStringInput("TRUE")
                    );
@@ -134,7 +134,7 @@ public:
   void testEmptyStreamInput() {
     stringstream ss( "", ios_base::in );
     checkEmptyInput(
-      ParserBuilder(*d_exprManager,"foo")
+      ParserBuilder(d_exprManager,"foo")
         .withInputLanguage(LANG_CVC4)
         .withStreamInput(ss)
                     );
@@ -143,7 +143,7 @@ public:
   void testTrueStreamInput() {
     stringstream ss( "TRUE", ios_base::in );
     checkTrueInput(
-      ParserBuilder(*d_exprManager,"foo")
+      ParserBuilder(d_exprManager,"foo")
         .withInputLanguage(LANG_CVC4)
         .withStreamInput(ss)
                    );
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index fffa36105..f6118d85c 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -104,7 +104,7 @@ class CnfStreamBlack : public CxxTest::TestSuite {
 
 void setUp() {
   d_context = new Context;
-  d_nodeManager = new NodeManager(d_context);
+  d_nodeManager = new NodeManager(d_context, NULL);
   NodeManagerScope nms(d_nodeManager);
   d_satSolver = new FakeSatSolver;
   d_theoryEngine = new TheoryEngine(d_context);
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
index e88f11673..0e8f5addb 100644
--- a/test/unit/theory/shared_term_manager_black.h
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -56,7 +56,7 @@ public:
   void setUp() {
     d_ctxt = new Context;
 
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     d_theoryEngine = new TheoryEngine(d_ctxt);
diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h
index 39dad4732..c60da2922 100644
--- a/test/unit/theory/stacking_map_black.h
+++ b/test/unit/theory/stacking_map_black.h
@@ -43,7 +43,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_map = new StackingMap<TNode, TNodeHashFunction>(d_ctxt);
 
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 9de8f94b4..060c3036d 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -93,7 +93,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
     d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL));
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 1897bbd1c..2d39af956 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -163,7 +163,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL));
     d_outputChannel.clear();
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 26908ec6e..f1a83cd49 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -236,7 +236,7 @@ public:
   void setUp() {
     d_ctxt = new Context;
 
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     d_nullChannel = new FakeOutputChannel;
diff --git a/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h
index 1940bc199..ae3eee369 100644
--- a/test/unit/theory/theory_uf_tim_white.h
+++ b/test/unit/theory/theory_uf_tim_white.h
@@ -58,7 +58,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
     d_euf = new TheoryUFTim(d_ctxt, d_outputChannel, Valuation(NULL));
diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h
index b9b4e58ce..6ba653946 100644
--- a/test/unit/theory/union_find_black.h
+++ b/test/unit/theory/union_find_black.h
@@ -43,7 +43,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_uf = new UnionFind<TNode, TNodeHashFunction>(d_ctxt);
 
diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h
index a12cb79ea..f5e299377 100644
--- a/test/unit/util/congruence_closure_white.h
+++ b/test/unit/util/congruence_closure_white.h
@@ -108,7 +108,7 @@ public:
 
   void setUp() {
     d_context = new Context;
-    d_nm = new NodeManager(d_context);
+    d_nm = new NodeManager(d_context, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_out = new MyOutputChannel(d_context, d_nm);
     d_cc = new CongruenceClosure<MyOutputChannel, CongruenceOperator<kind::APPLY_UF> >(d_context, d_out);