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.
author: Andrew Reynolds <andrew.j.reynolds@gmail.com> 2021-04-07 13:36:15 -0500
committer: GitHub <noreply@github.com> 2021-04-07 18:36:15 +0000
commit: 04a494e251a8cc2c90bb429e2858f1c4eb8f88ff (patch)
tree: 03b1a5792f2f6ca5537353b86682f427090668da
parent: 5059658ee0d6fc65e4cb1652c605895d016cd274 (diff)
92 files changed, 703 insertions, 907 deletions
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 3302be018..48c0e9f00 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "expr/type_matcher.h"
 
 using namespace cvc5::kind;
@@ -882,10 +883,11 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const
   NodeManager* nm = NodeManager::currentNM();
   std::stringstream ss;
   ss << "sel_" << index;
-  s = nm->mkSkolem(ss.str(),
-                   nm->mkSelectorType(dtt, t),
-                   "is a shared selector",
-                   NodeManager::SKOLEM_NO_NOTIFY);
+  SkolemManager* sm = nm->getSkolemManager();
+  s = sm->mkDummySkolem(ss.str(),
+                        nm->mkSelectorType(dtt, t),
+                        "is a shared selector",
+                        NodeManager::SKOLEM_NO_NOTIFY);
   d_sharedSel[dtt][t][index] = s;
   Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t
                          << std::endl;
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index ce15c7ede..927c48dda 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -15,6 +15,7 @@
 
 #include "expr/dtype.h"
 #include "expr/node_manager.h"
+#include "expr/skolem_manager.h"
 #include "expr/type_matcher.h"
 #include "options/datatypes_options.h"
 
@@ -45,8 +46,8 @@ void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType)
   // create the proper selector type)
   Assert(!isResolved());
   Assert(!selectorType.isNull());
-
-  Node type = NodeManager::currentNM()->mkSkolem(
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node type = sm->mkDummySkolem(
       "unresolved_" + selectorName,
       selectorType,
       "is an unresolved selector type placeholder",
@@ -505,6 +506,7 @@ bool DTypeConstructor::resolve(
                      << std::endl;
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   size_t index = 0;
   std::vector<TypeNode> argTypes;
   Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl;
@@ -523,7 +525,7 @@ bool DTypeConstructor::resolve(
       {
         Trace("datatypes-init") << "  ...self selector" << std::endl;
         range = self;
-        arg->d_selector = nm->mkSkolem(
+        arg->d_selector = sm->mkDummySkolem(
             argName,
             nm->mkSelectorType(self, self),
             "is a selector",
@@ -544,7 +546,7 @@ bool DTypeConstructor::resolve(
         {
           Trace("datatypes-init") << "  ...resolved selector" << std::endl;
           range = (*j).second;
-          arg->d_selector = nm->mkSkolem(
+          arg->d_selector = sm->mkDummySkolem(
               argName,
               nm->mkSelectorType(self, range),
               "is a selector",
@@ -574,7 +576,7 @@ bool DTypeConstructor::resolve(
       }
       Trace("datatypes-init")
           << "  ...range after parametric substitution " << range << std::endl;
-      arg->d_selector = nm->mkSkolem(
+      arg->d_selector = sm->mkDummySkolem(
           argName,
           nm->mkSelectorType(self, range),
           "is a selector",
@@ -603,12 +605,12 @@ bool DTypeConstructor::resolve(
   // The name of the tester variable does not matter, it is only used
   // internally.
   std::string testerName("is_" + d_name);
-  d_tester = nm->mkSkolem(
+  d_tester = sm->mkDummySkolem(
       testerName,
       nm->mkTesterType(self),
       "is a tester",
       NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
-  d_constructor = nm->mkSkolem(
+  d_constructor = sm->mkDummySkolem(
       getName(),
       nm->mkConstructorType(argTypes, self),
       "is a constructor",
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index a72eada23..465ddf588 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -87,6 +87,7 @@ class NodeManager
   friend class api::Solver;
   friend class expr::NodeValue;
   friend class expr::TypeChecker;
+  friend class SkolemManager;
 
   friend class NodeBuilder;
   friend class NodeManagerScope;
@@ -366,7 +367,7 @@ class NodeManager
    * lookup is done on the name.  If you mkVar("a", type) and then
    * mkVar("a", type) again, you have two variables.  The NodeManager
    * version of this is private to avoid internal uses of mkVar() from
-   * within CVC4.  Such uses should employ mkSkolem() instead.
+   * within CVC4.  Such uses should employ SkolemManager::mkSkolem() instead.
    */
   Node mkVar(const std::string& name, const TypeNode& type);
   Node* mkVarPtr(const std::string& name, const TypeNode& type);
@@ -375,6 +376,19 @@ class NodeManager
   Node mkVar(const TypeNode& type);
   Node* mkVarPtr(const TypeNode& type);
 
+  /**
+   * Create a skolem constant with the given name, type, and comment. For
+   * details, see SkolemManager::mkDummySkolem, which calls this method.
+   *
+   * This method is intentionally private. To create skolems, one should
+   * call a method from SkolemManager for allocating a skolem in a standard
+   * way, or otherwise use SkolemManager::mkDummySkolem.
+   */
+  Node mkSkolem(const std::string& prefix,
+                const TypeNode& type,
+                const std::string& comment = "",
+                int flags = SKOLEM_DEFAULT);
+
  public:
   explicit NodeManager();
   ~NodeManager();
@@ -578,27 +592,6 @@ class NodeManager
     SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
   };                         /* enum SkolemFlags */
 
-  /**
-   * Create a skolem constant with the given name, type, and comment.
-   *
-   * @param prefix the name of the new skolem variable is the prefix
-   * appended with a unique ID.  This way a family of skolem variables
-   * can be made with unique identifiers, used in dump, tracing, and
-   * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
-   * a unique ID appended and use prefix as the name.
-   *
-   * @param type the type of the skolem variable to create
-   *
-   * @param comment a comment for dumping output; if declarations are
-   * being dumped, this is included in a comment before the declaration
-   * and can be quite useful for debugging
-   *
-   * @param flags an optional mask of bits from SkolemFlags to control
-   * mkSkolem() behavior
-   */
-  Node mkSkolem(const std::string& prefix, const TypeNode& type,
-                const std::string& comment = "", int flags = SKOLEM_DEFAULT);
-
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
 
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index a823d5b60..8ca8810b1 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -204,6 +204,14 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal)
   return it->second;
 }
 
+Node SkolemManager::mkDummySkolem(const std::string& prefix,
+                                  const TypeNode& type,
+                                  const std::string& comment,
+                                  int flags)
+{
+  return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
+}
+
 Node SkolemManager::mkBooleanTermVariable(Node t)
 {
   return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 1295b2249..6cebee5d9 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -228,6 +228,28 @@ class SkolemManager
                         TypeNode tn,
                         Node cacheVal = Node::null());
   /**
+   * Create a skolem constant with the given name, type, and comment. This
+   * should only be used if the definition of the skolem does not matter.
+   * The definition of a skolem matters e.g. when the skolem is used in a
+   * proof.
+   *
+   * @param prefix the name of the new skolem variable is the prefix
+   * appended with a unique ID.  This way a family of skolem variables
+   * can be made with unique identifiers, used in dump, tracing, and
+   * debugging output.  Use SKOLEM_EXACT_NAME flag if you don't want
+   * a unique ID appended and use prefix as the name.
+   * @param type the type of the skolem variable to create
+   * @param comment a comment for dumping output; if declarations are
+   * being dumped, this is included in a comment before the declaration
+   * and can be quite useful for debugging
+   * @param flags an optional mask of bits from SkolemFlags to control
+   * mkSkolem() behavior
+   */
+  Node mkDummySkolem(const std::string& prefix,
+                     const TypeNode& type,
+                     const std::string& comment = "",
+                     int flags = NodeManager::SKOLEM_DEFAULT);
+  /**
    * Make Boolean term variable for term t. This is a special case of
    * mkPurifySkolem above, where the returned term has kind
    * BOOLEAN_TERM_VARIABLE.
diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp
index c2138499b..8c1d67c47 100644
--- a/src/expr/subs.cpp
+++ b/src/expr/subs.cpp
@@ -16,6 +16,7 @@
 
 #include <sstream>
 
+#include "expr/skolem_manager.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {
@@ -44,8 +45,9 @@ Node Subs::getSubs(Node v) const
 
 void Subs::add(Node v)
 {
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
   // default, use a fresh skolem of the same type
-  Node s = NodeManager::currentNM()->mkSkolem("sk", v.getType());
+  Node s = sm->mkDummySkolem("sk", v.getType());
   add(v, s);
 }
 
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index 929c8a97c..82585eabe 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -15,6 +15,7 @@
 #include "expr/sygus_datatype.h"
 
 #include <sstream>
+#include "expr/skolem_manager.h"
 
 using namespace cvc5::kind;
 
@@ -38,8 +39,9 @@ void SygusDatatype::addConstructor(Node op,
 
 void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
 {
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
   // add an "any constant" proxy variable
-  Node av = NodeManager::currentNM()->mkSkolem("_any_constant", tn);
+  Node av = sm->mkDummySkolem("_any_constant", tn);
   // mark that it represents any constant
   SygusAnyConstAttribute saca;
   av.setAttribute(saca, true);
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index a19994ad9..525d0b243 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -27,6 +27,7 @@
 
 #include "base/check.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
@@ -105,10 +106,12 @@ void storeFunctionAndAddLemmas(TNode func,
   if (set.find(term) == set.end())
   {
     TypeNode tn = term.getType();
-    Node skolem = nm->mkSkolem("SKOLEM$$",
-                               tn,
-                               "is a variable created by the ackermannization "
-                               "preprocessing pass");
+    SkolemManager* sm = nm->getSkolemManager();
+    Node skolem =
+        sm->mkDummySkolem("SKOLEM$$",
+                          tn,
+                          "is a variable created by the ackermannization "
+                          "preprocessing pass");
     for (const auto& t : set)
     {
       addLemmaForPair(t, term, func, assertions, nm);
@@ -206,12 +209,13 @@ void collectUSortsToBV(const std::unordered_set<TNode, TNodeHashFunction>& vars,
                        SubstitutionMap& usVarsToBVVars)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
 
   for (TNode var : vars)
   {
     TypeNode type = var.getType();
     size_t size = getBVSkolemSize(usortCardinality.at(type));
-    Node skolem = nm->mkSkolem(
+    Node skolem = sm->mkDummySkolem(
         "BVSKOLEM$$",
         nm->mkBitVectorType(size),
         "a variable created by the ackermannization "
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index c5f24c15c..28dcc1949 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -25,6 +25,7 @@
 
 #include "expr/node.h"
 #include "expr/node_traversal.h"
+#include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
@@ -702,6 +703,7 @@ Node BVToInt::translateWithChildren(Node original,
 
 Node BVToInt::translateNoChildren(Node original)
 {
+  SkolemManager* sm = d_nm->getSkolemManager();
   Node translation;
   Assert(original.isVar() || original.isConst());
   if (original.isVar())
@@ -722,11 +724,11 @@ Node BVToInt::translateNoChildren(Node original)
         // New integer variables  that are not bound (symbolic constants)
         // are added together with range constraints induced by the 
         // bit-width of the original bit-vector variables.
-        Node newVar = d_nm->mkSkolem("__bvToInt_var",
-                                     d_nm->integerType(),
-                                     "Variable introduced in bvToInt "
-                                     "pass instead of original variable "
-                                         + original.toString());
+        Node newVar = sm->mkDummySkolem("__bvToInt_var",
+                                        d_nm->integerType(),
+                                        "Variable introduced in bvToInt "
+                                        "pass instead of original variable "
+                                            + original.toString());
         uint64_t bvsize = original.getType().getBitVectorSize();
         translation = newVar;
         d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize));
@@ -783,9 +785,10 @@ Node BVToInt::translateFunctionSymbol(Node bvUF)
   {
     intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d);
   }
+  SkolemManager* sm = d_nm->getSkolemManager();
   ostringstream os;
   os << "__bvToInt_fun_" << bvUF << "_int";
-  intUF = d_nm->mkSkolem(
+  intUF = sm->mkDummySkolem(
       os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function");
   // introduce a `define-fun` in the smt-engine to keep
   // the correspondence between the original
diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index c6ea0ee27..8d1fed4a3 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -16,6 +16,7 @@
 
 #include <sstream>
 
+#include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
@@ -92,6 +93,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess)
   std::map<int, Node> subs_head;
   // first pass : find defined functions, transform quantifiers
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   for (size_t i = 0, asize = assertions.size(); i < asize; i++)
   {
     Node n = QuantAttributes::getFunDefHead(assertions[i]);
@@ -129,8 +131,8 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess)
           TypeNode typ = nm->mkFunctionType(iType, n[j].getType());
           std::stringstream ssf;
           ssf << f << "_arg_" << j;
-          d_input_arg_inj[f].push_back(
-              nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf"));
+          d_input_arg_inj[f].push_back(sm->mkDummySkolem(
+              ssf.str(), typ, "op created during fun def fmf"));
         }
 
         // construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 1bf980c49..619f3cfe2 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -19,6 +19,7 @@
 #include <sstream>
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
@@ -36,6 +37,7 @@ HoElim::HoElim(PreprocessingPassContext* preprocContext)
 Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
   std::vector<Node> visit;
   TNode cur;
@@ -90,7 +92,7 @@ Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda)
         }
         TypeNode rangeType = cur.getType().getRangeType();
         TypeNode nft = nm->mkFunctionType(ftypes, rangeType);
-        Node nf = nm->mkSkolem("ll", nft);
+        Node nf = sm->mkDummySkolem("ll", nft);
         Trace("ho-elim-ll")
             << "...introduce: " << nf << " of type " << nft << std::endl;
         newLambda[nf] = nlambda;
@@ -151,6 +153,7 @@ Node HoElim::eliminateHo(Node n)
 {
   Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::unordered_map<Node, Node, NodeHashFunction>::iterator it;
   std::map<Node, Node> preReplace;
   std::map<Node, Node>::iterator itr;
@@ -187,7 +190,7 @@ Node HoElim::eliminateHo(Node n)
             }
             else
             {
-              ret = nm->mkSkolem("k", ut);
+              ret = sm->mkDummySkolem("k", ut);
             }
             // must get the ho apply to ensure extensionality is applied
             Node hoa = getHoApplyUf(tn);
@@ -260,7 +263,7 @@ Node HoElim::eliminateHo(Node n)
             {
               Assert(!childrent.empty());
               TypeNode newFType = nm->mkFunctionType(childrent, cur.getType());
-              retOp = nm->mkSkolem("rf", newFType);
+              retOp = sm->mkDummySkolem("rf", newFType);
               d_visited_op[op] = retOp;
             }
             else
@@ -485,12 +488,13 @@ Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr)
   if (it == d_hoApplyUf.end())
   {
     NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
 
     std::vector<TypeNode> hoTypeArgs;
     hoTypeArgs.push_back(tnf);
     hoTypeArgs.push_back(tna);
     TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr);
-    Node k = NodeManager::currentNM()->mkSkolem("ho", tnh);
+    Node k = sm->mkDummySkolem("ho", tnh);
     d_hoApplyUf[tnf] = k;
     return k;
   }
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index ef9b261b0..1f223ad4f 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -24,6 +24,7 @@
 
 #include "expr/node.h"
 #include "expr/node_traversal.h"
+#include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
@@ -102,13 +103,14 @@ Node intToBV(TNode n, NodeMap& cache)
   AlwaysAssert(size > 0);
   AlwaysAssert(!options::incrementalSolving());
 
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   NodeMap binaryCache;
   Node n_binary = intToBVMakeBinary(n, binaryCache);
 
   for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER,
            [&cache](TNode nn) { return cache.count(nn) > 0; }))
   {
-    NodeManager* nm = NodeManager::currentNM();
     if (current.getNumChildren() > 0)
     {
       // Not a leaf
@@ -208,9 +210,9 @@ Node intToBV(TNode n, NodeMap& cache)
       {
         if (current.getType() == nm->integerType())
         {
-          result = nm->mkSkolem("__intToBV_var",
-                                nm->mkBitVectorType(size),
-                                "Variable introduced in intToBV pass");
+          result = sm->mkDummySkolem("__intToBV_var",
+                                     nm->mkBitVectorType(size),
+                                     "Variable introduced in intToBV pass");
         }
       }
       else if (current.isConst())
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index f3c4d2e12..9ca58c334 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "expr/node_self_iterator.h"
+#include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
@@ -201,6 +202,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
   SubstitutionMap& top_level_substs = tlsm.get();
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
   Node trueNode = nm->mkConst(true);
 
@@ -522,7 +524,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
             {
               stringstream ss;
               ss << "mipvar_" << *ii;
-              Node newVar = nm->mkSkolem(
+              Node newVar = sm->mkDummySkolem(
                   ss.str(),
                   nm->integerType(),
                   "a variable introduced due to scrubbing a miplib encoding",
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index 838a2a767..f07c5419f 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/nl_ext_purify.h"
 
+#include "expr/skolem_manager.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 
@@ -32,6 +33,8 @@ Node NlExtPurify::purifyNlTerms(TNode n,
                                 std::vector<Node>& var_eq,
                                 bool beneathMult)
 {
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   if (beneathMult)
   {
     NodeMap::iterator find = bcache.find(n);
@@ -69,10 +72,9 @@ Node NlExtPurify::purifyNlTerms(TNode n,
       else
       {
         // new variable
-        ret = NodeManager::currentNM()->mkSkolem(
-            "__purifyNl_var",
-            n.getType(),
-            "Variable introduced in purifyNl pass");
+        ret = sm->mkDummySkolem("__purifyNl_var",
+                                n.getType(),
+                                "Variable introduced in purifyNl pass");
         Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
         var_eq.push_back(np.eqNode(ret));
         Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np
@@ -92,7 +94,7 @@ Node NlExtPurify::purifyNlTerms(TNode n,
       }
       if (childChanged)
       {
-        ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+        ret = nm->mkNode(n.getKind(), children);
       }
     }
   }
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 8251183dd..6c97936b0 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -18,6 +18,7 @@
 
 #include <vector>
 
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
@@ -323,6 +324,8 @@ bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map<
 
 bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
   Trace("macros-debug") << "  process " << n << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   if( n.getKind()==NOT ){
     return process( n[0], !pol, args, f );
   }else if( n.getKind()==AND || n.getKind()==OR ){
@@ -335,11 +338,14 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
     if( isBoundVarApplyUf( n ) ){
       Node op = n.getOperator();
       if( d_macro_defs.find( op )==d_macro_defs.end() ){
-        Node n_def = NodeManager::currentNM()->mkConst( pol );
+        Node n_def = nm->mkConst(pol);
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           std::stringstream ss;
           ss << "mda_" << op << "";
-          Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" );
+          Node v =
+              sm->mkDummySkolem(ss.str(),
+                                n[i].getType(),
+                                "created during macro definition recognition");
           d_macro_basis[op].push_back( v );
         }
         //contains no ops
@@ -392,7 +398,10 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
                     for( size_t a=0; a<m.getNumChildren(); a++ ){
                       std::stringstream ss;
                       ss << "mda_" << op << "";
-                      Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
+                      Node v = sm->mkDummySkolem(
+                          ss.str(),
+                          m[a].getType(),
+                          "created during macro definition recognition");
                       d_macro_basis[op].push_back( v );
                     }
                   }
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index c80d55d3d..d8993ff1b 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -18,6 +18,7 @@
 
 #include <string>
 
+#include "expr/skolem_manager.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "theory/arith/arith_msum.h"
@@ -42,6 +43,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
   else
   {
     NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     Node ret = n;
     if (n.getNumChildren() > 0)
     {
@@ -178,9 +180,10 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
         }
         else if (n.isVar())
         {
-          ret = nm->mkSkolem("__realToIntInternal_var",
-                             nm->integerType(),
-                             "Variable introduced in realToIntInternal pass");
+          ret = sm->mkDummySkolem(
+              "__realToIntInternal_var",
+              nm->integerType(),
+              "Variable introduced in realToIntInternal pass");
           var_eq.push_back(n.eqNode(ret));
           // ensure that the original variable is defined to be the returned
           // one, which is important for models and for incremental solving.
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index 8c130768d..0c5ca9af9 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -20,6 +20,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/skolem_manager.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/rewriter.h"
@@ -41,6 +42,8 @@ Node preSkolemEmp(Node n,
   std::map<Node, Node>::iterator it = visited[pol].find(n);
   if (it == visited[pol].end())
   {
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol
                             << std::endl;
     Node ret = n;
@@ -50,14 +53,13 @@ Node preSkolemEmp(Node n,
       {
         TypeNode tnx = n[0].getType();
         TypeNode tny = n[1].getType();
-        Node x = NodeManager::currentNM()->mkSkolem(
-            "ex", tnx, "skolem location for negated emp");
-        Node y = NodeManager::currentNM()->mkSkolem(
-            "ey", tny, "skolem data for negated emp");
-        return NodeManager::currentNM()
+        Node x =
+            sm->mkDummySkolem("ex", tnx, "skolem location for negated emp");
+        Node y = sm->mkDummySkolem("ey", tny, "skolem data for negated emp");
+        return nm
             ->mkNode(kind::SEP_STAR,
-                     NodeManager::currentNM()->mkNode(kind::SEP_PTO, x, y),
-                     NodeManager::currentNM()->mkConst(true))
+                     nm->mkNode(kind::SEP_PTO, x, y),
+                     nm->mkConst(true))
             .negate();
       }
     }
@@ -83,7 +85,7 @@ Node preSkolemEmp(Node n,
       }
       if (childChanged)
       {
-        return NodeManager::currentNM()->mkNode(n.getKind(), children);
+        return nm->mkNode(n.getKind(), children);
       }
     }
     visited[pol][n] = ret;
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 9a9aaa366..2c01bd6d2 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -19,6 +19,7 @@
 #include "preprocessing/passes/unconstrained_simplifier.h"
 
 #include "expr/dtype.h"
+#include "expr/skolem_manager.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/logic_exception.h"
@@ -126,7 +127,8 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
 
 Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
 {
-  Node n = NodeManager::currentNM()->mkSkolem(
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node n = sm->mkDummySkolem(
       "unconstrained",
       t,
       "a new var introduced because of unconstrained variable "
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 7826c207b..5433368fa 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -21,6 +21,7 @@
 
 #include <utility>
 
+#include "expr/skolem_manager.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/passes/rewrite.h"
 #include "smt/smt_statistics_registry.h"
@@ -353,7 +354,8 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed)
   else
   {
     NodeManager* nm = NodeManager::currentNM();
-    Node skolem = nm->mkSkolem("compress", nm->booleanType());
+    SkolemManager* sm = nm->getSkolemManager();
+    Node skolem = sm->mkDummySkolem("compress", nm->booleanType());
     d_compressed[rewritten] = skolem;
     d_compressed[original] = skolem;
     d_compressed[compressed] = skolem;
@@ -1386,13 +1388,11 @@ Node ITESimplifier::getSimpVar(TypeNode t)
   {
     return (*it).second;
   }
-  else
-  {
-    Node var = NodeManager::currentNM()->mkSkolem(
-        "iteSimp", t, "is a variable resulting from ITE simplification");
-    d_simpVars[t] = var;
-    return var;
-  }
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node var = sm->mkDummySkolem(
+      "iteSimp", t, "is a variable resulting from ITE simplification");
+  d_simpVars[t] = var;
+  return var;
 }
 
 Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index ddc20ee8d..436d6618d 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -45,6 +45,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
         "Expecting a quantified formula as argument to get-qe.");
   }
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   // ensure the body is rewritten
   q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
   // do nested quantifier elimination if necessary
@@ -53,7 +54,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
                   << q << std::endl;
   // tag the quantified formula with the quant-elim attribute
   TypeNode t = nm->booleanType();
-  Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
+  Node n_attr = sm->mkDummySkolem("qe", t, "Auxiliary variable for qe attr.");
   std::vector<Node> node_values;
   TheoryEngine* te = d_smtSolver.getTheoryEngine();
   Assert(te != nullptr);
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 27e16ccc6..022691a12 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -17,6 +17,7 @@
 #include <sstream>
 
 #include "expr/dtype.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
@@ -261,6 +262,7 @@ void SygusSolver::printSynthSolution(std::ostream& out)
 void SygusSolver::checkSynthSolution(Assertions& as)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Notice() << "SygusSolver::checkSynthSolution(): checking synthesis solution"
            << std::endl;
   std::map<Node, std::map<Node, Node>> sol_map;
@@ -363,7 +365,7 @@ void SygusSolver::checkSynthSolution(Assertions& as)
         vars.push_back(conj[1][0][j]);
         std::stringstream ss;
         ss << "sk_" << j;
-        skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType()));
+        skos.push_back(sm->mkDummySkolem(ss.str(), conj[1][0][j].getType()));
         Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
                                  << skos.back() << "\n";
       }
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 218fdf179..64309ad16 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -20,6 +20,7 @@
 #include <ostream>
 
 #include "base/output.h"
+#include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "preprocessing/util/ite_utilities.h"
 #include "theory/arith/arith_utilities.h"
@@ -441,10 +442,11 @@ bool ArithIteUtils::solveBinOr(TNode binor){
         // a: (sel = otherL) or (sel = otherR), otherL-otherR = c
 
         NodeManager* nm = NodeManager::currentNM();
+        SkolemManager* sm = nm->getSkolemManager();
 
         Node cnd = findIteCnd(binor[0], binor[1]);
 
-        Node sk = nm->mkSkolem("deor", nm->booleanType());
+        Node sk = sm->mkDummySkolem("deor", nm->booleanType());
         Node ite = sk.iteNode(otherL, otherR);
         d_skolems.insert(sk, cnd);
         addSubstitution(sel, ite);
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index bc35c6941..c9f572364 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -49,20 +49,6 @@ inline Node mkBoolNode(bool b){
   return NodeManager::currentNM()->mkConst<bool>(b);
 }
 
-inline Node mkIntSkolem(const std::string& name){
-  return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType());
-}
-
-inline Node mkRealSkolem(const std::string& name){
-  return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType());
-}
-
-inline Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
-  NodeManager* currNM = NodeManager::currentNM();
-  TypeNode functionType = currNM->mkFunctionType(dom, range);
-  return currNM->mkSkolem(name, functionType);
-}
-
 /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
 inline bool isRelationOperator(Kind k){
   using namespace kind;
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index b2c48163f..0043ccae6 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -18,6 +18,7 @@
 #include "theory/arith/callbacks.h"
 
 #include "expr/proof_node.h"
+#include "expr/skolem_manager.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/arith/theory_arith_private.h"
 
@@ -46,7 +47,9 @@ TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
 : d_ta(ta)
 {}
 ArithVar TempVarMalloc::request(){
-  Node skolem = mkRealSkolem("tmpVar");
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  Node skolem = sm->mkDummySkolem("tmpVar", nm->realType());
   return d_ta.requestArithVar(skolem, false, true);
 }
 void TempVarMalloc::release(ArithVar v){
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 3825a3a42..6ceab1933 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -18,6 +18,7 @@
 #include <iostream>
 
 #include "base/output.h"
+#include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/partial_model.h"
@@ -29,8 +30,11 @@ namespace theory {
 namespace arith {
 
 inline Node makeIntegerVariable(){
-  NodeManager* curr = NodeManager::currentNM();
-  return curr->mkSkolem("intvar", curr->integerType(), "is an integer variable created by the dio solver");
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  return sm->mkDummySkolem("intvar",
+                           nm->integerType(),
+                           "is an integer variable created by the dio solver");
 }
 
 DioSolver::DioSolver(context::Context* ctxt)
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 1cf9cbc54..aa9bce776 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -14,11 +14,12 @@
 
 #include "theory/arith/nl/cad_solver.h"
 
-#include "theory/inference_id.h"
+#include "expr/skolem_manager.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/poly_conversion.h"
+#include "theory/inference_id.h"
 
 namespace cvc5 {
 namespace theory {
@@ -37,11 +38,10 @@ CadSolver::CadSolver(InferenceManager& im,
       d_im(im),
       d_model(model)
 {
-  d_ranVariable =
-      NodeManager::currentNM()->mkSkolem("__z",
-                                         NodeManager::currentNM()->realType(),
-                                         "",
-                                         NodeManager::SKOLEM_EXACT_NAME);
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  d_ranVariable = sm->mkDummySkolem(
+      "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
 #ifdef CVC4_POLY_IMP
   ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
   if (pc != nullptr)
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index c8c375096..2a1f2ad91 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -20,6 +20,7 @@
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
 #include "expr/proof.h"
+#include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
@@ -55,10 +56,11 @@ SineSolver::~SineSolver() {}
 void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Assert(a.getKind() == Kind::SINE);
   Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl;
   Assert(!d_data->d_pi.isNull());
-  Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
+  Node shift = sm->mkDummySkolem("s", nm->integerType(), "number of shifts");
   // TODO (cvc4-projects #47) : do not introduce shift here, instead needs model-based
   // refinement for constant shifts (cvc4-projects #1284)
   Node lem = nm->mkNode(
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index ed5ab4255..b3fd40ce7 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
@@ -56,14 +57,15 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& xts)
   }
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   for (const Node& a : needsMaster)
   {
     // should not have processed this already
     Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end());
     Kind k = a.getKind();
     Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
-    Node y =
-        nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
+    Node y = sm->mkDummySkolem(
+        "y", nm->realType(), "phase shifted trigonometric arg");
     Node new_a = nm->mkNode(k, y);
     d_tstate.d_trSlaves[new_a].insert(new_a);
     d_tstate.d_trSlaves[new_a].insert(a);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 0a64a4e63..7ad0bbfbb 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4958,16 +4958,6 @@ std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const Arith
         setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
       }
       break;
-    case inferbounds::Simplex:
-      {
-        // primDir * diffm * diff < c or primDir * diffm * diff > c
-        tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
-        setToMin(primDir * dm.sgn(), bestPrimDiff, tmp);
-
-        tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
-        setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
-      }
-      break;
     default:
       Unhandled();
     }
@@ -5298,419 +5288,11 @@ void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& t
   tmp.first = nb;
 }
 
-std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){
-
-  if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){
-    return make_pair(Node::null(), DeltaRational());
-  }
-
-  Assert(d_qflraStatus == Result::SAT);
-  Assert(d_errorSet.noSignals());
-  Assert(param.getAlgorithm() == inferbounds::Simplex);
-
-  // TODO Move me into a new file
-
-  enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
-  ResultState finalState = Unset;
-
-  const int maxRounds =
-      param.getSimplexRounds().just() ? param.getSimplexRounds().value() : -1;
-
-  Maybe<DeltaRational> threshold;
-  // TODO: get this from the parameters
-
-  // setup term
-  Polynomial p = Polynomial::parsePolynomial(tp);
-  vector<ArithVar> variables;
-  vector<Rational> coefficients;
-  asVectors(p, coefficients, variables);
-  if(sgn < 0){
-    for(size_t i=0, N=coefficients.size(); i < N; ++i){
-      coefficients[i] = -coefficients[i];
-    }
-  }
-  // implicitly an upperbound
-  Node skolem = mkRealSkolem("tmpVar$$");
-  ArithVar optVar = requestArithVar(skolem, false, true);
-  d_tableau.addRow(optVar, coefficients, variables);
-  RowIndex ridx = d_tableau.basicToRowIndex(optVar);
-
-  DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
-  d_partialModel.setAssignment(optVar, newAssignment);
-  d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
-
-  // Setup simplex
-  d_partialModel.stopQueueingBoundCounts();
-  UpdateTrackingCallback utcb(&d_linEq);
-  d_partialModel.processBoundsQueue(utcb);
-  d_linEq.startTrackingBoundCounts();
-
-  // maximize optVar via primal Simplex
-  int rounds = 0;
-  while(finalState == Unset){
-    ++rounds;
-    if(maxRounds >= 0 && rounds > maxRounds){
-      finalState = ExhaustedRounds;
-      break;
-    }
-
-    // select entering by bland's rule
-    // TODO improve upon bland's
-    ArithVar entering = ARITHVAR_SENTINEL;
-    const Tableau::Entry* enteringEntry = NULL;
-    for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
-      const Tableau::Entry& entry = *ri;
-      ArithVar v = entry.getColVar();
-      if(v != optVar){
-        int sgn1 = entry.getCoefficient().sgn();
-        Assert(sgn1 != 0);
-        bool candidate = (sgn1 > 0)
-                             ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
-                             : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
-        if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
-          entering = v;
-          enteringEntry = &entry;
-        }
-      }
-    }
-    if(entering == ARITHVAR_SENTINEL){
-      finalState = Inferred;
-      break;
-    }
-    Assert(entering != ARITHVAR_SENTINEL);
-    Assert(enteringEntry != NULL);
-
-    int esgn = enteringEntry->getCoefficient().sgn();
-    Assert(esgn != 0);
-
-    // select leaving and ratio
-    ArithVar leaving = ARITHVAR_SENTINEL;
-    DeltaRational minRatio;
-    const Tableau::Entry* pivotEntry = NULL;
-
-    // Special case check the upper/lowerbound on entering
-    ConstraintP cOnEntering = (esgn > 0)
-      ? d_partialModel.getUpperBoundConstraint(entering)
-      : d_partialModel.getLowerBoundConstraint(entering);
-    if(cOnEntering != NullConstraint){
-      leaving = entering;
-      minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
-    }
-    for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
-      const Tableau::Entry& centry = *ci;
-      ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
-      int csgn = centry.getCoefficient().sgn();
-      int basicDir = csgn * esgn;
-
-      ConstraintP bound = (basicDir > 0)
-        ? d_partialModel.getUpperBoundConstraint(basic)
-        : d_partialModel.getLowerBoundConstraint(basic);
-      if(bound != NullConstraint){
-        DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
-        DeltaRational ratio = diff/(centry.getCoefficient());
-        bool selected = false;
-        if(leaving == ARITHVAR_SENTINEL){
-          selected = true;
-        }else{
-          int cmp = ratio.compare(minRatio);
-          if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
-            selected = (cmp != 0) ||
-              ((leaving != entering) && (basic < leaving));
-          }
-        }
-        if(selected){
-          leaving = basic;
-          minRatio = ratio;
-          pivotEntry = &centry;
-        }
-      }
-    }
-
-
-    if(leaving == ARITHVAR_SENTINEL){
-      finalState = NoBound;
-      break;
-    }else if(leaving == entering){
-      d_linEq.update(entering, minRatio);
-    }else{
-      DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
-      d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
-      // no conflicts clear signals
-      Assert(d_errorSet.noSignals());
-    }
-
-    if(threshold.just()){
-      if (d_partialModel.getAssignment(optVar) >= threshold.value())
-      {
-        finalState = ReachedThreshold;
-        break;
-      }
-    }
-  };
-
-  result = InferBoundsResult(tp, sgn > 0);
-
-  // tear down term
-  switch(finalState){
-  case Inferred:
-    {
-      NodeBuilder nb(kind::AND);
-      for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
-        const Tableau::Entry& e =*ri;
-        ArithVar colVar = e.getColVar();
-        if(colVar != optVar){
-          const Rational& q = e.getCoefficient();
-          Assert(q.sgn() != 0);
-          ConstraintP c = (q.sgn() > 0)
-            ? d_partialModel.getUpperBoundConstraint(colVar)
-            : d_partialModel.getLowerBoundConstraint(colVar);
-          c->externalExplainByAssertions(nb);
-        }
-      }
-      Assert(nb.getNumChildren() >= 1);
-      Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
-      result.setBound(d_partialModel.getAssignment(optVar), exp);
-      result.setIsOptimal();
-      break;
-    }
-  case NoBound:
-    break;
-  case ReachedThreshold:
-    result.setReachedThreshold();
-    break;
-  case ExhaustedRounds:
-    result.setBudgetExhausted();
-    break;
-  case Unset:
-  default:
-    Unreachable();
-    break;
-  };
-
-  d_linEq.stopTrackingRowIndex(ridx);
-  d_tableau.removeBasicRow(optVar);
-  releaseArithVar(optVar);
-
-  d_linEq.stopTrackingBoundCounts();
-  d_partialModel.startQueueingBoundCounts();
-
-  if(result.foundBound()){
-    return make_pair(result.getExplanation(), result.getValue());
-  }else{
-    return make_pair(Node::null(), DeltaRational());
-  }
-}
-
 ArithProofRuleChecker* TheoryArithPrivate::getProofChecker()
 {
   return &d_checker;
 }
 
-// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const
-// inferbounds::InferBoundAlgorithm& param){
-//   Assert(param.findUpperBound());
-
-//   if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){
-//     InferBoundsResult inconsistent;
-//     inconsistent.setInconsistent();
-//     return inconsistent;
-//   }
-
-//   Assert(d_qflraStatus == Result::SAT);
-//   Assert(d_errorSet.noSignals());
-
-//   // TODO Move me into a new file
-
-//   enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
-//   ResultState finalState = Unset;
-
-//   int maxRounds = 0;
-//   switch(param.getParamKind()){
-//   case InferBoundsParameters::Unbounded:
-//     maxRounds = -1;
-//     break;
-//   case InferBoundsParameters::NumVars:
-//     maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter();
-//     break;
-//   case InferBoundsParameters::Direct:
-//     maxRounds = param.getSimplexRoundParameter();
-//     break;
-//   default: maxRounds = 0; break;
-//   }
-
-//   // setup term
-//   Polynomial p = Polynomial::parsePolynomial(t);
-//   vector<ArithVar> variables;
-//   vector<Rational> coefficients;
-//   asVectors(p, coefficients, variables);
-
-//   Node skolem = mkRealSkolem("tmpVar$$");
-//   ArithVar optVar = requestArithVar(skolem, false, true);
-//   d_tableau.addRow(optVar, coefficients, variables);
-//   RowIndex ridx = d_tableau.basicToRowIndex(optVar);
-
-//   DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
-//   d_partialModel.setAssignment(optVar, newAssignment);
-//   d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
-
-//   // Setup simplex
-//   d_partialModel.stopQueueingBoundCounts();
-//   UpdateTrackingCallback utcb(&d_linEq);
-//   d_partialModel.processBoundsQueue(utcb);
-//   d_linEq.startTrackingBoundCounts();
-
-//   // maximize optVar via primal Simplex
-//   int rounds = 0;
-//   while(finalState == Unset){
-//     ++rounds;
-//     if(maxRounds >= 0 && rounds > maxRounds){
-//       finalState = ExhaustedRounds;
-//       break;
-//     }
-
-//     // select entering by bland's rule
-//     // TODO improve upon bland's
-//     ArithVar entering = ARITHVAR_SENTINEL;
-//     const Tableau::Entry* enteringEntry = NULL;
-//     for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx);
-//     !ri.atEnd(); ++ri){
-//       const Tableau::Entry& entry = *ri;
-//       ArithVar v = entry.getColVar();
-//       if(v != optVar){
-//         int sgn = entry.getCoefficient().sgn();
-//         Assert(sgn != 0);
-//         bool candidate = (sgn > 0)
-//           ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
-//           : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
-//         if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
-//           entering = v;
-//           enteringEntry = &entry;
-//         }
-//       }
-//     }
-//     if(entering == ARITHVAR_SENTINEL){
-//       finalState = Inferred;
-//       break;
-//     }
-//     Assert(entering != ARITHVAR_SENTINEL);
-//     Assert(enteringEntry != NULL);
-
-//     int esgn = enteringEntry->getCoefficient().sgn();
-//     Assert(esgn != 0);
-
-//     // select leaving and ratio
-//     ArithVar leaving = ARITHVAR_SENTINEL;
-//     DeltaRational minRatio;
-//     const Tableau::Entry* pivotEntry = NULL;
-
-//     // Special case check the upper/lowerbound on entering
-//     ConstraintP cOnEntering = (esgn > 0)
-//       ? d_partialModel.getUpperBoundConstraint(entering)
-//       : d_partialModel.getLowerBoundConstraint(entering);
-//     if(cOnEntering != NullConstraint){
-//       leaving = entering;
-//       minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
-//     }
-//     for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
-//       const Tableau::Entry& centry = *ci;
-//       ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
-//       int csgn = centry.getCoefficient().sgn();
-//       int basicDir = csgn * esgn;
-
-//       ConstraintP bound = (basicDir > 0)
-//         ? d_partialModel.getUpperBoundConstraint(basic)
-//         : d_partialModel.getLowerBoundConstraint(basic);
-//       if(bound != NullConstraint){
-//         DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
-//         DeltaRational ratio = diff/(centry.getCoefficient());
-//         bool selected = false;
-//         if(leaving == ARITHVAR_SENTINEL){
-//           selected = true;
-//         }else{
-//           int cmp = ratio.compare(minRatio);
-//           if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
-//             selected = (cmp != 0) ||
-//               ((leaving != entering) && (basic < leaving));
-//           }
-//         }
-//         if(selected){
-//           leaving = basic;
-//           minRatio = ratio;
-//           pivotEntry = &centry;
-//         }
-//       }
-//     }
-
-//     if(leaving == ARITHVAR_SENTINEL){
-//       finalState = NoBound;
-//       break;
-//     }else if(leaving == entering){
-//       d_linEq.update(entering, minRatio);
-//     }else{
-//       DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
-//       d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
-//       // no conflicts clear signals
-//       Assert(d_errorSet.noSignals());
-//     }
-
-//     if(param.useThreshold()){
-//       if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){
-//         finalState = ReachedThreshold;
-//         break;
-//       }
-//     }
-//   };
-
-//   InferBoundsResult result(t, param.findUpperBound());
-
-//   // tear down term
-//   switch(finalState){
-//   case Inferred:
-//     {
-//       NodeBuilder nb(kind::AND);
-//       for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx);
-//       !ri.atEnd(); ++ri){
-//         const Tableau::Entry& e =*ri;
-//         ArithVar colVar = e.getColVar();
-//         if(colVar != optVar){
-//           const Rational& q = e.getCoefficient();
-//           Assert(q.sgn() != 0);
-//           ConstraintP c = (q.sgn() > 0)
-//             ? d_partialModel.getUpperBoundConstraint(colVar)
-//             : d_partialModel.getLowerBoundConstraint(colVar);
-//           c->externalExplainByAssertions(nb);
-//         }
-//       }
-//       Assert(nb.getNumChildren() >= 1);
-//       Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
-//       result.setBound(d_partialModel.getAssignment(optVar), exp);
-//       result.setIsOptimal();
-//       break;
-//     }
-//   case NoBound:
-//     break;
-//   case ReachedThreshold:
-//     result.setReachedThreshold();
-//     break;
-//   case ExhaustedRounds:
-//     result.setBudgetExhausted();
-//     break;
-//   case Unset:
-//   default:
-//     Unreachable();
-//     break;
-//   };
-
-//   d_linEq.stopTrackingRowIndex(ridx);
-//   d_tableau.removeBasicRow(optVar);
-//   releaseArithVar(optVar);
-
-//   d_linEq.stopTrackingBoundCounts();
-//   d_partialModel.startQueueingBoundCounts();
-
-//   return result;
-// }
-
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index ba3fdfaf5..50fb89808 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -137,12 +137,6 @@ private:
   void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
   void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
 
-  std::pair<Node, DeltaRational> entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out);
-
-  //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p);
-  //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p);
-  //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p);
-
   /**
    * Infers either a new upper/lower bound on term in the real relaxation.
    * Either:
diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp
index c5ea17847..2d540010f 100644
--- a/src/theory/builtin/theory_builtin_type_rules.cpp
+++ b/src/theory/builtin/theory_builtin_type_rules.cpp
@@ -17,6 +17,7 @@
 #include "theory/builtin/theory_builtin_type_rules.h"
 
 #include "expr/attribute.h"
+#include "expr/skolem_manager.h"
 
 namespace cvc5 {
 namespace theory {
@@ -39,7 +40,8 @@ Node SortProperties::mkGroundTerm(TypeNode type)
   {
     return type.getAttribute(gta);
   }
-  Node k = NodeManager::currentNM()->mkSkolem(
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node k = sm->mkDummySkolem(
       "groundTerm", type, "a ground term created for type " + type.toString());
   type.setAttribute(gta, k);
   return k;
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index acb67a373..348c8bebb 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -14,6 +14,7 @@
  **/
 #include "theory/bv/abstraction.h"
 
+#include "expr/skolem_manager.h"
 #include "options/bv_options.h"
 #include "printer/printer.h"
 #include "smt/dump.h"
@@ -282,6 +283,7 @@ Node AbstractionModule::getSignatureSkolem(TNode node)
 {
   Assert(node.getMetaKind() == kind::metakind::VARIABLE);
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   unsigned bitwidth = utils::getSize(node);
   if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end())
   {
@@ -296,9 +298,9 @@ Node AbstractionModule::getSignatureSkolem(TNode node)
   {
     ostringstream os;
     os << "sig_" << bitwidth << "_" << index;
-    skolems.push_back(nm->mkSkolem(os.str(),
-                                   nm->mkBitVectorType(bitwidth),
-                                   "skolem for computing signatures"));
+    skolems.push_back(sm->mkDummySkolem(os.str(),
+                                        nm->mkBitVectorType(bitwidth),
+                                        "skolem for computing signatures"));
   }
   ++(d_signatureIndices[bitwidth]);
   return skolems[index];
@@ -435,6 +437,7 @@ void AbstractionModule::storeGeneralization(TNode s, TNode t) {
 void AbstractionModule::finalizeSignatures()
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Debug("bv-abstraction")
       << "AbstractionModule::finalizeSignatures num signatures = "
       << d_signatures.size() << "\n";
@@ -519,8 +522,8 @@ void AbstractionModule::finalizeSignatures()
     TypeNode range = nm->mkBitVectorType(1);
 
     TypeNode abs_type = nm->mkFunctionType(arg_types, range);
-    Node abs_func =
-        nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory");
+    Node abs_func = sm->mkDummySkolem(
+        "abs_$$", abs_type, "abstraction function for bv theory");
     Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n";
 
     // NOTE: signature expression type is BOOLEAN
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 4f89eff71..de5210e1a 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/bv/bv_subtheory_core.h"
 
+#include "expr/skolem_manager.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
@@ -537,6 +538,7 @@ bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; }
 bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   bool sentLemma = false;
   eq::EqualityEngine* ee = d_equalityEngine;
   std::map<Node, Node> op_map;
@@ -592,7 +594,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
             // congruent modulo 2^( bv width )
             unsigned bvs = n.getType().getBitVectorSize();
             Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
-            Node k = nm->mkSkolem(
+            Node k = sm->mkDummySkolem(
                 "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
             t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
           }
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 96f91ea9f..292010cf4 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -18,6 +18,7 @@
 
 #include <vector>
 
+#include "expr/skolem_manager.h"
 #include "options/theory_options.h"
 #include "theory/theory.h"
 
@@ -278,10 +279,10 @@ Node mkConst(const BitVector& value)
 Node mkVar(unsigned size)
 {
   NodeManager* nm = NodeManager::currentNM();
-
-  return nm->mkSkolem("BVSKOLEM$$",
-                      nm->mkBitVectorType(size),
-                      "is a variable created by the theory of bitvectors");
+  SkolemManager* sm = nm->getSkolemManager();
+  return sm->mkDummySkolem("BVSKOLEM$$",
+                           nm->mkBitVectorType(size),
+                           "is a variable created by the theory of bitvectors");
 }
 
 /* ------------------------------------------------------------------------- */
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 14c004bda..31467df65 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -17,6 +17,7 @@
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_manager.h"
+#include "expr/skolem_manager.h"
 #include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
@@ -435,10 +436,11 @@ Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre)
     return itt->second;
   }
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::vector<TypeNode> types;
   types.push_back(tn);
   TypeNode ptn = nm->mkPredicateType(types);
-  Node pred = nm->mkSkolem(isPre ? "pre" : "post", ptn);
+  Node pred = sm->mkDummySkolem(isPre ? "pre" : "post", ptn);
   d_traversal_pred[index][tn][n] = pred;
   return pred;
 }
@@ -446,6 +448,7 @@ Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre)
 Node SygusExtension::eliminateTraversalPredicates(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   std::map<Node, Node>::iterator ittb;
@@ -471,7 +474,7 @@ Node SygusExtension::eliminateTraversalPredicates(Node n)
         {
           std::stringstream ss;
           ss << "v_" << cur;
-          ret = nm->mkSkolem(ss.str(), cur.getType());
+          ret = sm->mkDummySkolem(ss.str(), cur.getType());
           d_traversal_bool[cur] = ret;
         }
         else
@@ -1367,9 +1370,9 @@ void SygusExtension::registerSizeTerm(Node e)
       slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue());
     }else{
       Node mt = d_szinfo[m]->getOrMkActiveMeasureValue();
-      Node new_mt = d_szinfo[m]->getOrMkActiveMeasureValue(true);
+      Node newMt = d_szinfo[m]->getOrMkActiveMeasureValue(true);
       Node ds = nm->mkNode(DT_SIZE, e);
-      slem = mt.eqNode(nm->mkNode(PLUS, new_mt, ds));
+      slem = mt.eqNode(nm->mkNode(PLUS, newMt, ds));
     }
     Trace("sygus-sb") << "...size lemma : " << slem << std::endl;
     d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_MT_BOUND);
@@ -1761,7 +1764,8 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue()
   if (d_measure_value.isNull())
   {
     NodeManager* nm = NodeManager::currentNM();
-    d_measure_value = nm->mkSkolem("mt", nm->integerType());
+    SkolemManager* sm = nm->getSkolemManager();
+    d_measure_value = sm->mkDummySkolem("mt", nm->integerType());
     Node mtlem =
         nm->mkNode(kind::GEQ, d_measure_value, nm->mkConst(Rational(0)));
     d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
@@ -1775,7 +1779,8 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
   if (mkNew)
   {
     NodeManager* nm = NodeManager::currentNM();
-    Node new_mt = nm->mkSkolem("mt", nm->integerType());
+    SkolemManager* sm = nm->getSkolemManager();
+    Node new_mt = sm->mkDummySkolem("mt", nm->integerType());
     Node mtlem = nm->mkNode(kind::GEQ, new_mt, nm->mkConst(Rational(0)));
     d_measure_value_active = new_mt;
     d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 598b29cf6..df4560905 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -23,6 +23,7 @@
 #include "expr/dtype_cons.h"
 #include "expr/kind.h"
 #include "expr/proof_node_manager.h"
+#include "expr/skolem_manager.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
@@ -830,10 +831,12 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
 
 void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
   if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     std::stringstream ss;
     ss << sel << "_uf";
-    d_exp_def_skolem[dt][ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
-                                  NodeManager::currentNM()->mkFunctionType( dt, rt ) );
+    d_exp_def_skolem[dt][sel] =
+        sm->mkDummySkolem(ss.str().c_str(), nm->mkFunctionType(dt, rt));
   }
 }
 
@@ -841,8 +844,11 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) {
   if( n.getKind()==APPLY_CONSTRUCTOR ){
     NodeMap::const_iterator it = d_term_sk.find( n );
     if( it==d_term_sk.end() ){
+      NodeManager* nm = NodeManager::currentNM();
+      SkolemManager* sm = nm->getSkolemManager();
       //add purification unit lemma ( k = n )
-      Node k = NodeManager::currentNM()->mkSkolem( "k", n.getType(), "reference skolem for datatypes" );
+      Node k =
+          sm->mkDummySkolem("k", n.getType(), "reference skolem for datatypes");
       d_term_sk[n] = k;
       Node eq = k.eqNode( n );
       Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
@@ -1399,17 +1405,19 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c
 }
 
 Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   int index = pol ? 0 : 1;
   std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn );
   if( it==d_singleton_lemma[index].end() ){
     Node a;
     if( pol ){
-      Node v1 = NodeManager::currentNM()->mkBoundVar( tn );
-      Node v2 = NodeManager::currentNM()->mkBoundVar( tn );
-      a = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, v1, v2 ), v1.eqNode( v2 ) );
+      Node v1 = nm->mkBoundVar(tn);
+      Node v2 = nm->mkBoundVar(tn);
+      a = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v1, v2), v1.eqNode(v2));
     }else{
-      Node v1 = NodeManager::currentNM()->mkSkolem( "k1", tn );
-      Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
+      Node v1 = sm->mkDummySkolem("k1", tn);
+      Node v2 = sm->mkDummySkolem("k2", tn);
       a = v1.eqNode( v2 ).negate();
       //send out immediately as lemma
       d_im.lemma(a, InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ);
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index 0597bb3ea..08fa0164b 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/engine_output_channel.h"
 
+#include "expr/skolem_manager.h"
 #include "prop/prop_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/theory_engine.h"
@@ -118,10 +119,11 @@ void EngineOutputChannel::conflict(TNode conflictNode)
 
 void EngineOutputChannel::demandRestart()
 {
-  NodeManager* curr = NodeManager::currentNM();
-  Node restartVar = curr->mkSkolem(
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  Node restartVar = sm->mkDummySkolem(
       "restartVar",
-      curr->booleanType(),
+      nm->booleanType(),
       "A boolean variable asserted to be true to force a restart");
   Trace("theory::restart") << "EngineOutputChannel<" << d_theory
                            << ">::restart(" << restartVar << ")" << std::endl;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 93b492b88..88d01ea20 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "base/configuration.h"
+#include "expr/skolem_manager.h"
 #include "options/fp_options.h"
 #include "smt/logic_exception.h"
 #include "theory/fp/fp_converter.h"
@@ -205,6 +206,7 @@ Node TheoryFp::minUF(Node node) {
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   ComparisonUFMap::const_iterator i(d_minMap.find(t));
 
   Node fun;
@@ -212,16 +214,16 @@ Node TheoryFp::minUF(Node node) {
     std::vector<TypeNode> args(2);
     args[0] = t;
     args[1] = t;
-    fun = nm->mkSkolem("floatingpoint_min_zero_case",
-                       nm->mkFunctionType(args,
+    fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
+                            nm->mkFunctionType(args,
 #ifdef SYMFPUPROPISBOOL
-                                          nm->booleanType()
+                                               nm->booleanType()
 #else
-                                          nm->mkBitVectorType(1U)
+                                               nm->mkBitVectorType(1U)
 #endif
-                                              ),
-                       "floatingpoint_min_zero_case",
-                       NodeManager::SKOLEM_EXACT_NAME);
+                                                   ),
+                            "floatingpoint_min_zero_case",
+                            NodeManager::SKOLEM_EXACT_NAME);
     d_minMap.insert(t, fun);
   } else {
     fun = (*i).second;
@@ -236,6 +238,7 @@ Node TheoryFp::maxUF(Node node) {
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   ComparisonUFMap::const_iterator i(d_maxMap.find(t));
 
   Node fun;
@@ -243,16 +246,16 @@ Node TheoryFp::maxUF(Node node) {
     std::vector<TypeNode> args(2);
     args[0] = t;
     args[1] = t;
-    fun = nm->mkSkolem("floatingpoint_max_zero_case",
-                       nm->mkFunctionType(args,
+    fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
+                            nm->mkFunctionType(args,
 #ifdef SYMFPUPROPISBOOL
-                                          nm->booleanType()
+                                               nm->booleanType()
 #else
-                                          nm->mkBitVectorType(1U)
+                                               nm->mkBitVectorType(1U)
 #endif
-                                              ),
-                       "floatingpoint_max_zero_case",
-                       NodeManager::SKOLEM_EXACT_NAME);
+                                                   ),
+                            "floatingpoint_max_zero_case",
+                            NodeManager::SKOLEM_EXACT_NAME);
     d_maxMap.insert(t, fun);
   } else {
     fun = (*i).second;
@@ -271,6 +274,7 @@ Node TheoryFp::toUBVUF(Node node) {
 
   std::pair<TypeNode, TypeNode> p(source, target);
   NodeManager *nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   ConversionUFMap::const_iterator i(d_toUBVMap.find(p));
 
   Node fun;
@@ -278,10 +282,10 @@ Node TheoryFp::toUBVUF(Node node) {
     std::vector<TypeNode> args(2);
     args[0] = nm->roundingModeType();
     args[1] = source;
-    fun = nm->mkSkolem("floatingpoint_to_ubv_out_of_range_case",
-                       nm->mkFunctionType(args, target),
-                       "floatingpoint_to_ubv_out_of_range_case",
-                       NodeManager::SKOLEM_EXACT_NAME);
+    fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case",
+                            nm->mkFunctionType(args, target),
+                            "floatingpoint_to_ubv_out_of_range_case",
+                            NodeManager::SKOLEM_EXACT_NAME);
     d_toUBVMap.insert(p, fun);
   } else {
     fun = (*i).second;
@@ -300,6 +304,7 @@ Node TheoryFp::toSBVUF(Node node) {
 
   std::pair<TypeNode, TypeNode> p(source, target);
   NodeManager *nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   ConversionUFMap::const_iterator i(d_toSBVMap.find(p));
 
   Node fun;
@@ -307,10 +312,10 @@ Node TheoryFp::toSBVUF(Node node) {
     std::vector<TypeNode> args(2);
     args[0] = nm->roundingModeType();
     args[1] = source;
-    fun = nm->mkSkolem("floatingpoint_to_sbv_out_of_range_case",
-                       nm->mkFunctionType(args, target),
-                       "floatingpoint_to_sbv_out_of_range_case",
-                       NodeManager::SKOLEM_EXACT_NAME);
+    fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case",
+                            nm->mkFunctionType(args, target),
+                            "floatingpoint_to_sbv_out_of_range_case",
+                            NodeManager::SKOLEM_EXACT_NAME);
     d_toSBVMap.insert(p, fun);
   } else {
     fun = (*i).second;
@@ -324,16 +329,17 @@ Node TheoryFp::toRealUF(Node node) {
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   ComparisonUFMap::const_iterator i(d_toRealMap.find(t));
 
   Node fun;
   if (i == d_toRealMap.end()) {
     std::vector<TypeNode> args(1);
     args[0] = t;
-    fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case",
-                       nm->mkFunctionType(args, nm->realType()),
-                       "floatingpoint_to_real_infinity_and_NaN_case",
-                       NodeManager::SKOLEM_EXACT_NAME);
+    fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case",
+                            nm->mkFunctionType(args, nm->realType()),
+                            "floatingpoint_to_real_infinity_and_NaN_case",
+                            NodeManager::SKOLEM_EXACT_NAME);
     d_toRealMap.insert(t, fun);
   } else {
     fun = (*i).second;
@@ -348,6 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
 
   Node fun;
@@ -356,10 +363,10 @@ Node TheoryFp::abstractRealToFloat(Node node)
     std::vector<TypeNode> args(2);
     args[0] = node[0].getType();
     args[1] = node[1].getType();
-    fun = nm->mkSkolem("floatingpoint_abstract_real_to_float",
-                       nm->mkFunctionType(args, node.getType()),
-                       "floatingpoint_abstract_real_to_float",
-                       NodeManager::SKOLEM_EXACT_NAME);
+    fun = sm->mkDummySkolem("floatingpoint_abstract_real_to_float",
+                            nm->mkFunctionType(args, node.getType()),
+                            "floatingpoint_abstract_real_to_float",
+                            NodeManager::SKOLEM_EXACT_NAME);
     d_realToFloatMap.insert(t, fun);
   }
   else
@@ -380,6 +387,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
 
   Node fun;
@@ -388,10 +396,10 @@ Node TheoryFp::abstractFloatToReal(Node node)
     std::vector<TypeNode> args(2);
     args[0] = t;
     args[1] = nm->realType();
-    fun = nm->mkSkolem("floatingpoint_abstract_float_to_real",
-                       nm->mkFunctionType(args, nm->realType()),
-                       "floatingpoint_abstract_float_to_real",
-                       NodeManager::SKOLEM_EXACT_NAME);
+    fun = sm->mkDummySkolem("floatingpoint_abstract_float_to_real",
+                            nm->mkFunctionType(args, nm->realType()),
+                            "floatingpoint_abstract_float_to_real",
+                            NodeManager::SKOLEM_EXACT_NAME);
     d_floatToRealMap.insert(t, fun);
   }
   else
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;
 }
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 6085c034d..5585b36ab 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -20,6 +20,7 @@
 
 #include "base/map_util.h"
 #include "expr/kind.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/sep_options.h"
 #include "options/smt_options.h"
@@ -313,6 +314,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
   TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom;
   TNode slbl = atom.getKind() == SEP_LABEL ? atom[1] : TNode::null();
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   if (slbl.isNull())
   {
     Trace("sep-lemma-debug")
@@ -434,8 +436,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
       }
       else
       {
-        Node kl = nm->mkSkolem("loc", getReferenceType(satom));
-        Node kd = nm->mkSkolem("data", getDataType(satom));
+        Node kl = sm->mkDummySkolem("loc", getReferenceType(satom));
+        Node kd = sm->mkDummySkolem("data", getDataType(satom));
         Node econc = nm->mkNode(
             SEP_LABEL,
             nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true),
@@ -466,7 +468,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
     Trace("sep-lemma-debug")
         << "Negated spatial constraint asserted to sep theory: " << fact
         << std::endl;
-    Node g = nm->mkSkolem("G", nm->booleanType());
+    Node g = sm->mkDummySkolem("G", nm->booleanType());
     d_neg_guard_strategy[g].reset(new DecisionStrategySingleton(
         "sep_neg_guard", g, getSatContext(), getValuation()));
     DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get();
@@ -506,6 +508,7 @@ void TheorySep::postCheck(Effort level)
     return;
   }
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Trace("sep-process") << "Checking heap at full effort..." << std::endl;
   d_label_model.clear();
   d_tmodel.clear();
@@ -849,8 +852,8 @@ void TheorySep::postCheck(Effort level)
       {
         Trace("sep-process") << "Must witness label : " << ll
                              << ", data type is " << data_type << std::endl;
-        Node dsk =
-            nm->mkSkolem("dsk", data_type, "pto-data for implicit location");
+        Node dsk = sm->mkDummySkolem(
+            "dsk", data_type, "pto-data for implicit location");
         // if location is in the heap, then something must point to it
         Node lem = nm->mkNode(
             IMPLIES,
@@ -1160,6 +1163,8 @@ void TheorySep::initializeBounds() {
   if( !d_bounds_init ){
     Trace("sep-bound")  << "Initialize sep bounds..." << std::endl;
     d_bounds_init = true;
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){
       TypeNode tn = it->first;
       Trace("sep-bound")  << "Initialize bounds for " << tn << "..." << std::endl;
@@ -1174,7 +1179,8 @@ void TheorySep::initializeBounds() {
       Trace("sep-bound") << "Type reference size : " << d_type_references[tn].size() << std::endl;
       Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl;
       for( unsigned r=0; r<n_emp; r++ ){
-        Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
+        Node e =
+            sm->mkDummySkolem("e", tn, "cardinality bound element for seplog");
         d_type_references_card[tn].push_back( e );
         d_type_ref_card_id[e] = r;
       }
@@ -1185,19 +1191,20 @@ void TheorySep::initializeBounds() {
 Node TheorySep::getBaseLabel( TypeNode tn ) {
   std::map< TypeNode, Node >::iterator it = d_base_label.find( tn );
   if( it==d_base_label.end() ){
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     initializeBounds();
     Trace("sep") << "Make base label for " << tn << std::endl;
     std::stringstream ss;
     ss << "__Lb";
-    TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
-    //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
-    Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "base label" );
+    TypeNode ltn = nm->mkSetType(tn);
+    Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "base label");
     d_base_label[tn] = n_lbl;
     //make reference bound
     Trace("sep") << "Make reference bound label for " << tn << std::endl;
     std::stringstream ss2;
     ss2 << "__Lu";
-    d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" );
+    d_reference_bound[tn] = sm->mkDummySkolem(ss2.str(), ltn, "");
     d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() );
 
     //check whether monotonic (elements can be added to tn without effecting satisfiability)
@@ -1308,12 +1315,14 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) {
 Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
   std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child );
   if( it==d_label_map[atom][lbl].end() ){
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     TypeNode refType = getReferenceType( atom );
     std::stringstream ss;
     ss << "__Lc" << child;
     TypeNode ltn = NodeManager::currentNM()->mkSetType(refType);
     //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType));
-    Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "sep label" );
+    Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "sep label");
     d_label_map[atom][lbl][child] = n_lbl;
     d_label_map_parent[n_lbl] = lbl;
     return n_lbl;
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index b67df285d..bbe100e98 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/emptyset.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/sets_options.h"
 #include "smt/logic_exception.h"
 #include "theory/rewriter.h"
@@ -1015,6 +1016,7 @@ void CardinalityExtension::mkModelValueElementsFor(
       std::uint32_t vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
       Assert(els.size() <= vu);
       NodeManager* nm = NodeManager::currentNM();
+      SkolemManager* sm = nm->getSkolemManager();
       if (elementType.isInterpretedFinite())
       {
         // get all members of this finite type
@@ -1034,7 +1036,7 @@ void CardinalityExtension::mkModelValueElementsFor(
           // slack elements for the leaves without worrying about conflicts with
           // the current members of this finite type.
 
-          Node slack = nm->mkSkolem("slack", elementType);
+          Node slack = sm->mkDummySkolem("slack", elementType);
           Node singleton = nm->mkSingleton(elementType, slack);
           els.push_back(singleton);
           d_finite_type_slack_elements[elementType].push_back(slack);
@@ -1043,8 +1045,8 @@ void CardinalityExtension::mkModelValueElementsFor(
         }
         else
         {
-          els.push_back(
-              nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType)));
+          els.push_back(nm->mkSingleton(
+              elementType, sm->mkDummySkolem("msde", elementType)));
         }
       }
     }
diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp
index c18e9406d..8c0d125d5 100644
--- a/src/theory/sets/skolem_cache.cpp
+++ b/src/theory/sets/skolem_cache.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/sets/skolem_cache.h"
 
+#include "expr/skolem_manager.h"
 #include "theory/rewriter.h"
 
 using namespace cvc5::kind;
@@ -49,7 +50,8 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
 
 Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
 {
-  Node n = NodeManager::currentNM()->mkSkolem(c, tn, "sets skolem");
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node n = sm->mkDummySkolem(c, tn, "sets skolem");
   d_allSkolems.insert(n);
   return n;
 }
diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
index a093840f7..43eed46a6 100644
--- a/src/theory/sets/term_registry.cpp
+++ b/src/theory/sets/term_registry.cpp
@@ -15,6 +15,7 @@
 #include "theory/sets/term_registry.h"
 
 #include "expr/emptyset.h"
+#include "expr/skolem_manager.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -116,7 +117,8 @@ Node TermRegistry::getTypeConstraintSkolem(Node n, TypeNode tn)
   std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
   if (it == d_tc_skolem[n].end())
   {
-    Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
+    SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+    Node k = sm->mkDummySkolem("tc_k", tn);
     d_tc_skolem[n][tn] = k;
     return k;
   }
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index b97d3125d..3aa97672d 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1373,11 +1373,12 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
   }
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   TypeNode chooseUf = nm->mkFunctionType(setType, setType.getSetElementType());
   stringstream stream;
   stream << "chooseUf" << setType.getId();
   string name = stream.str();
-  Node chooseSkolem = nm->mkSkolem(
+  Node chooseSkolem = sm->mkDummySkolem(
       name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME);
   d_chooseFunctions[setType] = chooseSkolem;
   return chooseSkolem;
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 6609e4923..aa79f903b 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -15,8 +15,10 @@
  **/
 
 #include "theory/sets/theory_sets_rels.h"
-#include "theory/sets/theory_sets_private.h"
+
+#include "expr/skolem_manager.h"
 #include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -361,11 +363,11 @@ void TheorySetsRels::check(Theory::Effort level)
   }
 
   /* JOIN-IMAGE DOWN  : (x) IS_IN (R JOIN_IMAGE n)
-  *                     -------------------------------------------------------
-  *                     (x, x1) IS_IN R .... (x, xn) IS_IN R  DISTINCT(x1, ... , xn)
-  *
-  */
-
+   *                     -------------------------------------------------------
+   *                     (x, x1) IS_IN R .... (x, xn) IS_IN R  DISTINCT(x1, ...
+   * , xn)
+   *
+   */
   void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) {
     Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term
                         << " with mem_rep = " << mem_rep  << " and exp = " << exp << std::endl;
@@ -387,29 +389,37 @@ void TheorySetsRels::check(Theory::Effort level)
         }
       }
     }
-
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     Node reason = exp;
     Node conclusion = d_trueNode;
     std::vector< Node > distinct_skolems;
     Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
 
     if( exp[1] != join_image_term ) {
-      reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) );
+      reason =
+          nm->mkNode(AND, reason, nm->mkNode(EQUAL, exp[1], join_image_term));
     }
     for( unsigned int i = 0; i < min_card; i++ ) {
-      Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] );
+      Node skolem = sm->mkDummySkolem(
+          "jig", join_image_rel.getType()[0].getTupleTypes()[0]);
       distinct_skolems.push_back( skolem );
-      conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) );
+      conclusion = nm->mkNode(
+          AND,
+          conclusion,
+          nm->mkNode(
+              MEMBER,
+              RelsUtils::constructPair(join_image_rel, fst_mem_element, skolem),
+              join_image_rel));
     }
     if( distinct_skolems.size() >= 2 ) {
-      conclusion =  NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) );
+      conclusion =
+          nm->mkNode(AND, conclusion, nm->mkNode(DISTINCT, distinct_skolems));
     }
     sendInfer(conclusion, InferenceId::SETS_RELS_JOIN_IMAGE_DOWN, reason);
     Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl;
-
   }
 
-
   /* IDENTITY-DOWN  : (x, y) IS_IN IDEN(R)
   *               -------------------------------------------------------
   *                   x = y,  (x IS_IN R)
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index fb3551e9a..9427bb1d5 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -24,11 +24,12 @@
 #include <sstream>
 #include <vector>
 
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
-#include "theory/rewriter.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/rewriter.h"
 
 using namespace cvc5;
 using namespace cvc5::kind;
@@ -578,7 +579,7 @@ TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
       //must create new type
       std::stringstream ss;
       ss << "it_" << t << "_" << pref;
-      retType = NodeManager::currentNM()->mkSort( ss.str() );
+      retType = NodeManager::currentNM()->mkSort(ss.str());
     }
     Trace("sort-inference") << "-> Make type " << retType << " to correspond to ";
     printSort("sort-inference", t );
@@ -599,6 +600,8 @@ TypeNode SortInference::getTypeForId( int t ){
 }
 
 Node SortInference::getNewSymbol( Node old, TypeNode tn ){
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   // if no sort was inferred for this node, return original
   if( tn.isNull() || tn.isComparableTo( old.getType() ) ){
     return old;
@@ -607,18 +610,20 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){
     if( d_const_map[tn].find( old )==d_const_map[tn].end() ){
       std::stringstream ss;
       ss << "ic_" << tn << "_" << old;
-      d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" );  //use mkConst???
+      d_const_map[tn][old] = sm->mkDummySkolem(
+          ss.str(),
+          tn,
+          "constant created during sort inference");  // use mkConst???
     }
     return d_const_map[tn][ old ];
   }else if( old.getKind()==kind::BOUND_VARIABLE ){
     std::stringstream ss;
     ss << "b_" << old;
-    return NodeManager::currentNM()->mkBoundVar( ss.str(), tn );
-  }else{
-    std::stringstream ss;
-    ss << "i_" << old;
-    return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );
+    return nm->mkBoundVar(ss.str(), tn);
   }
+  std::stringstream ss;
+  ss << "i_" << old;
+  return sm->mkDummySkolem(ss.str(), tn, "created during sort inference");
 }
 
 Node SortInference::simplifyNode(
@@ -632,6 +637,8 @@ Node SortInference::simplifyNode(
   if( itv!=visited[n].end() ){
     return itv->second;
   }else{
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     Trace("sort-inference-debug2") << "Simplify " << n << ", type context=" << tnn << std::endl;
     std::vector< Node > children;
     std::map< Node, std::map< TypeNode, Node > > new_visited;
@@ -646,7 +653,7 @@ Node SortInference::simplifyNode(
         new_children.push_back( v );
         var_bound[ n[0][i] ] = v;
       }
-      children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) );
+      children.push_back(nm->mkNode(n[0].getKind(), new_children));
       use_new_visited = true;
     }
 
@@ -701,7 +708,7 @@ Node SortInference::simplifyNode(
         Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl;
         var_bound.erase( n[0][i] );
       }
-      ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      ret = nm->mkNode(n.getKind(), children);
     }else if( n.getKind()==kind::EQUAL ){
       TypeNode tn1 = children[0].getType();
       TypeNode tn2 = children[1].getType();
@@ -710,7 +717,7 @@ Node SortInference::simplifyNode(
         Trace("sort-inference-warn") << "  Types : " << children[0].getType() << " " << children[1].getType() << std::endl;
         Assert(false);
       }
-      ret = NodeManager::currentNM()->mkNode( kind::EQUAL, children );
+      ret = nm->mkNode(kind::EQUAL, children);
     }
     else if (isHandledApplyUf(n.getKind()))
     {
@@ -732,8 +739,9 @@ Node SortInference::simplifyNode(
         if( opChanged ){
           std::stringstream ss;
           ss << "io_" << op;
-          TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );
-          d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );
+          TypeNode typ = nm->mkFunctionType(argTypes, retType);
+          d_symbol_map[op] = sm->mkDummySkolem(
+              ss.str(), typ, "op created during sort inference");
           Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl;
           model_replace_f[op] = d_symbol_map[op];
         }else{
@@ -752,7 +760,7 @@ Node SortInference::simplifyNode(
           Assert(false);
         }
       }
-      ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
+      ret = nm->mkNode(kind::APPLY_UF, children);
     }else{
       std::map< Node, Node >::iterator it = var_bound.find( n );
       if( it!=var_bound.end() ){
@@ -767,7 +775,7 @@ Node SortInference::simplifyNode(
         //type is determined by context
         ret = getNewSymbol( n, tnn );
       }else if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+        ret = nm->mkNode(n.getKind(), children);
       }else{
         ret = n;
       }
@@ -778,18 +786,24 @@ Node SortInference::simplifyNode(
 }
 
 Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::vector< TypeNode > tns;
   tns.push_back( tn1 );
-  TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 );
-  Node f = NodeManager::currentNM()->mkSkolem( "inj", typ, "injection for monotonicity constraint" );
+  TypeNode typ = nm->mkFunctionType(tns, tn2);
+  Node f =
+      sm->mkDummySkolem("inj", typ, "injection for monotonicity constraint");
   Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl;
-  Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 );
-  Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 );
-  Node ret = NodeManager::currentNM()->mkNode( kind::FORALL,
-               NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ),
-               NodeManager::currentNM()->mkNode( kind::OR,
-                 NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(),
-                 v1.eqNode( v2 ) ) );
+  Node v1 = nm->mkBoundVar("?x", tn1);
+  Node v2 = nm->mkBoundVar("?y", tn1);
+  Node ret =
+      nm->mkNode(kind::FORALL,
+                 nm->mkNode(kind::BOUND_VAR_LIST, v1, v2),
+                 nm->mkNode(kind::OR,
+                            nm->mkNode(kind::APPLY_UF, f, v1)
+                                .eqNode(nm->mkNode(kind::APPLY_UF, f, v2))
+                                .negate(),
+                            v1.eqNode(v2)));
   ret = theory::Rewriter::rewrite( ret );
   return ret;
 }
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 1bb85ee81..eeb187984 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -274,6 +274,7 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
   int ret = 1;
   retNode = d_emptyRegexp;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
 
   PairNodeStr dv = std::make_pair( r, c );
   if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) {
@@ -355,7 +356,8 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
             }
           }
           if(ret == 0) {
-            Node sk = NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" );
+            Node sk =
+                sm->mkDummySkolem("rsp", nm->stringType(), "Split RegExp");
             retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);
             if(!rest.isNull()) {
               retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index ad36b8edd..ed9be34bb 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -154,7 +154,8 @@ Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
 Node SkolemCache::mkSkolem(const char* c)
 {
   // TODO: eliminate this
-  Node n = NodeManager::currentNM()->mkSkolem(c, d_strType, "string skolem");
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node n = sm->mkDummySkolem(c, d_strType, "string skolem");
   d_allSkolems.insert(n);
   return n;
 }
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8deba50ca..d18e10a16 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -17,6 +17,7 @@
 #include "theory/strings/theory_strings_preprocess.h"
 
 #include "expr/kind.h"
+#include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
 #include "proof/proof_manager.h"
@@ -58,6 +59,7 @@ Node StringsPreprocess::reduce(Node t,
       << "StringsPreprocess::reduce: " << t << std::endl;
   Node retNode = t;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Node zero = nm->mkConst(Rational(0));
   Node one = nm->mkConst(Rational(1));
   Node negOne = nm->mkConst(Rational(-1));
@@ -266,7 +268,8 @@ Node StringsPreprocess::reduce(Node t,
     std::vector<Node> conc;
     std::vector< TypeNode > argTypes;
     argTypes.push_back(nm->integerType());
-    Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
+    Node u =
+        sm->mkDummySkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
 
     Node lem = nm->mkNode(GEQ, leni, one);
     conc.push_back(lem);
@@ -345,7 +348,7 @@ Node StringsPreprocess::reduce(Node t,
 
     Node emp = Word::mkEmptyWord(s.getType());
     Node sEmpty = s.eqNode(emp);
-    Node k = nm->mkSkolem("k", nm->integerType());
+    Node k = sm->mkDummySkolem("k", nm->integerType());
     Node kc1 = nm->mkNode(GEQ, k, zero);
     Node kc2 = nm->mkNode(LT, k, lens);
     Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
@@ -361,7 +364,8 @@ Node StringsPreprocess::reduce(Node t,
     std::vector<Node> conc2;
     std::vector< TypeNode > argTypes;
     argTypes.push_back(nm->integerType());
-    Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
+    Node u =
+        sm->mkDummySkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
 
     lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens));
     conc2.push_back(lem);
@@ -531,7 +535,7 @@ Node StringsPreprocess::reduce(Node t,
     std::vector<TypeNode> argTypes;
     argTypes.push_back(nm->integerType());
     Node us =
-        nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
+        sm->mkDummySkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
     TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
     Node uf = sc->mkTypedSkolemCached(
         ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
@@ -670,7 +674,8 @@ Node StringsPreprocess::reduce(Node t,
         nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc");
     std::vector<TypeNode> argTypes;
     argTypes.push_back(nm->integerType());
-    Node us = nm->mkSkolem("Us", nm->mkFunctionType(argTypes, t.getType()));
+    Node us =
+        sm->mkDummySkolem("Us", nm->mkFunctionType(argTypes, t.getType()));
     TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
     Node uf = sc->mkTypedSkolemCached(
         ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
@@ -1013,7 +1018,8 @@ Node StringsPreprocess::mkForallInternal(Node bvl, Node body)
   }
   else
   {
-    qvar = nm->mkSkolem("qinternal", nm->booleanType());
+    SkolemManager* sm = nm->getSkolemManager();
+    qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
     // this dummy variable marks that the quantified formula is internal
     qvar.setAttribute(InternalQuantAttribute(), true);
     // remember the dummy variable
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 6b3b5ba0e..eb6145f9c 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -16,6 +16,7 @@
 
 #include <sstream>
 
+#include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "smt/logic_exception.h"
@@ -1126,6 +1127,8 @@ void SortModel::debugPrint( const char* c ){
 
 bool SortModel::checkLastCall()
 {
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   TheoryModel* m = d_state.getModel();
   if( Trace.isOn("uf-ss-warn") ){
     std::vector< Node > eqcs;
@@ -1163,7 +1166,7 @@ bool SortModel::checkLastCall()
       {
         std::stringstream ss;
         ss << "r_" << d_type << "_";
-        Node nn = NodeManager::currentNM()->mkSkolem(
+        Node nn = sm->mkDummySkolem(
             ss.str(), d_type, "enumeration to meet negative card constraint");
         d_fresh_aloc_reps.push_back( nn );
       }
@@ -1184,8 +1187,7 @@ bool SortModel::checkLastCall()
           }
         }
         Node cl = getCardinalityLiteral( d_maxNegCard );
-        Node lem = NodeManager::currentNM()->mkNode(
-            OR, cl, NodeManager::currentNM()->mkAnd(force_cl));
+        Node lem = nm->mkNode(OR, cl, nm->mkAnd(force_cl));
         Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
         d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE);
         return false;
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 75965e2c9..ebbc75e00 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -16,6 +16,7 @@
 #include "theory/uf/ho_extension.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/uf_options.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_rewriter.h"
@@ -66,10 +67,11 @@ Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached)
   std::vector<TypeNode> argTypes = tn.getArgTypes();
   std::vector<Node> skolems;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
   {
-    Node k =
-        nm->mkSkolem("k", argTypes[i], "skolem created for extensionality.");
+    Node k = sm->mkDummySkolem(
+        "k", argTypes[i], "skolem created for extensionality.");
     skolems.push_back(k);
   }
   Node t[2];
@@ -120,6 +122,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
   Node f = TheoryUfRewriter::decomposeHoApply(node, args, true);
   Node new_f = f;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   if (!TheoryUfRewriter::canUseAsApplyUfOperator(f))
   {
     NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f);
@@ -147,7 +150,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
 
         newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end());
         TypeNode nft = nm->mkFunctionType(newTypes, rangeType);
-        new_f = nm->mkSkolem("app_uf", nft);
+        new_f = sm->mkDummySkolem("app_uf", nft);
         for (const Node& v : vs)
         {
           new_f = nm->mkNode(HO_APPLY, new_f, v);
@@ -161,7 +164,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
       else
       {
         // introduce skolem to make a standard APPLY_UF
-        new_f = nm->mkSkolem("app_uf", f.getType());
+        new_f = sm->mkDummySkolem("app_uf", f.getType());
         lem = new_f.eqNode(f);
       }
       Trace("uf-ho-lemma")
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()));
author	Andrew Reynolds <andrew.j.reynolds@gmail.com>	2021-04-07 13:36:15 -0500
committer	GitHub <noreply@github.com>	2021-04-07 18:36:15 +0000
commit	04a494e251a8cc2c90bb429e2858f1c4eb8f88ff (patch)
tree	03b1a5792f2f6ca5537353b86682f427090668da
parent	5059658ee0d6fc65e4cb1652c605895d016cd274 (diff)