1 files changed, 26 insertions, 24 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 3bf547ceb..df3a304be 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -44,7 +44,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                   containing.getUserContext(),
                   containing.getOutputChannel()),
       d_model(containing.getSatContext()),
-      d_trSlv(d_model),
+      d_trSlv(d_im, d_model),
       d_nlSlv(containing, d_model),
       d_cadSlv(d_im, d_model),
       d_iandSlv(containing, d_model),
@@ -386,9 +386,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     // initialize the non-linear solver
     d_nlSlv.initLastCall(assertions, false_asserts, xts);
     // initialize the trancendental function solver
-    d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas);
-    // process lemmas that may have been generated by the transcendental solver
-    filterLemmas(lemmas, lems);
+    d_trSlv.initLastCall(assertions, false_asserts, xts);
   }
   if (options::nlCad())
   {
@@ -398,11 +396,12 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   // init last call with IAND
   d_iandSlv.initLastCall(assertions, false_asserts, xts);
 
-  if (!lems.empty())
+  if (d_im.hasUsed() || !lems.empty())
   {
-    Trace("nl-ext") << "  ...finished with " << lems.size()
+    unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+    Trace("nl-ext") << "  ...finished with " << count
                     << " new lemmas during registration." << std::endl;
-    return lems.size();
+    return count;
   }
 
   //----------------------------------- possibly split on zero
@@ -423,13 +422,13 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   if (options::nlExt())
   {
     // functions
-    lemmas = d_trSlv.checkTranscendentalInitialRefine();
-    filterLemmas(lemmas, lems);
-    if (!lems.empty())
+    d_trSlv.checkTranscendentalInitialRefine();
+    if (d_im.hasUsed())
     {
-      Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+      unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+      Trace("nl-ext") << "  ...finished with " << count << " new lemmas."
                       << std::endl;
-      return lems.size();
+      return count;
     }
   }
   //-----------------------------------initial lemmas for iand
@@ -456,13 +455,13 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     }
 
     //-----------------------------------monotonicity of transdental functions
-    lemmas = d_trSlv.checkTranscendentalMonotonic();
-    filterLemmas(lemmas, lems);
-    if (!lems.empty())
+    d_trSlv.checkTranscendentalMonotonic();
+    if (d_im.hasUsed())
     {
-      Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+      unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+      Trace("nl-ext") << "  ...finished with " << count << " new lemmas."
                       << std::endl;
-      return lems.size();
+      return count;
     }
 
     //------------------------lemmas based on magnitude of non-zero monomials
@@ -551,8 +550,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     }
     if (options::nlExtTfTangentPlanes())
     {
-      lemmas = d_trSlv.checkTranscendentalTangentPlanes();
-      filterLemmas(lemmas, wlems);
+      d_trSlv.checkTranscendentalTangentPlanes();
     }
   }
   if (options::nlCad())
@@ -572,8 +570,9 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   lemmas = d_iandSlv.checkFullRefine();
   filterLemmas(lemmas, wlems);
 
-  Trace("nl-ext") << "  ...finished with " << wlems.size() << " waiting lemmas."
-                  << std::endl;
+  Trace("nl-ext") << "  ...finished with "
+                  << (wlems.size() + d_im.numWaitingLemmas())
+                  << " waiting lemmas." << std::endl;
 
   return 0;
 }
@@ -614,6 +613,7 @@ void NonlinearExtension::check(Theory::Effort e)
       d_im.doPendingFacts();
       d_im.doPendingLemmas();
       d_im.doPendingPhaseRequirements();
+      d_im.reset();
       return;
     }
     // Otherwise, we will answer SAT. The values that we approximated are
@@ -728,7 +728,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
     {
       complete_status = num_shared_wrong_value > 0 ? -1 : 0;
       checkLastCall(assertions, false_asserts, xts, mlems, wlems);
-      if (!mlems.empty())
+      if (!mlems.empty() || d_im.hasSentLemma() || d_im.hasPendingLemma())
       {
         return true;
       }
@@ -768,10 +768,12 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
     if (complete_status != 1)
     {
       // flush the waiting lemmas
-      if (!wlems.empty())
+      if (!wlems.empty() || d_im.hasWaitingLemma())
       {
+        std::size_t count = wlems.size() + d_im.numWaitingLemmas();
         mlems.insert(mlems.end(), wlems.begin(), wlems.end());
-        Trace("nl-ext") << "...added " << wlems.size() << " waiting lemmas."
+        d_im.flushWaitingLemmas();
+        Trace("nl-ext") << "...added " << count << " waiting lemmas."
                         << std::endl;
         return true;
       }