fix unit tests

1 files changed, 27 insertions, 27 deletions

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index cca2ff4fc..d392050f8 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -53,7 +53,7 @@ public:
   }
 
   void testMkNodeNot() {
-    Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
+    Node x = d_nodeManager->mkSkolem("x",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(NOT, x);
     TS_ASSERT_EQUALS( n.getNumChildren(), 1u );
     TS_ASSERT_EQUALS( n.getKind(), NOT);
@@ -61,8 +61,8 @@ public:
   }
 
   void testMkNodeBinary() {
-    Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
-    Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
+    Node x = d_nodeManager->mkSkolem("x",d_nodeManager->booleanType());
+    Node y = d_nodeManager->mkSkolem("y",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(IMPLIES, x, y);
     TS_ASSERT_EQUALS( n.getNumChildren(), 2u );
     TS_ASSERT_EQUALS( n.getKind(), IMPLIES);
@@ -71,9 +71,9 @@ public:
   }
 
   void testMkNodeThreeChildren() {
-    Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
-    Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
-    Node z = d_nodeManager->mkVar("z",d_nodeManager->booleanType());
+    Node x = d_nodeManager->mkSkolem("x",d_nodeManager->booleanType());
+    Node y = d_nodeManager->mkSkolem("y",d_nodeManager->booleanType());
+    Node z = d_nodeManager->mkSkolem("z",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(AND, x, y, z);
     TS_ASSERT_EQUALS( n.getNumChildren(), 3u );
     TS_ASSERT_EQUALS( n.getKind(), AND);
@@ -83,10 +83,10 @@ public:
   }
 
   void testMkNodeFourChildren() {
-    Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
-    Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
+    Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
+    Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
+    Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
+    Node x4 = d_nodeManager->mkSkolem("x4",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
     TS_ASSERT_EQUALS( n.getNumChildren(), 4u );
     TS_ASSERT_EQUALS( n.getKind(), AND );
@@ -97,11 +97,11 @@ public:
   }
 
   void testMkNodeFiveChildren() {
-    Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
-    Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
-    Node x5 = d_nodeManager->mkVar("x5",d_nodeManager->booleanType());
+    Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
+    Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
+    Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
+    Node x4 = d_nodeManager->mkSkolem("x4",d_nodeManager->booleanType());
+    Node x5 = d_nodeManager->mkSkolem("x5",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
     TS_ASSERT_EQUALS( n.getNumChildren(), 5u );
     TS_ASSERT_EQUALS( n.getKind(), AND);
@@ -113,9 +113,9 @@ public:
   }
 
   void testMkNodeVectorOfNodeChildren() {
-    Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
+    Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
+    Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
+    Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
     std::vector<Node> args;
     args.push_back(x1);
     args.push_back(x2);
@@ -129,9 +129,9 @@ public:
   }
 
   void testMkNodeVectorOfTNodeChildren() {
-    Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
+    Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
+    Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
+    Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
     std::vector<TNode> args;
     args.push_back(x1);
     args.push_back(x2);
@@ -146,16 +146,16 @@ public:
 
   void testMkVarWithNoName() {
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node x = d_nodeManager->mkVar(booleanType);
-    TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
+    Node x = d_nodeManager->mkSkolem(booleanType);
+    TS_ASSERT_EQUALS(x.getKind(),SKOLEM);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
     TS_ASSERT_EQUALS(x.getType(),booleanType);
   }
 
   void testMkVarWithName() {
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node x = d_nodeManager->mkVar("x", booleanType);
-    TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
+    Node x = d_nodeManager->mkSkolem("x", booleanType);
+    TS_ASSERT_EQUALS(x.getKind(),SKOLEM);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
     TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x");
     TS_ASSERT_EQUALS(x.getType(),booleanType);
@@ -337,7 +337,7 @@ public:
   /* This test is only valid if assertions are enabled. */
   void testMkNodeTooFew() {
 #ifdef CVC4_ASSERTIONS
-    Node x = d_nodeManager->mkVar( d_nodeManager->booleanType() );
+    Node x = d_nodeManager->mkSkolem( d_nodeManager->booleanType() );
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException );
 #endif
   }
@@ -349,7 +349,7 @@ public:
     const unsigned int max = metakind::getUpperBoundForKind(AND);
     TypeNode boolType = d_nodeManager->booleanType();
     for( unsigned int i = 0; i <= max; ++i ) {
-      vars.push_back( d_nodeManager->mkVar(boolType) );
+      vars.push_back( d_nodeManager->mkSkolem(boolType) );
     }
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
 #endif