Fix assertion for relational triggers (#2096)

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 6fd9ae4184cc3d82688ae8144aba839f0ef171b6..90d1815a431a56bdd0046e17bcaec4c30610d00a 100644 (file)
--- 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;
         }
       }