1 files changed, 8 insertions, 4 deletions

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 9d414fcd7..c97ed9714 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -1074,11 +1074,15 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
   Assert(nbSgn != 0);
 
   if(nbSgn > 0){
-    if(d_upperBoundDifference.nothing() || nbDiff <= d_upperBoundDifference){
+    if (d_upperBoundDifference.nothing()
+        || nbDiff <= d_upperBoundDifference.value())
+    {
       return false;
     }
   }else{
-    if(d_lowerBoundDifference.nothing() || nbDiff >= d_lowerBoundDifference){
+    if (d_lowerBoundDifference.nothing()
+        || nbDiff >= d_lowerBoundDifference.value())
+    {
       return false;
     }
   }
@@ -1162,14 +1166,14 @@ UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational&
   if(d_variables.hasUpperBound(nb)){
     ConstraintP ub = d_variables.getUpperBoundConstraint(nb);
     d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb);
-    Border border(ub, d_upperBoundDifference, false, NULL, true);
+    Border border(ub, d_upperBoundDifference.value(), false, NULL, true);
     Debug("handleBorders") << "push back increasing " << border << endl;
     d_increasing.push_back(border);
   }
   if(d_variables.hasLowerBound(nb)){
     ConstraintP lb = d_variables.getLowerBoundConstraint(nb);
     d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb);
-    Border border(lb, d_lowerBoundDifference, false, NULL, false);
+    Border border(lb, d_lowerBoundDifference.value(), false, NULL, false);
     Debug("handleBorders") << "push back decreasing " << border << endl;
     d_decreasing.push_back(border);
   }