1 files changed, 7 insertions, 12 deletions
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 7e9fa13e5..a72010bf4 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -28,10 +28,10 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-IAndSolver::IAndSolver(TheoryArith& containing, NlModel& model)
-    : d_containing(containing),
+IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model)
+    : d_im(im),
       d_model(model),
-      d_initRefine(containing.getUserContext())
+      d_initRefine(state.getUserContext())
 {
   NodeManager* nm = NodeManager::currentNM();
   d_true = nm->mkConst(true);
@@ -66,10 +66,9 @@ void IAndSolver::initLastCall(const std::vector<Node>& assertions,
   Trace("iand") << "We have " << d_iands.size() << " IAND terms." << std::endl;
 }
 
-std::vector<NlLemma> IAndSolver::checkInitialRefine()
+void IAndSolver::checkInitialRefine()
 {
   Trace("iand-check") << "IAndSolver::checkInitialRefine" << std::endl;
-  std::vector<NlLemma> lems;
   NodeManager* nm = NodeManager::currentNM();
   for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands)
   {
@@ -101,17 +100,15 @@ std::vector<NlLemma> IAndSolver::checkInitialRefine()
       Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
       Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
                           << std::endl;
-      lems.emplace_back(lem, InferenceId::NL_IAND_INIT_REFINE);
+      d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_INIT_REFINE);
     }
   }
-  return lems;
 }
 
-std::vector<NlLemma> IAndSolver::checkFullRefine()
+void IAndSolver::checkFullRefine()
 {
   Trace("iand-check") << "IAndSolver::checkFullRefine";
   Trace("iand-check") << "IAND terms: " << std::endl;
-  std::vector<NlLemma> lems;
   for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands)
   {
     // the reference bitwidth
@@ -163,12 +160,10 @@ std::vector<NlLemma> IAndSolver::checkFullRefine()
         Node lem = valueBasedLemma(i);
         Trace("iand-lemma")
             << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
-        lems.emplace_back(lem, InferenceId::NL_IAND_VALUE_REFINE);
+        d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_VALUE_REFINE, true);
       }
     }
   }
-
-  return lems;
 }
 
 Node IAndSolver::convertToBvK(unsigned k, Node n) const