Fixing a bug in proof production for the DioSolver.

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 093fef0d5181a90e8900fa32b2b948af68fd43af..38cff88ff98fc19d6dd93d0c11cc4d5c7685a9ff 100644 (file)
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -213,10 +213,10 @@ Node DioSolver::proveIndex(TrailIndex i){
     Node input = proofVariableToReason(v);
     Assert(acceptableOriginalNodes(input));
     if(input.getKind() == kind::AND){
-      if(input.getNumChildren() != 2){
-        Warning() << "Fix this bug!" << std::endl;
+      for(Node::iterator input_iter = input.begin(), input_end = input.end(); input_iter != input_end; ++input_iter){
+       Node inputChild = *input_iter;
+       nb << inputChild;
       }
-      nb << input[0] << input[1];
     }else{
       nb << input;
     }

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index badfe4c41312a40143ad954d3fffa869c09b743f..6174e9500d8513053da6e4abecc6d6ee1092d5a3 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1521,7 +1521,7 @@ void TheoryArith::check(Effort effortLevel){
       d_partialModel.commitAssignmentChanges();
       revertOutOfConflict();
 
-      if(Debug.isOn("arith::consistency")){
+      if(Debug.isOn("arith::consistency::comitonconflict")){
         entireStateIsConsistent("commit on conflict");
       }
     }
@@ -2083,7 +2083,7 @@ bool TheoryArith::unenqueuedVariablesAreConsistent(){
         }
         Warning() << endl;
         result = false;
-      } else {
+      } else if(Debug.isOn("arith::consistency::initial")){
         d_partialModel.printModel(var);
         Warning() << "Initial var is not consistent for " << var << *i;
         if(d_tableau.isBasic(var)){