diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_abduct.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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 |