From 88e588fdf712dcfa7f1ca185ee6e7b15305ba84b Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 22 Feb 2012 22:32:45 +0000
Subject: [PATCH] Fix for bug 305.

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

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 05159407c..ec5752d3a 100644
--- 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;
-- 
2.30.2