diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 6497bee0b..56edc55c6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -260,11 +260,16 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, if (options::sygusUnifCondIndependent() && !unif_enums[1][e].empty()) { Node eu = unif_enums[1][e][0]; - Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); - Node exp_exc = d_tds->getExplain() - ->getExplanationForEquality(eu, unif_values[1][e][0]) - .negate(); - lems.push_back(nm->mkNode(OR, g.negate(), exp_exc)); + Assert(d_tds->isEnumerator(eu)); + if (d_tds->isPassiveEnumerator(eu)) + { + Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); + Node exp_exc = + d_tds->getExplain() + ->getExplanationForEquality(eu, unif_values[1][e][0]) + .negate(); + lems.push_back(nm->mkNode(OR, g.negate(), exp_exc)); + } } } } |