diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-26 15:45:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-26 15:45:27 -0500 |
commit | d48fc396512ede240e30952793abefce719726d1 (patch) | |
tree | c2c9532d0d77fbf1b62f89186022c161d1864f91 /src/theory/quantifiers | |
parent | 19442febecd2a14fe9a62a22d6fb174e013ee50e (diff) |
Fix assertion for relational triggers (#2096)
Diffstat (limited to 'src/theory/quantifiers')
-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; } } |