Fix for bug 305.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 05159407c975d71f0705c5305e737cb23a9b3301..ec5752d3a6bf0575fda6c5c71deb9f4eb5be4a82 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -587,6 +587,10 @@ Node TheoryArith::callDioSolver(){
     if(lb == ub){
       Assert(lb.getKind() == EQUAL);
       orig = lb;
+    }else if(lb.getKind() == EQUAL){
+      orig = lb;
+    }else if(ub.getKind() == EQUAL){
+      orig = ub;
     }else{
       NodeBuilder<> nb(AND);
       nb << ub << lb;