From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Jun 2018 20:45:27 +0000 (-0500)
Subject: Fix assertion for relational triggers (#2096)
X-Git-Tag: cvc5-1.0.0~4945
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d48fc396512ede240e30952793abefce719726d1;p=cvc5.git

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 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;
         }
       }