Added a warning to arithmetic for a known dio solver bug. Somehow the fix never made...

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 1ad6dd39582b5f9a8b676cb7cc28761dc7875a50..093fef0d5181a90e8900fa32b2b948af68fd43af 100644 (file)
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -213,6 +213,9 @@ 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;
+      }
       nb << input[0] << input[1];
     }else{
       nb << input;