From: Tim King <taking@cs.nyu.edu>
Date: Wed, 27 Jun 2012 22:45:51 +0000 (+0000)
Subject: Fixing a bug in proof production for the DioSolver.
X-Git-Tag: cvc5-1.0.0~7956
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86eb789dfb6b79a964912ac8289c2ecb28628667;p=cvc5.git

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 093fef0d5..38cff88ff 100644
--- 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 badfe4c41..6174e9500 100644
--- 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)){