diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_abduct.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 278d708ee..5cffda78f 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -123,7 +123,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, abvl = agtsd.getSygusVarList(); Assert(!abvl.isNull() && abvl.getKind() == BOUND_VAR_LIST); } - else + else if (!varlist.empty()) { // the bound variable list of the abduct-to-synthesize is determined by // the variable list above @@ -166,8 +166,11 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, aconj = aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl; Node sc = nm->mkNode(AND, aconj, abdApp); - Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); - sc = nm->mkNode(EXISTS, vbvl, sc); + if (!vars.empty()) + { + Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); + sc = nm->mkNode(EXISTS, vbvl, sc); + } Node sygusScVar = sm->mkDummySkolem("sygus_sc", nm->booleanType()); sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); |