Merge branch 'master' into fixErrorSetfixErrorSet

1 files changed, 13 insertions, 10 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 76a0c363d..cf2373b9f 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -193,9 +193,9 @@ void TheoryArith::postCheck(Effort level)
   if (Theory::fullEffort(level))
   {
     d_arithModelCache.clear();
+    std::set<Node> termSet;
     if (d_nonlinearExtension != nullptr)
     {
-      std::set<Node> termSet;
       updateModelCache(termSet);
       d_nonlinearExtension->checkFullEffort(d_arithModelCache, termSet);
     }
@@ -204,6 +204,15 @@ void TheoryArith::postCheck(Effort level)
       // set incomplete
       d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED);
     }
+    // If we won't be doing a last call effort check (which implies that
+    // models will be computed), we must sanity check the integer model
+    // from the linear solver now. We also must update the model cache
+    // if we did not do so above.
+    if (d_nonlinearExtension == nullptr)
+    {
+      updateModelCache(termSet);
+    }
+    sanityCheckIntegerModel();
   }
 }
 
@@ -274,12 +283,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
 
   updateModelCache(termSet);
 
-  if (sanityCheckIntegerModel())
-  {
-    // We added a lemma
-    return false;
-  }
-
   // We are now ready to assert the model.
   for (const std::pair<const Node, Node>& p : d_arithModelCache)
   {
@@ -383,9 +386,9 @@ bool TheoryArith::sanityCheckIntegerModel()
       Trace("arith-check") << p.first << " -> " << p.second << std::endl;
       if (p.first.getType().isInteger() && !p.second.getType().isInteger())
       {
-        Assert(false) << "TheoryArithPrivate generated a bad model value for "
-                        "integer variable "
-                      << p.first << " : " << p.second;
+        Warning() << "TheoryArithPrivate generated a bad model value for "
+                     "integer variable "
+                  << p.first << " : " << p.second;
         // must branch and bound
         TrustNode lem =
             d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());