diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 647b16637..b7e6e0c65 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -481,14 +481,17 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, Node c = d_enum_to_candidate[e]; std::vector<Node> enum_lems; d_sygus_unif[c].notifyEnumeration(e, v, enum_lems); - // the lemmas must be guarded by the active guard of the enumerator - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; - for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + if (!enum_lems.empty()) { - enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + // the lemmas must be guarded by the active guard of the enumerator + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + { + enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + } + lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } - lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } } for( unsigned i=0; i<candidates.size(); i++ ){ |