1 files changed, 22 insertions, 3 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 5ded7d3d0..bd48a726a 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -40,6 +40,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_model(containing.getSatContext()),
       d_trSlv(d_model),
       d_nlSlv(containing, d_model),
+      d_iandSlv(containing, d_model),
       d_builtModel(containing.getSatContext(), false)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -96,8 +97,9 @@ std::pair<bool, Node> NonlinearExtension::isExtfReduced(
   if (n != d_zero)
   {
     Kind k = n.getKind();
-    return std::make_pair(k != NONLINEAR_MULT && !isTranscendentalKind(k),
-                          Node::null());
+    return std::make_pair(
+        k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND,
+        Node::null());
   }
   Assert(n == d_zero);
   if (on.getKind() == NONLINEAR_MULT)
@@ -402,6 +404,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                                       std::vector<NlLemma>& wlems)
 {
   std::vector<NlLemma> lemmas;
+
   if (options::nlExt())
   {
     // initialize the non-linear solver
@@ -411,6 +414,10 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     // process lemmas that may have been generated by the transcendental solver
     filterLemmas(lemmas, lems);
   }
+  
+  // init last call with IAND
+  d_iandSlv.initLastCall(assertions, false_asserts, xts);
+  
   if (!lems.empty())
   {
     Trace("nl-ext") << "  ...finished with " << lems.size()
@@ -445,7 +452,16 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       return lems.size();
     }
   }
-
+  //-----------------------------------initial lemmas for iand
+  lemmas = d_iandSlv.checkInitialRefine();
+  filterLemmas(lemmas, lems);
+  if (!lems.empty())
+  {
+    Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                    << std::endl;
+    return lems.size();
+  }
+  
   // main calls to nlExt
   if (options::nlExt())
   {
@@ -559,6 +575,9 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       filterLemmas(lemmas, wlems);
     }
   }
+  // run the full refinement in the IAND solver
+  lemmas = d_iandSlv.checkFullRefine();
+  filterLemmas(lemmas, wlems);
 
   Trace("nl-ext") << "  ...finished with " << wlems.size() << " waiting lemmas."
                   << std::endl;