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.

29 files changed, 164 insertions, 112 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 292ec2ec6..1d602b925 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -16,6 +16,7 @@
 
 #include <algorithm>
 
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/quantifiers/bv_inverter_utils.h"
@@ -35,14 +36,12 @@ Node BvInverter::getSolveVariable(TypeNode tn)
   std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn);
   if (its == d_solve_var.end())
   {
-    Node k = NodeManager::currentNM()->mkSkolem("slv", tn);
+    SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+    Node k = sm->mkDummySkolem("slv", tn);
     d_solve_var[tn] = k;
     return k;
   }
-  else
-  {
-    return its->second;
-  }
+  return its->second;
 }
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index bdd6d26ab..45433bdb6 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
 
 #include <stack>
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
@@ -642,6 +643,7 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
   if (options::cegqiBvRmExtract())
   {
     NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
     // map from terms to bitvector extracts applied to that term
     std::map<Node, std::vector<Node> > extract_map;
@@ -691,9 +693,9 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
         Node ex = bv::utils::mkExtract(
             es.first, boundaries[i - 1] - 1, boundaries[i]);
         Node var =
-            nm->mkSkolem("ek",
-                         ex.getType(),
-                         "variable to represent disjoint extract region");
+            sm->mkDummySkolem("ek",
+                              ex.getType(),
+                              "variable to represent disjoint extract region");
         children.push_back(var);
         vars.push_back(var);
       }
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 5e3a64325..74469e7de 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
@@ -463,7 +464,8 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
     return it->second;
   }
   NodeManager * nm = NodeManager::currentNM();
-  Node g = nm->mkSkolem("g", nm->booleanType());
+  SkolemManager* sm = nm->getSkolemManager();
+  Node g = sm->mkDummySkolem("g", nm->booleanType());
   // ensure that it is a SAT literal
   Node ceLit = d_qstate.getValuation().ensureLiteral(g);
   d_ce_lit[q] = ceLit;
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index 1974e7c7c..5f114c313 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/vts_term_cache.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/rewriter.h"
@@ -60,18 +61,19 @@ Node VtsTermCache::getVtsDelta(bool isFree, bool create)
   if (create)
   {
     NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     if (d_vts_delta_free.isNull())
     {
       d_vts_delta_free =
-          nm->mkSkolem("delta_free",
-                       nm->realType(),
-                       "free delta for virtual term substitution");
+          sm->mkDummySkolem("delta_free",
+                            nm->realType(),
+                            "free delta for virtual term substitution");
       Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero);
       d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA);
     }
     if (d_vts_delta.isNull())
     {
-      d_vts_delta = nm->mkSkolem(
+      d_vts_delta = sm->mkDummySkolem(
           "delta", nm->realType(), "delta for virtual term substitution");
       // mark as a virtual term
       VirtualTermSkolemAttribute vtsa;
@@ -86,15 +88,16 @@ Node VtsTermCache::getVtsInfinity(TypeNode tn, bool isFree, bool create)
   if (create)
   {
     NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     if (d_vts_inf_free[tn].isNull())
     {
-      d_vts_inf_free[tn] = nm->mkSkolem(
+      d_vts_inf_free[tn] = sm->mkDummySkolem(
           "inf_free", tn, "free infinity for virtual term substitution");
     }
     if (d_vts_inf[tn].isNull())
     {
-      d_vts_inf[tn] =
-          nm->mkSkolem("inf", tn, "infinity for virtual term substitution");
+      d_vts_inf[tn] = sm->mkDummySkolem(
+          "inf", tn, "infinity for virtual term substitution");
       // mark as a virtual term
       VirtualTermSkolemAttribute vtsa;
       d_vts_inf[tn].setAttribute(vtsa, true);
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 41d881f2c..ba716254a 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/conjecture_generator.h"
 
+#include "expr/skolem_manager.h"
 #include "expr/term_canonize.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
@@ -1089,8 +1090,11 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo
 Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
   std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );
   if( it==d_typ_pred.end() ){
-    TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );
-    Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." );
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
+    TypeNode op_tn = nm->mkFunctionType(tn, nm->booleanType());
+    Node op = sm->mkDummySkolem(
+        "PE", op_tn, "was created by conjecture ground term enumerator.");
     d_typ_pred[tn] = op;
     return op;
   }else{
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index fe712e01e..f72acaa18 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/dynamic_rewrite.h"
 
+#include "expr/skolem_manager.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -144,6 +145,8 @@ Node DynamicRewriter::toExternal(Node ai)
 
 Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
 {
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::vector<TypeNode> ctypes;
   for (const Node& cn : n)
   {
@@ -173,10 +176,9 @@ Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
   }
   else
   {
-    utype = NodeManager::currentNM()->mkFunctionType(ctypes);
+    utype = nm->mkFunctionType(ctypes);
   }
-  Node f = NodeManager::currentNM()->mkSkolem(
-      "ufd", utype, "internal op for dynamic_rewriter");
+  Node f = sm->mkDummySkolem("ufd", utype, "internal op for dynamic_rewriter");
   curr->d_sym = f;
   return f;
 }
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index b21252358..801bde022 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/expr_miner.h"
 
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -46,6 +47,7 @@ Node ExprMiner::convertToSkolem(Node n)
   std::vector<Node> sks;
   // map to skolems
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   for (unsigned i = 0, size = fvs.size(); i < size; i++)
   {
     Node v = fvs[i];
@@ -56,7 +58,7 @@ Node ExprMiner::convertToSkolem(Node n)
       std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
       if (itf == d_fv_to_skolem.end())
       {
-        Node sk = nm->mkSkolem("rrck", v.getType());
+        Node sk = sm->mkDummySkolem("rrck", v.getType());
         d_fv_to_skolem[v] = sk;
         sks.push_back(sk);
       }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index efa3dd160..bbbf820b6 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
@@ -43,7 +44,8 @@ BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
     : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u)
 {
   if( options::fmfBoundLazy() ){
-    d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
+    SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+    d_proxy_range = isProxy ? r : sm->mkDummySkolem("pbir", r.getType());
   }else{
     d_proxy_range = r;
   }
@@ -315,6 +317,7 @@ void BoundedIntegers::checkOwnership(Node f)
   //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
   Trace("bound-int") << "check ownership quantifier " << f << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
 
   bool success;
   do{
@@ -484,8 +487,8 @@ void BoundedIntegers::checkOwnership(Node f)
         if (expr::hasBoundVar(r))
         {
           // introduce a new bound
-          Node new_range = NodeManager::currentNM()->mkSkolem(
-              "bir", r.getType(), "bound for term");
+          Node new_range =
+              sm->mkDummySkolem("bir", r.getType(), "bound for term");
           d_nground_range[f][v] = r;
           d_range[f][v] = new_range;
           r = new_range;
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index 515d9fe58..cc2e0fbf1 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 
 #include "expr/attribute.h"
+#include "expr/skolem_manager.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/rewriter.h"
 
@@ -90,8 +91,9 @@ Node FirstOrderModelFmc::getStar(TypeNode tn)
   {
     return it->second;
   }
-  Node st = NodeManager::currentNM()->mkSkolem(
-      "star", tn, "skolem created for full-model checking");
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node st =
+      sm->mkDummySkolem("star", tn, "skolem created for full-model checking");
   d_type_star[tn] = st;
   st.setAttribute(IsStarAttribute(), true);
   return st;
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 7dbc10f57..6f0c13f63 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/fmf/full_model_check.h"
 
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
@@ -1349,6 +1350,7 @@ void FullModelChecker::registerQuantifiedFormula(Node q)
     return;
   }
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::vector<TypeNode> types;
   for (const Node& v : q[0])
   {
@@ -1363,7 +1365,7 @@ void FullModelChecker::registerQuantifiedFormula(Node q)
     types.push_back(tn);
   }
   TypeNode typ = nm->mkFunctionType(types, nm->booleanType());
-  Node op = nm->mkSkolem("qfmc", typ, "op for full-model checking");
+  Node op = sm->mkDummySkolem("qfmc", typ, "op for full-model checking");
   d_quant_cond[q] = op;
 }
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 89358c511..7e484956e 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -18,6 +18,7 @@
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
@@ -1563,7 +1564,8 @@ Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
   children.push_back(body);
   if (marked)
   {
-    Node avar = nm->mkSkolem("id", nm->booleanType());
+    SkolemManager* sm = nm->getSkolemManager();
+    Node avar = sm->mkDummySkolem("id", nm->booleanType());
     QuantIdNumAttribute ida;
     avar.setAttribute(ida, 0);
     iplc.push_back(nm->mkNode(kind::INST_ATTRIBUTE, avar));
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index 2fe173763..7a1a6fb45 100644
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -17,6 +17,7 @@
 #include <sstream>
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
@@ -180,6 +181,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
   Assert(d_input_funcs.empty());
   Assert(d_si_vars.empty());
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   d_has_input_funcs = has_funcs;
   d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end());
   d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end());
@@ -194,7 +196,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
   Assert(d_si_vars.size() == d_arg_types.size());
   for (const Node& inf : d_input_funcs)
   {
-    Node sk = nm->mkSkolem("_sik", inf.getType());
+    Node sk = sm->mkDummySkolem("_sik", inf.getType());
     d_input_func_sks.push_back(sk);
   }
   Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl;
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 51b400dbe..43d30f5bd 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -178,6 +178,7 @@ Node Skolemize::mkSkolemizedBody(Node f,
                                  std::vector<unsigned>& sub_vars)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Assert(sk.empty() || sk.size() == f[0].getNumChildren());
   // calculate the variables and substitution
   std::vector<TNode> ind_vars;
@@ -202,21 +203,20 @@ Node Skolemize::mkSkolemizedBody(Node f,
     {
       if (argTypes.empty())
       {
-        s = NodeManager::currentNM()->mkSkolem(
+        s = sm->mkDummySkolem(
             "skv", f[0][i].getType(), "created during skolemization");
       }
       else
       {
-        TypeNode typ = NodeManager::currentNM()->mkFunctionType(
-            argTypes, f[0][i].getType());
-        Node op = NodeManager::currentNM()->mkSkolem(
+        TypeNode typ = nm->mkFunctionType(argTypes, f[0][i].getType());
+        Node op = sm->mkDummySkolem(
             "skop", typ, "op created during pre-skolemization");
         // DOTHIS: set attribute on op, marking that it should not be selected
         // as trigger
         std::vector<Node> funcArgs;
         funcArgs.push_back(op);
         funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
-        s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs);
+        s = nm->mkNode(kind::APPLY_UF, funcArgs);
       }
       sk.push_back(s);
     }
@@ -264,27 +264,19 @@ Node Skolemize::mkSkolemizedBody(Node f,
         {
           conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
         }
-        disj.push_back(conj.size() == 1
-                           ? conj[0]
-                           : NodeManager::currentNM()->mkNode(OR, conj));
+        disj.push_back(conj.size() == 1 ? conj[0] : nm->mkNode(OR, conj));
       }
       Assert(!disj.empty());
-      n_str_ind = disj.size() == 1
-                      ? disj[0]
-                      : NodeManager::currentNM()->mkNode(AND, disj);
+      n_str_ind = disj.size() == 1 ? disj[0] : nm->mkNode(AND, disj);
     }
     else if (options::intWfInduction() && tn.isInteger())
     {
-      Node icond = NodeManager::currentNM()->mkNode(
-          GEQ, k, NodeManager::currentNM()->mkConst(Rational(0)));
-      Node iret =
-          ret.substitute(
-                 ind_vars[0],
-                 NodeManager::currentNM()->mkNode(
-                     MINUS, k, NodeManager::currentNM()->mkConst(Rational(1))))
-              .negate();
-      n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret);
-      n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind);
+      Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0)));
+      Node iret = ret.substitute(ind_vars[0],
+                                 nm->mkNode(MINUS, k, nm->mkConst(Rational(1))))
+                      .negate();
+      n_str_ind = nm->mkNode(OR, icond.negate(), iret);
+      n_str_ind = nm->mkNode(AND, icond, n_str_ind);
     }
     else
     {
@@ -299,17 +291,15 @@ Node Skolemize::mkSkolemizedBody(Node f,
         rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
     if (!rem_ind_vars.empty())
     {
-      Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars);
-      nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret);
+      Node bvl = nm->mkNode(BOUND_VAR_LIST, rem_ind_vars);
+      nret = nm->mkNode(FORALL, bvl, nret);
       nret = Rewriter::rewrite(nret);
       sub = nret;
       sub_vars.insert(
           sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
-      n_str_ind = NodeManager::currentNM()
-                      ->mkNode(FORALL, bvl, n_str_ind.negate())
-                      .negate();
+      n_str_ind = nm->mkNode(FORALL, bvl, n_str_ind.negate()).negate();
     }
-    ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind);
+    ret = nm->mkNode(OR, nret, n_str_ind);
   }
   Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
                                 << " returns : " << ret << std::endl;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 5e9f2d591..796e749cc 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -14,6 +14,7 @@
  **/
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_engine.h"
@@ -144,6 +145,7 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
     return;
   }
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   d_single_inv = d_sip->getSingleInvocation();
   d_single_inv = TermUtil::simpleNegate(d_single_inv);
   std::vector<Node> func_vars;
@@ -159,8 +161,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
   d_sip->getSingleInvocationVariables(sivars);
   for (unsigned i = 0, size = sivars.size(); i < size; i++)
   {
-    Node v = NodeManager::currentNM()->mkSkolem(
-        "a", sivars[i].getType(), "single invocation arg");
+    Node v =
+        sm->mkDummySkolem("a", sivars[i].getType(), "single invocation arg");
     d_single_inv_arg_sk.push_back(v);
   }
   d_single_inv = d_single_inv.substitute(sivars.begin(),
@@ -209,15 +211,16 @@ bool CegSingleInv::solve()
   }
   Trace("sygus-si") << "Solve using single invocation..." << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   // Mark the quantified formula with the quantifier elimination attribute to
   // ensure its structure is preserved in the query below.
   Node siq = d_single_inv;
   if (siq.getKind() == FORALL)
   {
-    Node n_attr =
-        nm->mkSkolem("qe_si",
-                     nm->booleanType(),
-                     "Auxiliary variable for qe attr for single invocation.");
+    Node n_attr = sm->mkDummySkolem(
+        "qe_si",
+        nm->booleanType(),
+        "Auxiliary variable for qe attr for single invocation.");
     QuantElimAttribute qea;
     n_attr.setAttribute(qea, true);
     n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 9a5c6146d..84e9f1070 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/cegis_unif.h"
 
+#include "expr/skolem_manager.h"
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -417,7 +418,8 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
 Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node new_lit = nm->mkSkolem("G_cost", nm->booleanType());
+  SkolemManager* sm = nm->getSkolemManager();
+  Node newLit = sm->mkDummySkolem("G_cost", nm->booleanType());
   unsigned new_size = n + 1;
 
   // allocate an enumerator for each candidate
@@ -425,13 +427,13 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
   {
     Node c = ci.first;
     TypeNode ct = c.getType();
-    Node eu = nm->mkSkolem("eu", ct);
+    Node eu = sm->mkDummySkolem("eu", ct);
     Node ceu;
     if (!d_useCondPool && !ci.second.d_enums[0].empty())
     {
       // make a new conditional enumerator as well, starting the
       // second type around
-      ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
+      ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type);
     }
     // register the new enumerators
     for (unsigned index = 0; index < 2; index++)
@@ -452,7 +454,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
     {
       Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
                                << " to new size " << new_size << "\n";
-      registerEvalPtAtSize(c, ei, new_lit, new_size);
+      registerEvalPtAtSize(c, ei, newLit, new_size);
     }
   }
   // enforce fairness between number of enumerators and enumerator size
@@ -483,7 +485,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
       datatypes.push_back(sdt.getDatatype());
       std::vector<TypeNode> dtypes = nm->mkMutualDatatypeTypes(
           datatypes, unresolvedTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
-      d_virtual_enum = nm->mkSkolem("_ve", dtypes[0]);
+      d_virtual_enum = sm->mkDummySkolem("_ve", dtypes[0]);
       d_tds->registerEnumerator(
           d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
     }
@@ -497,7 +499,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
       Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
       Node fair_lemma =
           nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
-      fair_lemma = nm->mkNode(OR, new_lit, fair_lemma);
+      fair_lemma = nm->mkNode(OR, newLit, fair_lemma);
       Trace("cegis-unif-enum-lemma")
           << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
       // this lemma relates the number of conditions we enumerate and the
@@ -510,7 +512,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
     }
   }
 
-  return new_lit;
+  return newLit;
 }
 
 void CegisUnifEnumDecisionStrategy::initialize(
@@ -526,6 +528,7 @@ void CegisUnifEnumDecisionStrategy::initialize(
   }
   // initialize type information for candidates
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   for (const Node& e : es)
   {
     Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n";
@@ -570,7 +573,7 @@ void CegisUnifEnumDecisionStrategy::initialize(
     // allocate a condition enumerator for each candidate
     for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
     {
-      Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
+      Node ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type);
       setUpEnumerator(ceu, ci.second, 1);
     }
   }
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp
index 97ae4878d..0e498bb18 100644
--- a/src/theory/quantifiers/sygus/rcons_type_info.cpp
+++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/rcons_type_info.h"
 
+#include "expr/skolem_manager.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 
 namespace cvc5 {
@@ -26,9 +27,10 @@ void RConsTypeInfo::initialize(TermDbSygus* tds,
                                const std::vector<Node>& builtinVars)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
 
   d_enumerator.reset(new SygusEnumerator(tds, nullptr, s, true));
-  d_enumerator->initialize(nm->mkSkolem("sygus_rcons", stn));
+  d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn));
   d_crd.reset(new CandidateRewriteDatabase(true, false, true, false));
   // since initial samples are not always useful for equivalence checks, set
   // their number to 0
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 8df45320f..278d708ee 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "expr/sygus_datatype.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -43,6 +44,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
                                         TypeNode abdGType)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::unordered_set<Node, NodeHashFunction> symset;
   for (size_t i = 0, size = asserts.size(); i < size; i++)
   {
@@ -166,7 +168,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   Node sc = nm->mkNode(AND, aconj, abdApp);
   Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars);
   sc = nm->mkNode(EXISTS, vbvl, sc);
-  Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType());
+  Node sygusScVar = sm->mkDummySkolem("sygus_sc", nm->booleanType());
   sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
   Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
   // build in the side condition
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
index 1b3a52db8..4f3d9a2e4 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_qe_preproc.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "theory/quantifiers/single_inv_partition.h"
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
@@ -35,6 +36,7 @@ Node SygusQePreproc::preprocess(Node q)
     body = body[0][1];
   }
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Trace("cegqi-qep") << "Compute single invocation for " << q << "..."
                      << std::endl;
   quantifiers::SingleInvocationPartition sip;
@@ -84,7 +86,7 @@ Node SygusQePreproc::preprocess(Node q)
   // skolemize non-qe variables
   for (unsigned i = 0, size = nqe_vars.size(); i < size; i++)
   {
-    Node k = nm->mkSkolem(
+    Node k = sm->mkDummySkolem(
         "k", nqe_vars[i].getType(), "qe for non-ground single invocation");
     orig.push_back(nqe_vars[i]);
     subs.push_back(k);
@@ -100,7 +102,7 @@ Node SygusQePreproc::preprocess(Node q)
     Node fv = sip.getFirstOrderVariableForFunction(f);
     Assert(!fi.isNull());
     orig.push_back(fi);
-    Node k = nm->mkSkolem(
+    Node k = sm->mkDummySkolem(
         "k", fv.getType(), "qe for function in non-ground single invocation");
     subs.push_back(k);
     Trace("cegqi-qep") << "  subs : " << fi << " -> " << k << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index 55e8c922d..70e6b7f2e 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_reconstruct.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "smt/command.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/rewriter.h"
@@ -47,12 +48,13 @@ Node SygusReconstruct::reconstructSolution(Node sol,
   initialize(stn);
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
 
   /** a set of obligations that are not yet satisfied for each sygus datatype */
   TypeObligationSetMap unsolvedObs;
 
   // paramaters sol and stn constitute the main obligation to satisfy
-  Node mainOb = nm->mkSkolem("sygus_rcons", stn);
+  Node mainOb = sm->mkDummySkolem("sygus_rcons", stn);
 
   // add the main obligation to the set of obligations that are not yet
   // satisfied
@@ -99,7 +101,7 @@ Node SygusReconstruct::reconstructSolution(Node sol,
         {
           // if not, create an "artifical" obligation whose solution would be
           // the enumerated term
-          k = nm->mkSkolem("sygus_rcons", pair.first);
+          k = sm->mkDummySkolem("sygus_rcons", pair.first);
           d_obInfo.emplace(k, RConsObligationInfo(builtin));
           d_stnInfo[pair.first].setBuiltinToOb(builtin, k);
         }
@@ -201,6 +203,7 @@ Node SygusReconstruct::reconstructSolution(Node sol,
 TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   TypeObligationSetMap obsPrime;
 
   // obligations generated by match. Note that we might have already seen (and
@@ -241,7 +244,7 @@ TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz)
       else
       {
         // otherwise, create a new obligation of the corresponding sygus type
-        newVar = nm->mkSkolem("sygus_rcons", stn);
+        newVar = sm->mkDummySkolem("sygus_rcons", stn);
         d_obInfo.emplace(newVar, candOb.second);
         d_stnInfo[stn].setBuiltinToOb(candOb.second, newVar);
         // if the candidate obligation is a constant and the grammar allows
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 179798222..47ead92c1 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -433,6 +434,7 @@ Node SygusRepairConst::getFoQuery(Node body,
                                   const std::vector<Node>& sk_vars)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Trace("sygus-repair-const") << "  Substitute skeletons..." << std::endl;
   body = body.substitute(candidates.begin(),
                          candidates.end(),
@@ -451,7 +453,7 @@ Node SygusRepairConst::getFoQuery(Node body,
     if (itf == d_sk_to_fo.end())
     {
       TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
-      Node sk_fov = nm->mkSkolem("k", builtinType);
+      Node sk_fov = sm->mkDummySkolem("k", builtinType);
       d_sk_to_fo[v] = sk_fov;
       d_fo_to_sk[sk_fov] = v;
       Trace("sygus-repair-const-debug")
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index c3cff70d9..eade6b38e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 
+#include "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -133,6 +134,7 @@ Node SygusUnifRl::purifyLemma(Node n,
   bool childChanged = false;
   std::vector<Node> children;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   for (unsigned i = 0; i < size; ++i)
   {
     if (i == 0 && fapp)
@@ -182,10 +184,10 @@ Node SygusUnifRl::purifyLemma(Node n,
       // Build purified head with fresh skolem and recreate node
       std::stringstream ss;
       ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
-      Node new_f = nm->mkSkolem(ss.str(),
-                                nb[0].getType(),
-                                "head of unif evaluation point",
-                                NodeManager::SKOLEM_EXACT_NAME);
+      Node new_f = sm->mkDummySkolem(ss.str(),
+                                     nb[0].getType(),
+                                     "head of unif evaluation point",
+                                     NodeManager::SKOLEM_EXACT_NAME);
       // Adds new enumerator to map from candidate
       Trace("sygus-unif-rl-purify")
           << "...new enum " << new_f << " for candidate " << nb[0] << "\n";
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 24bcb1eab..fb93d26a9 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
+#include "expr/skolem_manager.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_unif.h"
@@ -172,6 +173,7 @@ void SygusUnifStrategy::registerStrategyPoint(Node et,
 void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   if (d_tinfo.find(tn) == d_tinfo.end())
   {
     // register type
@@ -194,7 +196,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
   std::map<EnumRole, Node>::iterator iten = eti.d_enum.find(erole);
   if (iten == eti.d_enum.end())
   {
-    ee = nm->mkSkolem("ee", tn);
+    ee = sm->mkDummySkolem("ee", tn);
     eti.d_enum[erole] = ee;
     Trace("sygus-unif-debug")
         << "...enumerator " << ee << " for " << tn.getDType().getName()
@@ -245,7 +247,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
     {
       TypeNode ttn = dt[j][k].getRangeType();
-      Node kv = nm->mkSkolem("ut", ttn);
+      Node kv = sm->mkDummySkolem("ut", ttn);
       sks.push_back(kv);
       cop_to_sks[cop].push_back(kv);
       sktns.push_back(ttn);
@@ -303,7 +305,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
                                    << std::endl;
         Node esk = nm->mkNode(DT_SYGUS_EVAL, echildren);
         vs.push_back(esk);
-        Node tvar = nm->mkSkolem("templ", esk.getType());
+        Node tvar = sm->mkDummySkolem("templ", esk.getType());
         templ_var_index[tvar] = k;
         Trace("sygus-unif-debug2") << "* template inference : looking for "
                                    << tvar << " for arg " << k << std::endl;
@@ -574,7 +576,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
           if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end())
           {
             // it is templated, allocate a fresh variable
-            et = nm->mkSkolem("et", ct);
+            et = sm->mkDummySkolem("et", ct);
             Trace("sygus-unif-debug") << "...enumerate " << et << " of type "
                                       << ct.getDType().getName();
             Trace("sygus-unif-debug") << " for arg " << j << " of "
diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp
index 6c14aaa80..4d1d0ab1d 100644
--- a/src/theory/quantifiers/sygus/sygus_utils.cpp
+++ b/src/theory/quantifiers/sygus/sygus_utils.cpp
@@ -17,6 +17,7 @@
 #include <sstream>
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 
@@ -42,8 +43,9 @@ Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
 {
   Assert(!fs.empty());
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   SygusAttribute ca;
-  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
+  Node sygusVar = sm->mkDummySkolem("sygus", nm->booleanType());
   sygusVar.setAttribute(ca, true);
   std::vector<Node> ipls{nm->mkNode(INST_ATTRIBUTE, sygusVar)};
   // insert the remaining instantiation attributes
@@ -65,6 +67,7 @@ Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
 {
   Assert(!fs.empty());
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::vector<Node> iattrs;
   // take existing properties, without the previous solves
   SygusSolutionAttribute ssa;
@@ -72,7 +75,7 @@ Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
   for (size_t i = 0, nsolved = solvedf.size(); i < nsolved; i++)
   {
     Node eq = solvedf.getEquality(i);
-    Node var = nm->mkSkolem("solved", nm->booleanType());
+    Node var = sm->mkDummySkolem("solved", nm->booleanType());
     var.setAttribute(ssa, eq);
     Node ipv = nm->mkNode(INST_ATTRIBUTE, var);
     iattrs.push_back(ipv);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index f7566e7a2..f63941b1c 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
 #include "base/configuration.h"
+#include "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
@@ -29,9 +30,9 @@
 #include "theory/quantifiers/sygus/enum_stream_substitution.h"
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 #include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
-#include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_pbe.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
@@ -102,9 +103,10 @@ void SynthConjecture::assign(Node q)
   Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl;
   d_quant = q;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
 
   // initialize the guard
-  d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
+  d_feasible_guard = sm->mkDummySkolem("G", nm->booleanType());
   d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
   d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard);
   AlwaysAssert(!d_feasible_guard.isNull());
@@ -170,8 +172,7 @@ void SynthConjecture::assign(Node q)
   for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++)
   {
     vars.push_back(d_embed_quant[0][i]);
-    Node e =
-        NodeManager::currentNM()->mkSkolem("e", d_embed_quant[0][i].getType());
+    Node e = sm->mkDummySkolem("e", d_embed_quant[0][i].getType());
     d_candidates.push_back(e);
   }
   Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
@@ -460,6 +461,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   }
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
 
   // check the side condition if we constructed a candidate
   if (constructed_cand)
@@ -540,7 +542,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     {
       for (const Node& v : inst[0][0])
       {
-        Node sk = nm->mkSkolem("rsk", v.getType());
+        Node sk = sm->mkDummySkolem("rsk", v.getType());
         sks.push_back(sk);
         vars.push_back(v);
         Trace("cegqi-check-debug")
diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp
index 875b25370..02d287fdf 100644
--- a/src/theory/quantifiers/sygus/template_infer.cpp
+++ b/src/theory/quantifiers/sygus/template_infer.cpp
@@ -14,6 +14,7 @@
  **/
 #include "theory/quantifiers/sygus/template_infer.h"
 
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_utils.h"
@@ -84,6 +85,7 @@ void SygusTemplateInfer::initialize(Node q)
   }
   Assert(prog == q[0][0]);
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   // map the program back via non-single invocation map
   std::vector<Node> prog_templ_vars;
   d_ti.getVariables(prog_templ_vars);
@@ -98,7 +100,7 @@ void SygusTemplateInfer::initialize(Node q)
   {
     atn = atn.getRangeType();
   }
-  d_templ_arg[prog] = nm->mkSkolem("I", atn);
+  d_templ_arg[prog] = sm->mkDummySkolem("I", atn);
 
   // construct template
   Node templ;
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 34a81467a..e4ecee72f 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -18,6 +18,7 @@
 
 #include "base/check.h"
 #include "expr/dtype_cons.h"
+#include "expr/skolem_manager.h"
 #include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
@@ -165,18 +166,19 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
   {
     SygusTypeInfo& ti = getTypeInfo(tn);
     int anyC = ti.getAnyConstantConsNum();
+    NodeManager* nm = NodeManager::currentNM();
     Node k;
     if (anyC == -1)
     {
-      k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy");
+      SkolemManager* sm = nm->getSkolemManager();
+      k = sm->mkDummySkolem("sy", tn, "sygus proxy");
       SygusPrintProxyAttribute spa;
       k.setAttribute(spa, c);
     }
     else
     {
       const DType& dt = tn.getDType();
-      k = NodeManager::currentNM()->mkNode(
-          APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c);
+      k = nm->mkNode(APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c);
     }
     d_proxy_vars[tn][c] = k;
     return k;
@@ -562,8 +564,9 @@ void TermDbSygus::registerEnumerator(Node e,
   // populate a pool of terms, or (some cases) of when it is actively generated.
   if (isActiveGen || erole == ROLE_ENUM_POOL)
   {
+    SkolemManager* sm = nm->getSkolemManager();
     // make the guard
-    Node ag = nm->mkSkolem("eG", nm->booleanType());
+    Node ag = sm->mkDummySkolem("eG", nm->booleanType());
     // must ensure it is a literal immediately here
     ag = d_qstate.getValuation().ensureLiteral(ag);
     // must ensure that it is asserted as a literal before we begin solving
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
index 7ee2f2ec6..eb2f0f739 100644
--- a/src/theory/quantifiers/sygus/transition_inference.cpp
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/sygus/transition_inference.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
@@ -197,6 +198,7 @@ void TransitionInference::process(Node n, Node f)
 void TransitionInference::process(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   d_complete = true;
   d_trivial = true;
   std::vector<Node> n_check;
@@ -276,7 +278,7 @@ void TransitionInference::process(Node n)
       {
         for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; j++)
         {
-          Node v = nm->mkSkolem(
+          Node v = sm->mkDummySkolem(
               "ir", next[j].getType(), "template inference rev argument");
           d_prime_vars.push_back(v);
         }
@@ -426,9 +428,11 @@ bool TransitionInference::processDisjunct(
       d_func = op;
       Trace("cegqi-inv-debug") << "Use " << op << " with args ";
       NodeManager* nm = NodeManager::currentNM();
+      SkolemManager* sm = nm->getSkolemManager();
       for (const Node& l : lit)
       {
-        Node v = nm->mkSkolem("i", l.getType(), "template inference argument");
+        Node v =
+            sm->mkDummySkolem("i", l.getType(), "template inference argument");
         d_vars.push_back(v);
         Trace("cegqi-inv-debug") << v << " ";
       }
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 81dc5cecb..e394eab26 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -18,6 +18,7 @@
 #include <unordered_set>
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -462,7 +463,8 @@ Node SygusInst::getCeLiteral(Node q)
   }
 
   NodeManager* nm = NodeManager::currentNM();
-  Node sk = nm->mkSkolem("CeLiteral", nm->booleanType());
+  SkolemManager* sm = nm->getSkolemManager();
+  Node sk = sm->mkDummySkolem("CeLiteral", nm->booleanType());
   Node lit = d_qstate.getValuation().ensureLiteral(sk);
   d_ce_lits[q] = lit;
   return lit;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 64c2fda76..517c3ac24 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/term_database.h"
 
+#include "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
@@ -154,11 +155,11 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
       d_type_fv.find(tn);
   if (it == d_type_fv.end())
   {
+    SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
     std::stringstream ss;
     ss << language::SetLanguage(options::outputLanguage());
     ss << "e_" << tn;
-    Node k = NodeManager::currentNM()->mkSkolem(
-        ss.str(), tn, "is a termDb fresh variable");
+    Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable");
     Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
                    << std::endl;
     if (options::instMaxLevel() != -1)
@@ -168,10 +169,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
     d_type_fv[tn] = k;
     return k;
   }
-  else
-  {
-    return it->second;
-  }
+  return it->second;
 }
 
 Node TermDb::getMatchOperator( Node n ) {
@@ -468,6 +466,7 @@ void TermDb::addTermHo(Node n)
     return;
   }
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Node curr = n;
   std::vector<Node> args;
   while (curr.getKind() == HO_APPLY)
@@ -481,9 +480,9 @@ void TermDb::addTermHo(Node n)
       Node psk;
       if (itp == d_ho_fun_op_purify.end())
       {
-        psk = nm->mkSkolem("pfun",
-                           curr.getType(),
-                           "purify for function operator term indexing");
+        psk = sm->mkDummySkolem("pfun",
+                                curr.getType(),
+                                "purify for function operator term indexing");
         d_ho_fun_op_purify[curr] = psk;
         // we do not add it to d_ops since it is an internal operator
       }
@@ -1224,8 +1223,9 @@ Node TermDb::getHoTypeMatchPredicate(TypeNode tn)
     return ithp->second;
   }
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
-  Node k = nm->mkSkolem("U", ptn, "predicate to force higher-order types");
+  Node k = sm->mkDummySkolem("U", ptn, "predicate to force higher-order types");
   d_ho_type_match_pred[tn] = k;
   return k;
 }