diff options
Diffstat (limited to 'src/preprocessing/passes/ackermann.cpp')
| -rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
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 " |