From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 21 Dec 2020 13:55:34 +0000 (-0600)
Subject: Fix issue with selector triggers (#5689)
X-Git-Tag: cvc5-1.0.0~2419
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=134ce1704c4f2467a0c5eeef2127afd140d44cc4;p=cvc5.git

Fix issue with selector triggers (#5689)

Code could segfault if the number of wrongly applied selector applications was different from correctly applied ones.
---

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index beefe4288..728ba61e8 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -45,10 +45,6 @@ CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
   Assert(!d_op.isNull());
 }
 
-void CandidateGeneratorQE::resetInstantiationRound(){
-  d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op );
-}
-
 void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); }
 
 void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
@@ -56,6 +52,7 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
   d_term_iter = 0;
   d_eqc = eqc;
   d_op = op;
+  d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms(d_op);
   if( eqc.isNull() ){
     d_mode = cand_term_db;
   }else{
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index c1548050a..2674bce39 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -89,8 +89,6 @@ class CandidateGeneratorQE : public CandidateGenerator
 
  public:
   CandidateGeneratorQE(QuantifiersEngine* qe, Node pat);
-  /** reset instantiation round */
-  void resetInstantiationRound() override;
   /** reset */
   void reset(Node eqc) override;
   /** get next candidate */
@@ -102,7 +100,6 @@ class CandidateGeneratorQE : public CandidateGenerator
   {
     return d_exclude_eqc.find(r) != d_exclude_eqc.end();
   }
-
  protected:
   /** reset this class for matching operator op in equivalence class eqc */
   void resetForOperator(Node eqc, Node op);