2 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index d4904ebe8..382cb233f 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -35,8 +35,9 @@ namespace theory {
 namespace quantifiers {
 
 InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
-                                         QuantifiersState& qs)
-    : QuantifiersModule(qs, qe),
+                                         QuantifiersState& qs,
+                                         QuantifiersInferenceManager& qim)
+    : QuantifiersModule(qs, qim, qe),
       d_instStrategies(),
       d_isup(),
       d_i_ag(),
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index f22da6ec1..f5b999cea 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -48,7 +48,9 @@ class InstantiationEngine : public QuantifiersModule {
   void doInstantiationRound(Theory::Effort effort);
 
  public:
-  InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs);
+  InstantiationEngine(QuantifiersEngine* qe,
+                      QuantifiersState& qs,
+                      QuantifiersInferenceManager& qim);
   ~InstantiationEngine();
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;