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 beefe428835975cafe42abeebd00a947ede68a0c..728ba61e81de0cc5a507915f079263a9994f3c93 100644 (file)
--- 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 c1548050a2b427cbc87651a9872b5949f90c1e5c..2674bce39e90c3538df1b68bffd7514ec1cf2d4c 100644 (file)
--- 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);