1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 0ab2988d2..4c606a273 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -17,7 +17,6 @@
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
 #include "util/hash.h"
@@ -31,10 +30,11 @@ namespace inst {
 HigherOrderTrigger::HigherOrderTrigger(
     QuantifiersEngine* qe,
     quantifiers::QuantifiersInferenceManager& qim,
+    quantifiers::QuantifiersRegistry& qr,
     Node q,
     std::vector<Node>& nodes,
     std::map<Node, std::vector<Node> >& ho_apps)
-    : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps)
+    : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
 {
   NodeManager* nm = NodeManager::currentNM();
   // process the higher-order variable applications
@@ -201,11 +201,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     // get substitution corresponding to m
     std::vector<TNode> vars;
     std::vector<TNode> subs;
-    quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
     for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
     {
       subs.push_back(m.d_vals[i]);
-      vars.push_back(tutil->getInstantiationConstant(d_quant, i));
+      vars.push_back(d_qreg.getInstantiationConstant(d_quant, i));
     }
 
     Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;