Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)

This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.

This PR also eliminates some unused code in TheoryArithPrivate.

Followup PRs will start formalizing/eliminating calls to mkDummySkolem.

13 files changed, 141 insertions, 126 deletions

diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp
index 880bb85e4..0ec1c5e56 100644
--- a/test/unit/node/attribute_black.cpp
+++ b/test/unit/node/attribute_black.cpp
@@ -55,7 +55,7 @@ class TestNodeBlackAttribute : public TestNode
 TEST_F(TestNodeBlackAttribute, ints)
 {
   TypeNode booleanType = d_nodeManager->booleanType();
-  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+  Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
   const uint64_t val = 63489;
   uint64_t data0 = 0;
   uint64_t data1 = 0;
@@ -72,9 +72,9 @@ TEST_F(TestNodeBlackAttribute, ints)
 TEST_F(TestNodeBlackAttribute, tnodes)
 {
   TypeNode booleanType = d_nodeManager->booleanType();
-  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+  Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
 
-  Node val(d_nodeManager->mkSkolem("b", booleanType));
+  Node val(d_skolemManager->mkDummySkolem("b", booleanType));
   TNode data0;
   TNode data1;
 
@@ -90,7 +90,7 @@ TEST_F(TestNodeBlackAttribute, tnodes)
 TEST_F(TestNodeBlackAttribute, strings)
 {
   TypeNode booleanType = d_nodeManager->booleanType();
-  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+  Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
 
   std::string val("63489");
   std::string data0;
@@ -108,7 +108,7 @@ TEST_F(TestNodeBlackAttribute, strings)
 TEST_F(TestNodeBlackAttribute, bools)
 {
   TypeNode booleanType = d_nodeManager->booleanType();
-  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+  Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
 
   bool val = true;
   bool data0 = false;
diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp
index b9cac2169..1a739cf1b 100644
--- a/test/unit/node/node_algorithm_black.cpp
+++ b/test/unit/node/node_algorithm_black.cpp
@@ -39,7 +39,7 @@ class TestNodeBlackNodeAlgorithm : public TestNode
 TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1)
 {
   // The only symbol in ~x (x is a boolean varible) should be x
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
   Node n = d_nodeManager->mkNode(NOT, x);
   std::unordered_set<Node, NodeHashFunction> syms;
   getSymbols(n, syms);
@@ -53,8 +53,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
   // "var" is bound.
 
   // left conjunct
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
-  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
+  Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->integerType());
   Node left = d_nodeManager->mkNode(EQUAL, x, y);
 
   // right conjunct
@@ -87,12 +87,13 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
       std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
 
   // create test formula
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
   Node plus = d_nodeManager->mkNode(PLUS, x, x);
   Node mul = d_nodeManager->mkNode(MULT, x, x);
   Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul);
 
-  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4));
+  Node y =
+      d_skolemManager->mkDummySkolem("y", d_nodeManager->mkBitVectorType(4));
   Node ext1 = theory::bv::utils::mkExtract(y, 1, 0);
   Node ext2 = theory::bv::utils::mkExtract(y, 3, 2);
   Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2);
@@ -143,7 +144,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, match)
   Node two = d_nodeManager->mkConst(Rational(2));
 
   Node x = d_nodeManager->mkBoundVar(integer);
-  Node a = d_nodeManager->mkSkolem("a", integer);
+  Node a = d_skolemManager->mkDummySkolem("a", integer);
 
   Node n1 = d_nodeManager->mkNode(MULT, two, x);
   std::unordered_map<Node, Node, NodeHashFunction> subs;
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 87121c1c2..cfe008ec0 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -26,6 +26,7 @@
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
 #include "expr/node_value.h"
+#include "expr/skolem_manager.h"
 #include "smt/smt_engine.h"
 #include "test_node.h"
 #include "theory/rewriter.h"
@@ -43,10 +44,11 @@ std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager,
                                    TypeNode type)
 {
   std::vector<Node> skolems;
+  SkolemManager* sm = nodeManager->getSkolemManager();
   for (uint32_t i = 0; i < n; i++)
   {
-    skolems.push_back(nodeManager->mkSkolem(
-        "skolem_", type, "Created by makeNSkolemNodes()"));
+    skolems.push_back(
+        sm->mkDummySkolem("skolem_", type, "Created by makeNSkolemNodes()"));
   }
   return skolems;
 }
@@ -119,12 +121,12 @@ TEST_F(TestNodeBlackNode, operator_equals)
 {
   Node a, b, c;
 
-  b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+  b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
 
   a = b;
   c = a;
 
-  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+  Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType());
 
   ASSERT_TRUE(a == a);
   ASSERT_TRUE(a == b);
@@ -154,12 +156,12 @@ TEST_F(TestNodeBlackNode, operator_not_equals)
 {
   Node a, b, c;
 
-  b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+  b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
 
   a = b;
   c = a;
 
-  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+  Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType());
 
   /*structed assuming operator == works */
   ASSERT_TRUE(iff(a != a, !(a == a)));
@@ -215,7 +217,7 @@ TEST_F(TestNodeBlackNode, operator_assign)
 {
   Node a, b;
   Node c = d_nodeManager->mkNode(
-      NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
+      NOT, d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType()));
 
   b = c;
   ASSERT_EQ(b, c);
@@ -232,8 +234,8 @@ TEST_F(TestNodeBlackNode, operator_less_than)
   // We don't have access to the ids so we can't test the implementation
   // in the black box tests.
 
-  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
-  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+  Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
+  Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
 
   ASSERT_TRUE(a < b || b < a);
   ASSERT_TRUE(!(a < b && b < a));
@@ -275,8 +277,8 @@ TEST_F(TestNodeBlackNode, operator_less_than)
 TEST_F(TestNodeBlackNode, eqNode)
 {
   TypeNode t = d_nodeManager->mkSort();
-  Node left = d_nodeManager->mkSkolem("left", t);
-  Node right = d_nodeManager->mkSkolem("right", t);
+  Node left = d_skolemManager->mkDummySkolem("left", t);
+  Node right = d_skolemManager->mkDummySkolem("right", t);
   Node eq = left.eqNode(right);
 
   ASSERT_EQ(EQUAL, eq.getKind());
@@ -325,8 +327,8 @@ TEST_F(TestNodeBlackNode, orNode)
 
 TEST_F(TestNodeBlackNode, iteNode)
 {
-  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
-  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+  Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
+  Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
 
   Node cnd = d_nodeManager->mkNode(OR, a, b);
   Node thenBranch = d_nodeManager->mkConst(true);
@@ -382,8 +384,8 @@ TEST_F(TestNodeBlackNode, xorNode)
 
 TEST_F(TestNodeBlackNode, getKind)
 {
-  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
-  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+  Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
+  Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
 
   Node n = d_nodeManager->mkNode(NOT, a);
   ASSERT_EQ(NOT, n.getKind());
@@ -391,8 +393,8 @@ TEST_F(TestNodeBlackNode, getKind)
   n = d_nodeManager->mkNode(EQUAL, a, b);
   ASSERT_EQ(EQUAL, n.getKind());
 
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
-  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->realType());
+  Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->realType());
 
   n = d_nodeManager->mkNode(PLUS, x, y);
   ASSERT_EQ(PLUS, n.getKind());
@@ -407,8 +409,8 @@ TEST_F(TestNodeBlackNode, getOperator)
   TypeNode booleanType = d_nodeManager->booleanType();
   TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
-  Node f = d_nodeManager->mkSkolem("f", predType);
-  Node a = d_nodeManager->mkSkolem("a", sort);
+  Node f = d_skolemManager->mkDummySkolem("f", predType);
+  Node a = d_skolemManager->mkDummySkolem("a", sort);
   Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
 
   ASSERT_TRUE(fa.hasOperator());
@@ -460,9 +462,9 @@ TEST_F(TestNodeBlackNode, getNumChildren)
 TEST_F(TestNodeBlackNode, iterator)
 {
   NodeBuilder b;
-  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 x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
+  Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
+  Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
   Node n = b << x << y << z << kind::AND;
 
   {  // iterator
@@ -487,9 +489,9 @@ TEST_F(TestNodeBlackNode, kinded_iterator)
 {
   TypeNode integerType = d_nodeManager->integerType();
 
-  Node x = d_nodeManager->mkSkolem("x", integerType);
-  Node y = d_nodeManager->mkSkolem("y", integerType);
-  Node z = d_nodeManager->mkSkolem("z", integerType);
+  Node x = d_skolemManager->mkDummySkolem("x", integerType);
+  Node y = d_skolemManager->mkDummySkolem("y", integerType);
+  Node z = d_skolemManager->mkDummySkolem("z", integerType);
   Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
   Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
 
@@ -510,13 +512,13 @@ TEST_F(TestNodeBlackNode, toString)
 {
   TypeNode booleanType = d_nodeManager->booleanType();
 
-  Node w = d_nodeManager->mkSkolem(
+  Node w = d_skolemManager->mkDummySkolem(
       "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node x = d_nodeManager->mkSkolem(
+  Node x = d_skolemManager->mkDummySkolem(
       "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node y = d_nodeManager->mkSkolem(
+  Node y = d_skolemManager->mkDummySkolem(
       "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node z = d_nodeManager->mkSkolem(
+  Node z = d_skolemManager->mkDummySkolem(
       "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
   Node m = NodeBuilder() << w << x << kind::OR;
   Node n = NodeBuilder() << m << y << z << kind::AND;
@@ -528,13 +530,13 @@ TEST_F(TestNodeBlackNode, toStream)
 {
   TypeNode booleanType = d_nodeManager->booleanType();
 
-  Node w = d_nodeManager->mkSkolem(
+  Node w = d_skolemManager->mkDummySkolem(
       "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node x = d_nodeManager->mkSkolem(
+  Node x = d_skolemManager->mkDummySkolem(
       "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node y = d_nodeManager->mkSkolem(
+  Node y = d_skolemManager->mkDummySkolem(
       "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node z = d_nodeManager->mkSkolem(
+  Node z = d_skolemManager->mkDummySkolem(
       "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
   Node m = NodeBuilder() << x << y << kind::OR;
   Node n = NodeBuilder() << w << m << z << kind::AND;
@@ -597,14 +599,14 @@ TEST_F(TestNodeBlackNode, dagifier)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
 
-  Node x =
-      d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node y =
-      d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node f =
-      d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node g =
-      d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node x = d_skolemManager->mkDummySkolem(
+      "x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node y = d_skolemManager->mkDummySkolem(
+      "y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node f = d_skolemManager->mkDummySkolem(
+      "f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node g = d_skolemManager->mkDummySkolem(
+      "g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
   Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
   Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
   Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
@@ -702,7 +704,7 @@ TEST_F(TestNodeBlackNode, isConst)
       listType.getDType().getConstructors();
   Node cons = lcons[0]->getConstructor();
   Node nil = lcons[1]->getConstructor();
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
   Node cons_x_nil =
       d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
                             cons,
@@ -764,8 +766,9 @@ TEST_F(TestNodeBlackNode, isConst)
 namespace {
 Node level0(NodeManager* nm)
 {
+  SkolemManager* sm = nm->getSkolemManager();
   NodeBuilder nb(kind::AND);
-  Node x = nm->mkSkolem("x", nm->booleanType());
+  Node x = sm->mkDummySkolem("x", nm->booleanType());
   nb << x;
   nb << x;
   return Node(nb.constructNode());
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index 8c6145940..2b8ef7a04 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -92,7 +92,7 @@ TEST_F(TestNodeBlackNodeBuilder, getKind)
   NodeBuilder noKind;
   ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
 
-  Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
+  Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
   noKind << x << x;
   ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
 
@@ -112,7 +112,7 @@ TEST_F(TestNodeBlackNodeBuilder, getKind)
 
 TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
 {
-  Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
+  Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
 
   NodeBuilder nb;
 #ifdef CVC4_ASSERTIONS
@@ -300,16 +300,16 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
 
 TEST_F(TestNodeBlackNodeBuilder, append)
 {
-  Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
-  Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
-  Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
+  Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode);
+  Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode);
+  Node z = d_skolemManager->mkDummySkolem("z", *d_boolTypeNode);
   Node m = d_nodeManager->mkNode(AND, y, z, x);
   Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z);
   Node o = d_nodeManager->mkNode(XOR, y, x);
 
-  Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode);
-  Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode);
-  Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode);
+  Node r = d_skolemManager->mkDummySkolem("r", *d_realTypeNode);
+  Node s = d_skolemManager->mkDummySkolem("s", *d_realTypeNode);
+  Node t = d_skolemManager->mkDummySkolem("t", *d_realTypeNode);
 
   Node p = d_nodeManager->mkNode(
       EQUAL,
@@ -389,13 +389,13 @@ TEST_F(TestNodeBlackNodeBuilder, leftist_building)
 {
   NodeBuilder nb;
 
-  Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode);
+  Node a = d_skolemManager->mkDummySkolem("a", *d_boolTypeNode);
 
-  Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode);
-  Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode);
+  Node b = d_skolemManager->mkDummySkolem("b", *d_boolTypeNode);
+  Node c = d_skolemManager->mkDummySkolem("c", *d_boolTypeNode);
 
-  Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode);
-  Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode);
+  Node d = d_skolemManager->mkDummySkolem("d", *d_realTypeNode);
+  Node e = d_skolemManager->mkDummySkolem("e", *d_realTypeNode);
 
   nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE;
 
diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index 5d21ff734..6ad6f583c 100644
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -37,7 +37,7 @@ class TestNodeBlackNodeManager : public TestNode
 
 TEST_F(TestNodeBlackNodeManager, mkNode_not)
 {
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
   Node n = d_nodeManager->mkNode(NOT, x);
   ASSERT_EQ(n.getNumChildren(), 1u);
   ASSERT_EQ(n.getKind(), NOT);
@@ -46,8 +46,8 @@ TEST_F(TestNodeBlackNodeManager, mkNode_not)
 
 TEST_F(TestNodeBlackNodeManager, mkNode_binary)
 {
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
-  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
+  Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
   Node n = d_nodeManager->mkNode(IMPLIES, x, y);
   ASSERT_EQ(n.getNumChildren(), 2u);
   ASSERT_EQ(n.getKind(), IMPLIES);
@@ -57,9 +57,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_binary)
 
 TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
 {
-  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 x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
+  Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
+  Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
   Node n = d_nodeManager->mkNode(AND, x, y, z);
   ASSERT_EQ(n.getNumChildren(), 3u);
   ASSERT_EQ(n.getKind(), AND);
@@ -70,10 +70,10 @@ TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
 
 TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
 {
-  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 x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
+  Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
   Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
   ASSERT_EQ(n.getNumChildren(), 4u);
   ASSERT_EQ(n.getKind(), AND);
@@ -85,11 +85,11 @@ TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
 
 TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
 {
-  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 x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
+  Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
+  Node x5 = d_skolemManager->mkDummySkolem("x5", d_nodeManager->booleanType());
   Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
   ASSERT_EQ(n.getNumChildren(), 5u);
   ASSERT_EQ(n.getKind(), AND);
@@ -102,9 +102,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
 
 TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
 {
-  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 x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
   std::vector<Node> args;
   args.push_back(x1);
   args.push_back(x2);
@@ -120,9 +120,9 @@ TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
 
 TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
 {
-  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 x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
   std::vector<TNode> args;
   args.push_back(x1);
   args.push_back(x2);
@@ -138,7 +138,7 @@ TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
 
 TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
 {
-  Node x = d_nodeManager->mkSkolem(
+  Node x = d_skolemManager->mkDummySkolem(
       "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
   ASSERT_EQ(x.getKind(), SKOLEM);
   ASSERT_EQ(x.getNumChildren(), 0u);
@@ -303,7 +303,7 @@ TEST_F(TestNodeBlackNodeManager, mkPredicateType)
 TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
 {
 #ifdef CVC4_ASSERTIONS
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
   ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
                "Nodes with kind AND must have at least 2 children");
 #endif
@@ -316,8 +316,8 @@ TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
   std::vector<Node> vars;
   const uint32_t max = metakind::getMaxArityForKind(AND);
   TypeNode boolType = d_nodeManager->booleanType();
-  Node skolem_i = d_nodeManager->mkSkolem("i", boolType);
-  Node skolem_j = d_nodeManager->mkSkolem("j", boolType);
+  Node skolem_i = d_skolemManager->mkDummySkolem("i", boolType);
+  Node skolem_j = d_skolemManager->mkDummySkolem("j", boolType);
   Node andNode = skolem_i.andNode(skolem_j);
   Node orNode = skolem_i.orNode(skolem_j);
   while (vars.size() <= max)
diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp
index 66ac65cb5..a13e76d03 100644
--- a/test/unit/node/node_manager_white.cpp
+++ b/test/unit/node/node_manager_white.cpp
@@ -64,8 +64,8 @@ TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
 TEST_F(TestNodeWhiteNodeManager, topological_sort)
 {
   TypeNode boolType = d_nodeManager->booleanType();
-  Node i = d_nodeManager->mkSkolem("i", boolType);
-  Node j = d_nodeManager->mkSkolem("j", boolType);
+  Node i = d_skolemManager->mkDummySkolem("i", boolType);
+  Node j = d_skolemManager->mkDummySkolem("j", boolType);
   Node n1 = d_nodeManager->mkNode(kind::AND, j, j);
   Node n2 = d_nodeManager->mkNode(kind::AND, i, n1);
 
diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp
index 43eebcda9..fa4889540 100644
--- a/test/unit/node/node_self_iterator_black.cpp
+++ b/test/unit/node/node_self_iterator_black.cpp
@@ -32,8 +32,8 @@ class TestNodeBlackNodeSelfIterator : public TestNode
 
 TEST_F(TestNodeBlackNodeSelfIterator, iteration)
 {
-  Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
-  Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
+  Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode);
+  Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode);
   Node x_and_y = x.andNode(y);
   NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y);
   ASSERT_NE(i, x_and_y.end());
diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index 359cc0b6f..dacc1f543 100644
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -16,6 +16,7 @@
 #define CVC4__TEST__UNIT__TEST_NODE_H
 
 #include "expr/node_manager.h"
+#include "expr/skolem_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "test.h"
@@ -29,6 +30,7 @@ class TestNode : public TestInternal
   void SetUp() override
   {
     d_nodeManager.reset(new NodeManager());
+    d_skolemManager = d_nodeManager->getSkolemManager();
     d_scope.reset(new NodeManagerScope(d_nodeManager.get()));
     d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType()));
     d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2)));
@@ -38,6 +40,7 @@ class TestNode : public TestInternal
 
   std::unique_ptr<NodeManagerScope> d_scope;
   std::unique_ptr<NodeManager> d_nodeManager;
+  SkolemManager* d_skolemManager;
   std::unique_ptr<TypeNode> d_boolTypeNode;
   std::unique_ptr<TypeNode> d_bvTypeNode;
   std::unique_ptr<TypeNode> d_intTypeNode;
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index f26bd0ff6..9be954059 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -19,6 +19,7 @@
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "expr/proof_checker.h"
+#include "expr/skolem_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "test.h"
@@ -43,6 +44,7 @@ class TestSmt : public TestInternal
   void SetUp() override
   {
     d_nodeManager.reset(new NodeManager());
+    d_skolemManager = d_nodeManager->getSkolemManager();
     d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
     d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
     d_smtEngine->finishInit();
@@ -50,6 +52,7 @@ class TestSmt : public TestInternal
 
   std::unique_ptr<NodeManagerScope> d_nmScope;
   std::unique_ptr<NodeManager> d_nodeManager;
+  SkolemManager* d_skolemManager;
   std::unique_ptr<SmtEngine> d_smtEngine;
 };
 
@@ -59,12 +62,14 @@ class TestSmtNoFinishInit : public TestInternal
   void SetUp() override
   {
     d_nodeManager.reset(new NodeManager());
+    d_skolemManager = d_nodeManager->getSkolemManager();
     d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
     d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
   }
 
   std::unique_ptr<NodeManagerScope> d_nmScope;
   std::unique_ptr<NodeManager> d_nodeManager;
+  SkolemManager* d_skolemManager;
   std::unique_ptr<SmtEngine> d_smtEngine;
 };
 
diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index 586afd8b5..10a606d11 100644
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -41,7 +41,8 @@ class TestTheoryWhiteBagsRewriter : public TestSmt
     std::vector<Node> elements(n);
     for (size_t i = 0; i < n; i++)
     {
-      elements[i] = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+      elements[i] =
+          d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
     }
     return elements;
   }
@@ -63,8 +64,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality)
   std::vector<Node> elements = getNStrings(2);
   Node x = elements[0];
   Node y = elements[1];
-  Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType());
-  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->integerType());
+  Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
+  Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->integerType());
   Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
   Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), y, d);
   Node emptyBag = d_nodeManager->mkConst(
@@ -129,7 +130,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element)
 
 TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element)
 {
-  Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+  Node skolem =
+      d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(),
                                        skolem,
                                        d_nodeManager->mkConst(Rational(-1)));
@@ -160,7 +162,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element)
 TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
 {
   int n = 3;
-  Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+  Node skolem =
+      d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(skolem.getType())));
   Node bag = d_nodeManager->mkBag(
@@ -181,7 +184,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
 
 TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)
 {
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node bag = d_nodeManager->mkBag(
       d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
 
@@ -585,7 +588,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove)
 
 TEST_F(TestTheoryWhiteBagsRewriter, choose)
 {
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node c = d_nodeManager->mkConst(Rational(3));
   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
 
@@ -598,7 +601,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, choose)
 
 TEST_F(TestTheoryWhiteBagsRewriter, bag_card)
 {
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
   Node zero = d_nodeManager->mkConst(Rational(0));
@@ -640,8 +643,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton)
 {
   Node emptybag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
-  Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
+  Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
 
   // TODO(projects#223): complete this function
@@ -662,7 +665,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton)
 
 TEST_F(TestTheoryWhiteBagsRewriter, from_set)
 {
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
 
   // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1)
@@ -676,7 +679,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set)
 
 TEST_F(TestTheoryWhiteBagsRewriter, to_set)
 {
-  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node bag = d_nodeManager->mkBag(
       d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
 
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
index 64ba39e7f..92e76d5f5 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
@@ -41,7 +41,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
 
     d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4));
     d_t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(4));
-    d_sk = d_nodeManager->mkSkolem("sk", d_t.getType());
+    d_sk = d_skolemManager->mkDummySkolem("sk", d_t.getType());
     d_x = d_nodeManager->mkBoundVar(d_t.getType());
     d_bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {d_x});
   }
@@ -139,7 +139,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
     {
       s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4));
       x = d_nodeManager->mkBoundVar(s2.getType());
-      sk = d_nodeManager->mkSkolem("sk", s2.getType());
+      sk = d_skolemManager->mkDummySkolem("sk", s2.getType());
       t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8));
       sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, x, s2);
       sc = getICBvConcat(pol, litk, 0, sk, sv_t, t);
@@ -148,7 +148,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
     {
       s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4));
       x = d_nodeManager->mkBoundVar(s1.getType());
-      sk = d_nodeManager->mkSkolem("sk", s1.getType());
+      sk = d_skolemManager->mkDummySkolem("sk", s1.getType());
       t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8));
       sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x);
       sc = getICBvConcat(pol, litk, 1, sk, sv_t, t);
@@ -159,7 +159,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
       s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4));
       s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4));
       x = d_nodeManager->mkBoundVar(s2.getType());
-      sk = d_nodeManager->mkSkolem("sk", s1.getType());
+      sk = d_skolemManager->mkDummySkolem("sk", s1.getType());
       t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(12));
       sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x, s2);
       sc = getICBvConcat(pol, litk, 1, sk, sv_t, t);
@@ -195,7 +195,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
     unsigned w = 8;
 
     Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(wx));
-    Node sk = d_nodeManager->mkSkolem("sk", x.getType());
+    Node sk = d_skolemManager->mkDummySkolem("sk", x.getType());
     x = d_nodeManager->mkBoundVar(x.getType());
 
     Node t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(w));
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp
index 33543cc42..920075674 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.cpp
+++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp
@@ -33,11 +33,11 @@ class TestTheoryBlackStringsSkolemCache : public TestSmt
 TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
 {
   Node zero = d_nodeManager->mkConst(Rational(0));
-  Node n = d_nodeManager->mkSkolem("n", d_nodeManager->integerType());
-  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->stringType());
-  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->stringType());
-  Node c = d_nodeManager->mkSkolem("c", d_nodeManager->stringType());
-  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->stringType());
+  Node n = d_skolemManager->mkDummySkolem("n", d_nodeManager->integerType());
+  Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->stringType());
+  Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->stringType());
+  Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->stringType());
+  Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->stringType());
   Node sa = d_nodeManager->mkNode(
       kind::STRING_SUBSTR,
       a,
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index 97bbb1bcf..2e266ce58 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -36,20 +36,20 @@ class TestUtilBlackBooleanSimplification : public TestNode
   {
     TestNode::SetUp();
 
-    d_a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
-    d_b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-    d_c = d_nodeManager->mkSkolem("c", d_nodeManager->booleanType());
-    d_d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
-    d_e = d_nodeManager->mkSkolem("e", d_nodeManager->booleanType());
-    d_f = d_nodeManager->mkSkolem(
+    d_a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
+    d_b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
+    d_c = d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType());
+    d_d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType());
+    d_e = d_skolemManager->mkDummySkolem("e", d_nodeManager->booleanType());
+    d_f = d_skolemManager->mkDummySkolem(
         "f",
         d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
                                       d_nodeManager->booleanType()));
-    d_g = d_nodeManager->mkSkolem(
+    d_g = d_skolemManager->mkDummySkolem(
         "g",
         d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
                                       d_nodeManager->booleanType()));
-    d_h = d_nodeManager->mkSkolem(
+    d_h = d_skolemManager->mkDummySkolem(
         "h",
         d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
                                       d_nodeManager->booleanType()));