From d48fc396512ede240e30952793abefce719726d1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 26 Jun 2018 15:45:27 -0500 Subject: [PATCH] Fix assertion for relational triggers (#2096) --- src/theory/quantifiers/ematching/inst_match_generator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; } } -- 2.30.2