From: Tim King <taking@cs.nyu.edu>
Date: Wed, 22 Feb 2012 22:32:45 +0000 (+0000)
Subject: Fix for bug 305.
X-Git-Tag: cvc5-1.0.0~8308
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=88e588fdf712dcfa7f1ca185ee6e7b15305ba84b;p=cvc5.git

Fix for bug 305.
---

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;