Introduce inference ids for quantifier instantiation (#6119)

This makes quantifiers use standard inference ids.

This eliminates the need to track ad-hoc statistics, per instantiation type.

This makes minor modifications to a few interfaces in quantifiers to enable this.

26 files changed, 218 insertions, 131 deletions

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 7acf2e861..7eeba8497 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -123,6 +123,55 @@ const char* toString(InferenceId i)
       return "DATATYPES_SYGUS_MT_BOUND";
     case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS";
 
+    case InferenceId::QUANTIFIERS_INST_E_MATCHING:
+      return "QUANTIFIERS_INST_E_MATCHING";
+    case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE:
+      return "QUANTIFIERS_INST_E_MATCHING_SIMPLE";
+    case InferenceId::QUANTIFIERS_INST_E_MATCHING_MT:
+      return "QUANTIFIERS_INST_E_MATCHING_MT";
+    case InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL:
+      return "QUANTIFIERS_INST_E_MATCHING_MTL";
+    case InferenceId::QUANTIFIERS_INST_E_MATCHING_HO:
+      return "QUANTIFIERS_INST_E_MATCHING_HO";
+    case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN:
+      return "QUANTIFIERS_INST_E_MATCHING_VAR_GEN";
+    case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT:
+      return "QUANTIFIERS_INST_CBQI_CONFLICT";
+    case InferenceId::QUANTIFIERS_INST_CBQI_PROP:
+      return "QUANTIFIERS_INST_CBQI_PROP";
+    case InferenceId::QUANTIFIERS_INST_FMF_EXH:
+      return "QUANTIFIERS_INST_FMF_EXH";
+    case InferenceId::QUANTIFIERS_INST_FMF_FMC:
+      return "QUANTIFIERS_INST_FMF_FMC";
+    case InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH:
+      return "QUANTIFIERS_INST_FMF_FMC_EXH";
+    case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI";
+    case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI";
+    case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM";
+    case InferenceId::QUANTIFIERS_CEGQI_CEX_DEP:
+      return "QUANTIFIERS_CEGQI_CEX_DEP";
+    case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA:
+      return "QUANTIFIERS_CEGQI_VTS_LB_DELTA";
+    case InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA:
+      return "QUANTIFIERS_CEGQI_VTS_UB_DELTA";
+    case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF:
+      return "QUANTIFIERS_CEGQI_VTS_LB_INF";
+    case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD:
+      return "QUANTIFIERS_SYQI_EVAL_UNFOLD";
+    case InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC:
+      return "QUANTIFIERS_SYGUS_QE_PREPROC";
+    case InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT:
+      return "QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT";
+    case InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT:
+      return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT";
+    case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT:
+      return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
+    case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
+      return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
+    case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE";
+    case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ:
+      return "QUANTIFIERS_REDUCE_ALPHA_EQ";
+
     case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
     case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
 
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 8cc678162..f5fda1747 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -201,10 +201,40 @@ enum class InferenceId
   // ---------------------------------- end datatypes theory
 
   //-------------------------------------- quantifiers theory
-  // skolemization
-  QUANTIFIERS_SKOLEMIZE,
-  // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent
-  QUANTIFIERS_REDUCE_ALPHA_EQ,
+  //-------------------- types of instantiations.
+  // Notice the identifiers in this section cover all the techniques used for
+  // quantifier instantiation. The subcategories below are for specific lemmas
+  // that are not instantiation lemmas added, per technique.
+  // instantiation from E-matching
+  QUANTIFIERS_INST_E_MATCHING,
+  // E-matching using simple trigger implementation
+  QUANTIFIERS_INST_E_MATCHING_SIMPLE,
+  // E-matching using multi-triggers
+  QUANTIFIERS_INST_E_MATCHING_MT,
+  // E-matching using linear implementation of multi-triggers
+  QUANTIFIERS_INST_E_MATCHING_MTL,
+  // instantiation due to higher-order matching on top of e-matching
+  QUANTIFIERS_INST_E_MATCHING_HO,
+  // E-matching based on variable triggers
+  QUANTIFIERS_INST_E_MATCHING_VAR_GEN,
+  // conflicting instantiation from conflict-based instantiation
+  QUANTIFIERS_INST_CBQI_CONFLICT,
+  // propagating instantiation from conflict-based instantiation
+  QUANTIFIERS_INST_CBQI_PROP,
+  // instantiation from naive exhaustive instantiation in finite model finding
+  QUANTIFIERS_INST_FMF_EXH,
+  // instantiation from finite model finding based on its model-based algorithm
+  QUANTIFIERS_INST_FMF_FMC,
+  // instantiation from running exhaustive instantiation on a subdomain of
+  // the quantified formula in finite model finding based on its model-based
+  // algorithm
+  QUANTIFIERS_INST_FMF_FMC_EXH,
+  // instantiations from counterexample-guided instantiation
+  QUANTIFIERS_INST_CEGQI,
+  // instantiations from syntax-guided instantiation
+  QUANTIFIERS_INST_SYQI,
+  // instantiations from enumerative instantiation
+  QUANTIFIERS_INST_ENUM,
   //-------------------- counterexample-guided instantiation
   // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose
   // counterexample literal is G1.
@@ -215,6 +245,9 @@ enum class InferenceId
   QUANTIFIERS_CEGQI_VTS_UB_DELTA,
   // infinity > c
   QUANTIFIERS_CEGQI_VTS_LB_INF,
+  //-------------------- syntax-guided instantiation
+  // evaluation unfolding for syntax-guided instantiation
+  QUANTIFIERS_SYQI_EVAL_UNFOLD,
   //-------------------- sygus solver
   // preprocessing a sygus conjecture based on quantifier elimination, of the
   // form Q <=> Q_preprocessed
@@ -227,6 +260,11 @@ enum class InferenceId
   QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT,
   // ~Q where Q is a PBE conjecture with conflicting examples
   QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA,
+  //-------------------- reductions
+  // skolemization
+  QUANTIFIERS_SKOLEMIZE,
+  // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent
+  QUANTIFIERS_REDUCE_ALPHA_EQ,
   //-------------------------------------- end quantifiers theory
 
   // ---------------------------------- sep theory
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 56bd14b33..dcc0e885b 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -483,10 +483,13 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
     //check if we need virtual term substitution (if used delta or infinity)
     bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
     if (d_quantEngine->getInstantiate()->addInstantiation(
-            d_curr_quant, subs, false, false, used_vts))
+            d_curr_quant,
+            subs,
+            InferenceId::QUANTIFIERS_INST_CEGQI,
+            false,
+            false,
+            used_vts))
     {
-      ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
-      //d_added_inst.insert( d_curr_quant );
       return true;
     }else{
       //this should never happen for monotonic selection strategies
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index d69b3f19c..953693f59 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -198,7 +198,7 @@ uint64_t HigherOrderTrigger::addInstantiations()
   return addedHoLemmas + addedFoLemmas;
 }
 
-bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
+bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
 {
   if (options::hoMatching())
   {
@@ -207,7 +207,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     std::vector<TNode> subs;
     for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
     {
-      subs.push_back(m.d_vals[i]);
+      subs.push_back(m[i]);
       vars.push_back(d_qreg.getInstantiationConstant(d_quant, i));
     }
 
@@ -238,7 +238,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     {
       TNode var = ha.first;
       unsigned vnum = var.getAttribute(InstVarNumAttribute());
-      TNode value = m.d_vals[vnum];
+      TNode value = m[vnum];
       Trace("ho-unif-debug") << "  val[" << var << "] = " << value << std::endl;
 
       Trace("ho-unif-debug2") << "initialize lambda information..."
@@ -372,27 +372,29 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
   else
   {
     // do not run higher-order matching
-    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
   }
 }
 
 // recursion depth limited by number of arguments of higher order variables
 // occurring as pattern operators (very small)
-bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
+bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m,
+                                           size_t var_index)
 {
   Trace("ho-unif-debug2") << "send inst " << var_index << " / "
                           << d_ho_var_list.size() << std::endl;
   if (var_index == d_ho_var_list.size())
   {
     // we now have an instantiation to try
-    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
+    return d_quantEngine->getInstantiate()->addInstantiation(
+        d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO);
   }
   else
   {
     Node var = d_ho_var_list[var_index];
     unsigned vnum = var.getAttribute(InstVarNumAttribute());
-    Assert(vnum < m.d_vals.size());
-    Node value = m.d_vals[vnum];
+    Assert(vnum < m.size());
+    Node value = m[vnum];
     Assert(d_lchildren[vnum][0] == value);
     Assert(d_ho_var_bvl.find(var) != d_ho_var_bvl.end());
 
@@ -402,13 +404,13 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
         sendInstantiationArg(m, var_index, vnum, 0, d_ho_var_bvl[var], false);
 
     // reset the value
-    m.d_vals[vnum] = value;
+    m[vnum] = value;
 
     return ret;
   }
 }
 
-bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
+bool HigherOrderTrigger::sendInstantiationArg(std::vector<Node>& m,
                                               unsigned var_index,
                                               unsigned vnum,
                                               unsigned arg_index,
@@ -428,7 +430,7 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
           NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]);
       Trace("ho-unif-debug2") << "  got " << body << std::endl;
       Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body);
-      m.d_vals[vnum] = lam;
+      m[vnum] = lam;
       Trace("ho-unif-debug2") << "  try " << vnum << " -> " << lam << std::endl;
     }
     return sendInstantiation(m, var_index + 1);
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index 3f9ca1507..fcb3cbfee 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -34,15 +34,15 @@ class Trigger;
 /** HigherOrder trigger
  *
  * This extends the trigger class with techniques that post-process
- * instantiations, specified by InstMatch objects, according to a variant of
+ * instantiations, specified by vectors of terms, according to a variant of
  * Huet's algorithm. For details, see Chapter 16 of the Handbook of Automated
  * Reasoning (vol. 2), by Gilles Dowek.
  *
  * The main difference between HigherOrderTrigger and Trigger is the function
  * sendInstantiation(...). Recall that this function is called when its
- * underlying IMGenerator generates an InstMatch m using E-matching technique.
- * We enumerate additional instantiations based on m, when the domain of m
- * contains variables of function type.
+ * underlying IMGenerator generates a vectors of terms m using E-matching
+ * technique. We enumerate additional instantiations based on m, when the
+ * domain of m contains variables of function type.
  *
  * Examples below (f, x, y are universal variables):
  *
@@ -170,7 +170,7 @@ class HigherOrderTrigger : public Trigger
   * matching ground terms to function applications with variable heads.
   * See examples (EX1)-(EX3) above.
   */
-  bool sendInstantiation(InstMatch& m) override;
+  bool sendInstantiation(std::vector<Node>& m, InferenceId id) override;
 
  private:
   //-------------------- current information about the match
@@ -235,7 +235,7 @@ class HigherOrderTrigger : public Trigger
   *   when var_index = 0,1, we are processing possibilities for
   *    instantiation of f1,f2 respectively.
   */
-  bool sendInstantiation(InstMatch& m, unsigned var_index);
+  bool sendInstantiation(std::vector<Node>& m, size_t var_index);
   /** higher-order pattern unification algorithm
    * Sends an instantiation that is equivalent to m via
    * d_quantEngine->addInstantiation(...).
@@ -266,7 +266,7 @@ class HigherOrderTrigger : public Trigger
    *   arg_changed is true, since we modified at least one previous
    *     argument of f1 or f2.
    */
-  bool sendInstantiationArg(InstMatch& m,
+  bool sendInstantiationArg(std::vector<Node>& m,
                             unsigned var_index,
                             unsigned vnum,
                             unsigned arg_index,
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 30fb8d49b..719451d1e 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -42,9 +42,11 @@ IMGenerator::IMGenerator(quantifiers::QuantifiersState& qs,
 {
 }
 
-bool IMGenerator::sendInstantiation(Trigger* tparent, InstMatch& m)
+bool IMGenerator::sendInstantiation(Trigger* tparent,
+                                    InstMatch& m,
+                                    InferenceId id)
 {
-  return tparent->sendInstantiation(m);
+  return tparent->sendInstantiation(m, id);
 }
 
 InstMatchGenerator::InstMatchGenerator(
@@ -426,7 +428,8 @@ int InstMatchGenerator::getMatch(
     if (success)
     {
       Trace("matching-debug2") << "Continue next " << d_next << std::endl;
-      ret_val = continueNextMatch(f, m, qe, tparent);
+      ret_val = continueNextMatch(
+          f, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING);
     }
   }
   if (ret_val < 0)
@@ -442,14 +445,15 @@ int InstMatchGenerator::getMatch(
 int InstMatchGenerator::continueNextMatch(Node q,
                                           InstMatch& m,
                                           QuantifiersEngine* qe,
-                                          Trigger* tparent)
+                                          Trigger* tparent,
+                                          InferenceId id)
 {
   if( d_next!=NULL ){
     return d_next->getNextMatch(q, m, qe, tparent);
   }
   if (d_active_add)
   {
-    return sendInstantiation(tparent, m) ? 1 : -1;
+    return sendInstantiation(tparent, m, id) ? 1 : -1;
   }
   return 1;
 }
@@ -559,7 +563,7 @@ uint64_t InstMatchGenerator::addInstantiations(Node f,
   while (getNextMatch(f, m, qe, tparent) > 0)
   {
     if( !d_active_add ){
-      if (sendInstantiation(tparent, m))
+      if (sendInstantiation(tparent, m, InferenceId::UNKNOWN))
       {
         addedLemmas++;
         if (d_qstate.isInConflict())
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 892096224..7a22a5ded 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -19,6 +19,7 @@
 
 #include <map>
 #include "expr/node_trie.h"
+#include "theory/inference_id.h"
 #include "theory/quantifiers/inst_match.h"
 
 namespace CVC4 {
@@ -118,7 +119,7 @@ public:
    * indicating that an instantiation was enqueued in the quantifier engine's
    * lemma cache.
    */
-  bool sendInstantiation(Trigger* tparent, InstMatch& m);
+  bool sendInstantiation(Trigger* tparent, InstMatch& m, InferenceId id);
   /** The state of the quantifiers engine */
   quantifiers::QuantifiersState& d_qstate;
   /** The quantifiers inference manager */
@@ -426,7 +427,8 @@ class InstMatchGenerator : public IMGenerator {
   int continueNextMatch(Node q,
                         InstMatch& m,
                         QuantifiersEngine* qe,
-                        Trigger* tparent);
+                        Trigger* tparent,
+                        InferenceId id);
   /** Get inst match generator
    *
    * Gets the InstMatchGenerator that implements the
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 8d89c25d8..a1674e89f 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -232,7 +232,8 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
   if (childIndex == endChildIndex)
   {
     // m is an instantiation
-    if (sendInstantiation(tparent, m))
+    if (sendInstantiation(
+            tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
     {
       addedLemmas++;
       Trace("multi-trigger-cache-debug")
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
index 41f83269c..d70011bfb 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -158,7 +158,8 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
       << "InstMatchGeneratorMultiLinear::getNextMatch : continue match "
       << std::endl;
   Assert(d_next != nullptr);
-  int ret_val = continueNextMatch(q, m, qe, tparent);
+  int ret_val = continueNextMatch(
+      q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
   if (ret_val > 0)
   {
     Trace("multi-trigger-linear")
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 91cb6e929..879bd50b9 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -101,7 +101,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
           if (t.first != r)
           {
             InstMatch m(q);
-            addInstantiations(m, qe, addedLemmas, 0, &(t.second));
+            addInstantiations(m, qe, addedLemmas, 0, &(t.second), tparent);
             if (qs.isInConflict())
             {
               break;
@@ -118,7 +118,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
   if (tat && !qs.isInConflict())
   {
     InstMatch m(q);
-    addInstantiations(m, qe, addedLemmas, 0, tat);
+    addInstantiations(m, qe, addedLemmas, 0, tat, tparent);
   }
   return addedLemmas;
 }
@@ -127,7 +127,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
                                                  QuantifiersEngine* qe,
                                                  uint64_t& addedLemmas,
                                                  size_t argIndex,
-                                                 TNodeTrie* tat)
+                                                 TNodeTrie* tat,
+                                                 Trigger* tparent)
 {
   Debug("simple-trigger-debug")
       << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
@@ -149,7 +150,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     // we do not need the trigger parent for simple triggers (no post-processing
     // required)
-    if (qe->getInstantiate()->addInstantiation(d_quant, m.d_vals))
+    if (sendInstantiation(
+            tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
     {
       addedLemmas++;
       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
@@ -171,7 +173,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
         if (prev.isNull() || prev == t)
         {
           m.setValue(v, t);
-          addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
+          addInstantiations(
+              m, qe, addedLemmas, argIndex + 1, &(tt.second), tparent);
           m.setValue(v, prev);
           if (qs.isInConflict())
           {
@@ -187,7 +190,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
   std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
   if (it != tat->d_data.end())
   {
-    addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second));
+    addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second), tparent);
   }
 }
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
index 72a3b4959..dd8746f71 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -104,7 +104,8 @@ class InstMatchGeneratorSimple : public IMGenerator
                          QuantifiersEngine* qe,
                          uint64_t& addedLemmas,
                          size_t argIndex,
-                         TNodeTrie* tat);
+                         TNodeTrie* tat,
+                         Trigger* tparent);
 };
 
 }  // namespace inst
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 9855441f1..257684704 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -204,11 +204,6 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
       hasInst = numInst > 0 || hasInst;
       Trace("process-trigger")
           << "  Done, numInst = " << numInst << "." << std::endl;
-      d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
-      if (r == 1)
-      {
-        d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
-      }
       if (d_qstate.isInConflict())
       {
         break;
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index 289c5150b..c9e566b77 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -135,11 +135,6 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
     unsigned numInst = t->addInstantiations();
     Trace("process-trigger")
         << "  Done, numInst = " << numInst << "." << std::endl;
-    d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
-    if (t->isMultiTrigger())
-    {
-      d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
-    }
     if (d_qstate.isInConflict())
     {
       // we are already in conflict
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index ef9b8063f..7d397403d 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -150,9 +150,14 @@ uint64_t Trigger::addInstantiations()
   return gtAddedLemmas + addedLemmas;
 }
 
-bool Trigger::sendInstantiation(InstMatch& m)
+bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
 {
-  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
+  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
+}
+
+bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)
+{
+  return sendInstantiation(m.d_vals, id);
 }
 
 bool Trigger::mkTriggerTerms(Node q,
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 892f453ea..31661e611 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -18,6 +18,7 @@
 #define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 
 #include "expr/node.h"
+#include "theory/inference_id.h"
 
 namespace CVC4 {
 namespace theory {
@@ -208,7 +209,9 @@ class Trigger {
    * but in some cases (e.g. higher-order) we may modify m before calling
    * Instantiate::addInstantiation(...).
    */
-  virtual bool sendInstantiation(InstMatch& m);
+  virtual bool sendInstantiation(std::vector<Node>& m, InferenceId id);
+  /** inst match version, calls the above method */
+  bool sendInstantiation(InstMatch& m, InferenceId id);
   /**
    * Ensure that all ground subterms of n have been preprocessed. This makes
    * calls to the provided valuation to obtain the preprocessed form of these
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index 1795ec8d3..20e157808 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -67,7 +67,8 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q,
     }
     else
     {
-      ret_val = continueNextMatch(q, m, qe, tparent);
+      ret_val = continueNextMatch(
+          q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
       if (ret_val > 0)
       {
         return ret_val;
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 2ecf3673f..46c27df3d 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -610,7 +610,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       // just exhaustive instantiate
       Node c = mkCondDefault(fmfmc, f);
       d_quant_models[f].addEntry(fmfmc, c, d_false);
-      if (!exhaustiveInstantiate(fmfmc, f, c, -1))
+      if (!exhaustiveInstantiate(fmfmc, f, c))
       {
         return 0;
       }
@@ -697,7 +697,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         // (should only add one instance)
         Node c = mkCond(cond);
         unsigned prevInst = d_addedLemmas;
-        exhaustiveInstantiate(fmfmc, f, c, -1);
+        exhaustiveInstantiate(fmfmc, f, c);
         if (d_addedLemmas == prevInst)
         {
           d_star_insts[f].push_back(i);
@@ -706,7 +706,8 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       }
       // just add the instance
       d_triedLemmas++;
-      if (instq->addInstantiation(f, inst, true))
+      if (instq->addInstantiation(
+              f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, true))
       {
         Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
         d_addedLemmas++;
@@ -746,7 +747,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       int j = d_star_insts[f][i];
       if (temp.addEntry(fmfmc, mcond[j], d_quant_models[f].d_value[j]))
       {
-        if (!exhaustiveInstantiate(fmfmc, f, mcond[j], j))
+        if (!exhaustiveInstantiate(fmfmc, f, mcond[j]))
         {
           // something went wrong, resort to exhaustive instantiation
           return 0;
@@ -810,8 +811,11 @@ class RepBoundFmcEntry : public QRepBoundExt
   FirstOrderModelFmc* d_fm;
 };
 
-bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
-  Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " ";
+bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
+                                             Node f,
+                                             Node c)
+{
+  Trace("fmc-exh") << "----Exhaustive instantiate based on " << c << " ";
   debugPrintCond("fmc-exh", c, true);
   Trace("fmc-exh")<< std::endl;
   RepBoundFmcEntry rbfe(d_qe, c, fm);
@@ -848,7 +852,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       if (ev!=d_true) {
         Trace("fmc-exh-debug") << ", add!";
         //add as instantiation
-        if (d_qe->getInstantiate()->addInstantiation(f, inst, true))
+        if (d_qe->getInstantiate()->addInstantiation(
+                f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true))
         {
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 370a88488..6cad3fff5 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -119,8 +119,13 @@ protected:
   std::map<TypeNode, bool> d_preinitialized_types;
   //--------------------end for preinitialization
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
-  bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
-private:
+  /**
+   * Exhaustively instantiate quantified formula q based on condition c, which
+   * indicate the domain to instantiate.
+   */
+  bool exhaustiveInstantiate(FirstOrderModelFmc* fm, Node q, Node c);
+
+ private:
   void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
 
   void doNegate( Def & dc );
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 297a3ffcc..6cfb31c53 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -261,8 +261,6 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     }
     d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem;
     d_addedLemmas += mb->getNumAddedLemmas()-prev_alem;
-    d_quantEngine->d_statistics.d_instantiations_fmf_mbqi +=
-        (mb->getNumAddedLemmas() - prev_alem);
   }else{
     if( Trace.isOn("fmf-exh-inst-debug") ){
       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
@@ -291,7 +289,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
           //add as instantiation
-          if (inst->addInstantiation(f, m.d_vals, true))
+          if (inst->addInstantiation(
+                  f, m.d_vals, InferenceId::QUANTIFIERS_INST_FMF_EXH, true))
           {
             addedLemmas++;
             if (d_qstate.isInConflict())
@@ -305,7 +304,6 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         }
         d_addedLemmas += addedLemmas;
         d_triedLemmas += triedLemmas;
-        d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas;
       }
     }else{
       Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 0595484fa..6efcd2adf 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -207,10 +207,10 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd)
     // try instantiation
     failMask.clear();
     /* if (ie->addInstantiation(quantifier, terms)) */
-    if (ie->addInstantiationExpFail(quantifier, terms, failMask, false))
+    if (ie->addInstantiationExpFail(
+            quantifier, terms, failMask, InferenceId::QUANTIFIERS_INST_ENUM))
     {
       Trace("inst-alg-rd") << "Success!" << std::endl;
-      ++(d_quantEngine->d_statistics.d_instantiations_guess);
       return true;
     }
     else
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f6fb9ed75..6c8d826cb 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -100,8 +100,12 @@ void Instantiate::addRewriter(InstantiationRewriter* ir)
   d_instRewrite.push_back(ir);
 }
 
-bool Instantiate::addInstantiation(
-    Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
+bool Instantiate::addInstantiation(Node q,
+                                   std::vector<Node>& terms,
+                                   InferenceId id,
+                                   bool mkRep,
+                                   bool modEq,
+                                   bool doVts)
 {
   // For resource-limiting (also does a time check).
   d_qim.safePoint(ResourceManager::Resource::QuantifierStep);
@@ -319,11 +323,12 @@ bool Instantiate::addInstantiation(
   if (hasProof)
   {
     // use proof generator
-    addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, d_pfInst.get());
+    addedLem =
+        d_qim.addPendingLemma(lem, id, LemmaProperty::NONE, d_pfInst.get());
   }
   else
   {
-    addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
+    addedLem = d_qim.addPendingLemma(lem, id);
   }
 
   if (!addedLem)
@@ -386,12 +391,13 @@ bool Instantiate::addInstantiation(
 bool Instantiate::addInstantiationExpFail(Node q,
                                           std::vector<Node>& terms,
                                           std::vector<bool>& failMask,
+                                          InferenceId id,
                                           bool mkRep,
                                           bool modEq,
                                           bool doVts,
                                           bool expFull)
 {
-  if (addInstantiation(q, terms, mkRep, modEq, doVts))
+  if (addInstantiation(q, terms, id, mkRep, modEq, doVts))
   {
     return true;
   }
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index e55e677df..abdee69ef 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -22,6 +22,7 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "expr/proof.h"
+#include "theory/inference_id.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/quant_util.h"
 #include "util/statistics_registry.h"
@@ -126,12 +127,16 @@ class Instantiate : public QuantifiersUtil
    * This function returns true if the instantiation lemma for quantified
    * formula q for the substitution specified by terms is successfully enqueued
    * via a call to QuantifiersInferenceManager::addPendingLemma.
-   *   mkRep : whether to take the representatives of the terms in the range of
-   *           the substitution m,
-   *   modEq : whether to check for duplication modulo equality in instantiation
-   *           tries (for performance),
-   *   doVts : whether we must apply virtual term substitution to the
-   *           instantiation lemma.
+   * @param q the quantified formula to instantiate
+   * @param terms the terms to instantiate with
+   * @param id the identifier of the instantiation lemma sent via the inference
+   * manager
+   * @param mkRep whether to take the representatives of the terms in the
+   * range of the substitution m,
+   * @param modEq whether to check for duplication modulo equality in
+   * instantiation tries (for performance),
+   * @param doVts whether we must apply virtual term substitution to the
+   * instantiation lemma.
    *
    * This call may fail if it can be determined that the instantiation is not
    * relevant or legal in the current context. This happens if:
@@ -147,6 +152,7 @@ class Instantiate : public QuantifiersUtil
    */
   bool addInstantiation(Node q,
                         std::vector<Node>& terms,
+                        InferenceId id,
                         bool mkRep = false,
                         bool modEq = false,
                         bool doVts = false);
@@ -176,6 +182,7 @@ class Instantiate : public QuantifiersUtil
   bool addInstantiationExpFail(Node q,
                                std::vector<Node>& terms,
                                std::vector<bool>& failMask,
+                               InferenceId id,
                                bool mkRep = false,
                                bool modEq = false,
                                bool doVts = false,
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 0aafbde56..7bf7cc09b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2164,7 +2164,10 @@ void QuantConflictFind::checkQuantifiedFormula(Node q,
       }
       // Process the lemma: either add an instantiation or specific lemmas
       // constructed during the isTConstraintSpurious call, or both.
-      if (!qinst->addInstantiation(q, terms))
+      InferenceId id = (d_effort == EFFORT_CONFLICT
+                            ? InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT
+                            : InferenceId::QUANTIFIERS_INST_CBQI_PROP);
+      if (!qinst->addInstantiation(q, terms, id))
       {
         Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
         // This should only happen if the algorithm generates the same
@@ -2188,7 +2191,6 @@ void QuantConflictFind::checkQuantifiedFormula(Node q,
         // ensure that quantified formulas that are more likely to have
         // conflicting instances are checked earlier.
         d_quantEngine->markRelevant(q);
-        ++(d_quantEngine->d_statistics.d_instantiations_qcf);
         if (options::qcfAllConflict())
         {
           isConflict = true;
@@ -2202,7 +2204,6 @@ void QuantConflictFind::checkQuantifiedFormula(Node q,
       else if (d_effort == EFFORT_PROP_EQ)
       {
         d_quantEngine->markRelevant(q);
-        ++(d_quantEngine->d_statistics.d_instantiations_qcf);
       }
     }
     // clean up assigned
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index fa6d80085..bbc13b463 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -286,7 +286,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
 
     if (mode == options::SygusInstMode::PRIORITY_INST)
     {
-      if (!inst->addInstantiation(q, terms))
+      if (!inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI))
       {
         sendEvalUnfoldLemmas(eval_unfold_lemmas);
       }
@@ -295,13 +295,13 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
     {
       if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
       {
-        inst->addInstantiation(q, terms);
+        inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
       }
     }
     else
     {
       Assert(mode == options::SygusInstMode::INTERLEAVE);
-      inst->addInstantiation(q, terms);
+      inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
       sendEvalUnfoldLemmas(eval_unfold_lemmas);
     }
   }
@@ -313,7 +313,8 @@ bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
   for (const Node& lem : lemmas)
   {
     Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
-    added_lemma |= d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
+    added_lemma |=
+        d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD);
   }
   return added_lemma;
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 401857206..24919fae0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -767,21 +767,12 @@ QuantifiersEngine::Statistics::Statistics()
       d_ematching_time("theory::QuantifiersEngine::time_ematching"),
       d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
       d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
-      d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
+      d_instantiation_rounds_lc(
+          "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
       d_triggers("QuantifiersEngine::Triggers", 0),
       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
-      d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
-      d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
-      d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
-      d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
-      d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
-      d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
-      d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
-      d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
-      d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
-      d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
-      d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
+      d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_time);
   smtStatisticsRegistry()->registerStat(&d_qcf_time);
@@ -792,17 +783,7 @@ QuantifiersEngine::Statistics::Statistics()
   smtStatisticsRegistry()->registerStat(&d_triggers);
   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
-  smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
   smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
 }
 
 QuantifiersEngine::Statistics::~Statistics(){
@@ -815,17 +796,7 @@ QuantifiersEngine::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
-  smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
   smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
 }
 
 Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 5fca96f0d..91c21a650 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -247,17 +247,7 @@ public:
     IntStat d_triggers;
     IntStat d_simple_triggers;
     IntStat d_multi_triggers;
-    IntStat d_multi_trigger_instantiations;
     IntStat d_red_alpha_equiv;
-    IntStat d_instantiations_user_patterns;
-    IntStat d_instantiations_auto_gen;
-    IntStat d_instantiations_guess;
-    IntStat d_instantiations_qcf;
-    IntStat d_instantiations_qcf_prop;
-    IntStat d_instantiations_fmf_exh;
-    IntStat d_instantiations_fmf_mbqi;
-    IntStat d_instantiations_cbqi;
-    IntStat d_instantiations_rr;
     Statistics();
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */