This commit merges in the changes from branches/arithmetic/refactor0

- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work.
- Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver.
- Fix to an assertion in CDQueue.
- Implements a CDArithVarSet using a vector of booleans and CDList.
- Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h
index f84b66349..d733e0b1c 100644
--- a/src/context/cdqueue.h
+++ b/src/context/cdqueue.h
@@ -122,7 +122,7 @@ public:
       // Some elements have been enqueued and dequeued in the same
       // context and now the queue is empty we can destruct them.
       CDList<T>::truncateList(d_lastsave);
-      Assert(d_size ==  d_lastsave);
+      Assert(CDList<T>::d_size ==  d_lastsave);
       d_iter = d_lastsave;
     }
   }