From c89b0605d5ff327f140f3b0be87796f086228640 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Sat, 29 Sep 2012 20:42:16 +0000
Subject: Calling the setIncompleteness() flag on all full checks once a
 non-linear term has been seen.

---
 src/theory/arith/theory_arith.h | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/theory/arith/theory_arith.h')

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()
-- 
cgit v1.2.3