4 files changed, 17 insertions, 16 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 460877a23..3cb5464da 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -325,7 +325,7 @@ Constraint ConstraintValue::getCeiling() {
 
   DeltaRational ceiling(getValue().ceiling());
 
-#warning "Optimize via the iterator"
+  // TODO: "Optimize via the iterator"
   return d_database->getConstraint(getVariable(), getType(), ceiling);
 }
 
@@ -334,7 +334,7 @@ Constraint ConstraintValue::getFloor() {
 
   DeltaRational floor(Rational(getValue().floor()));
 
-#warning "Optimize via the iterator"
+  // TODO: "Optimize via the iterator"
   return d_database->getConstraint(getVariable(), getType(), floor);
 }
 
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 1b3a5cac7..613ce8368 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -504,7 +504,7 @@ SumPair DioSolver::processEquationsForCut(){
 
 
 SumPair DioSolver::purifyIndex(TrailIndex i){
-#warning "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient."
+  // TODO: "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient."
 
   SumPair curr = d_trail[i].d_eq;
 
@@ -612,7 +612,10 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::solveIndex(DioS
 
   Debug("arith::dio") << "before solveIndex("<<i<<":"<<si.getNode()<< ")" << endl;
 
+#ifdef CVC4_ASSERTIONS
   const Polynomial& p = si.getPolynomial();
+#endif
+
   Assert(p.isIntegral());
 
   Assert(p.selectAbsMinimum() == d_trail[i].d_minimalMonomial);
@@ -644,7 +647,10 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::decomposeIndex(
 
   Debug("arith::dio") << "before decomposeIndex("<<i<<":"<<si.getNode()<< ")" << endl;
 
+#ifdef CVC4_ASSERTIONS
   const Polynomial& p = si.getPolynomial();
+#endif
+
   Assert(p.isIntegral());
 
   Assert(p.selectAbsMinimum() == d_trail[i].d_minimalMonomial);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e183e0e1b..7f0088f5b 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -53,8 +53,8 @@ namespace arith {
 const uint32_t RESET_START = 2;
 
 
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
-  Theory(THEORY_ARITH, c, u, out, valuation),
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+  Theory(THEORY_ARITH, c, u, out, valuation, logicInfo),
   d_hasDoneWorkSinceCut(false),
   d_learner(d_pbSubstitutions),
   d_setupLiteralCallback(this),
@@ -904,7 +904,7 @@ Comparison TheoryArith::mkIntegerEqualityFromAssignment(ArithVar v){
 }
 
 Node TheoryArith::dioCutting(){
-  context::Context::ScopedPush speculativePush(getContext());
+  context::Context::ScopedPush speculativePush(getSatContext());
   //DO NOT TOUCH THE OUTPUTSTREAM
 
   //TODO: Improve this
@@ -1043,7 +1043,7 @@ Node TheoryArith::assertionCases(TNode assertion){
   //Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind));
   Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion);
 
-  Debug("arith::assertions")  << "arith assertion @" << getContext()->getLevel()
+  Debug("arith::assertions")  << "arith assertion @" << getSatContext()->getLevel()
                               <<"(" << assertion
                               << " \\-> "
     //<< determineLeftVariable(assertion, simpleKind)
@@ -1352,7 +1352,7 @@ void TheoryArith::debugPrintModel(){
 
 Node TheoryArith::explain(TNode n) {
 
-  Debug("arith::explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
+  Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
 
   Constraint c = d_constraintDatabase.lookup(n);
   if(c != NullConstraint){
@@ -1387,7 +1387,7 @@ void TheoryArith::propagate(Effort e) {
     }else if(!c->assertedToTheTheory()){
 
       Node literal = c->getLiteral();
-      Debug("arith::prop") << "propagating @" << getContext()->getLevel() << " " << literal << endl;
+      Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl;
 
       d_out->propagate(literal);
     }else{
@@ -1578,9 +1578,6 @@ Node TheoryArith::getValue(TNode n) {
   }
 }
 
-void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
-}
-
 void TheoryArith::notifyRestart(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
 
@@ -1674,7 +1671,7 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
   if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
      (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
 
-#warning "Policy point"
+    // TODO: "Policy point"
     //We are only going to recreate the functionality for now.
     //In the future this can be improved to generate a temporary constraint
     //if none exists.
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index aa7740c37..59653b62d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -259,7 +259,7 @@ private:
   DeltaRational getDeltaValue(TNode n);
 
 public:
-  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
   virtual ~TheoryArith();
 
   /**
@@ -271,8 +271,6 @@ public:
   void propagate(Effort e);
   Node explain(TNode n);
 
-  void notifyEq(TNode lhs, TNode rhs);
-
   Node getValue(TNode n);
 
   void shutdown(){ }