diff options
| -rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 6fd9ae418..90d1815a4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -421,7 +421,7 @@ int InstMatchGenerator::getNextMatch(Node f, Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl; success = getMatch(f, t, m, qe, tparent); if( d_independent_gen && success<0 ){ - Assert( d_eq_class.isNull() ); + Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull()); d_curr_exclude_match[t] = true; } } |