From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Mar 2020 18:34:18 +0000 (-0500)
Subject: Ensure legal candidate equalities when using relational triggers (#4035)
X-Git-Tag: cvc5-1.0.0~3502
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f906530aa75e9c21e7877cac30cd3cb8245e3058;p=cvc5.git

Ensure legal candidate equalities when using relational triggers (#4035)
---

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 8e09ef6a2..2a123e59c 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -146,7 +146,9 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){
     Node n = (*d_eqc_false);
     ++d_eqc_false;
     if( n.getKind()==d_match_pattern.getKind() ){
-      if( n[0].getType().isComparableTo( d_match_pattern_type ) ){
+      if (n[0].getType().isComparableTo(d_match_pattern_type)
+          && isLegalCandidate(n))
+      {
         //found an iff or equality, try to match it
         //DO_THIS: cache to avoid redundancies?
         //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?