1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 869d22737..c12f387bc 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -39,7 +39,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe,
       d_sqp(qe)
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-      new SynthConjecture(d_quantEngine, qs, d_statistics)));
+      new SynthConjecture(d_quantEngine, qs, qim, d_statistics)));
   d_conj = d_conjs.back().get();
 }
 
@@ -160,7 +160,7 @@ void SynthEngine::assignConjecture(Node q)
   if (d_conjs.back()->isAssigned())
   {
     d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-        new SynthConjecture(d_quantEngine, d_qstate, d_statistics)));
+        new SynthConjecture(d_quantEngine, d_qstate, d_qim, d_statistics)));
   }
   d_conjs.back()->assign(q);
 }
@@ -224,7 +224,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
     bool addedLemma = false;
     for (const Node& lem : cclems)
     {
-      if (d_quantEngine->addLemma(lem))
+      if (d_qim.addPendingLemma(lem))
       {
         ++(d_statistics.d_cegqi_lemmas_ce);
         addedLemma = true;