Calling the setIncompleteness() flag on all full checks once a non-linear term has been seen.

2 files changed, 8 insertions, 2 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e552ae5a0..2b0d9149d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -58,7 +58,7 @@ const uint32_t RESET_START = 2;
 
 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
-  d_nlIncomplete(u, false),
+  d_nlIncomplete( false),
   d_qflraStatus(Result::SAT_UNKNOWN),
   d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
@@ -1707,6 +1707,10 @@ void TheoryArith::check(Effort effortLevel){
       }
     }
   }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
+  if(fullEffort(effortLevel) && d_nlIncomplete){
+    // TODO this is total paranoia
+    d_out->setIncomplete();
+  }
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
   if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1c2c942fd..4b3a633cb 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -64,7 +64,9 @@ class InstantiatorTheoryArith;
 class TheoryArith : public Theory {
   friend class InstantiatorTheoryArith;
 private:
-  context::CDO<bool> d_nlIncomplete;
+  bool d_nlIncomplete;
+  // TODO A better would be:
+  //context::CDO<bool> d_nlIncomplete;
 
   enum Result::Sat d_qflraStatus;
   // check()