From 43b978c7f326cb8d34b5b87d9bdbe9955397d1ce Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 25 Jun 2012 16:00:21 +0000
Subject: [PATCH] Added a warning to arithmetic for a known dio solver bug.
 Somehow the fix never made it to trunk. Do not know how. The fix to the bug
 is pending the hunt for bug 363.

---
 src/theory/arith/dio_solver.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 1ad6dd395..093fef0d5 100644
--- 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;
-- 
2.30.2