1 files changed, 13 insertions, 11 deletions

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);