From f906530aa75e9c21e7877cac30cd3cb8245e3058 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Mar 2020 13:34:18 -0500 Subject: [PATCH] Ensure legal candidate equalities when using relational triggers (#4035) --- src/theory/quantifiers/ematching/candidate_generator.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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? -- 2.30.2