Fix for bug 439. Delta computation now includes disequality information.

1 files changed, 6 insertions, 3 deletions

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 83e2a4f2b..bcc65b85d 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -175,16 +175,19 @@ public:
     return d_ubc[x] != NullConstraint;
   }
 
-  const Rational& getDelta(){
+  const Rational& getDelta(const Rational& init = Rational(1)){
+    Assert(init.sgn() > 0);
     if(!d_deltaIsSafe){
-      computeDelta();
+      computeDelta(init);
+    }else if(init < d_delta){
+      d_delta = init;
     }
     return d_delta;
   }
 
 private:
 
-  void computeDelta();
+  void computeDelta(const Rational& init);
   void deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u);
 
   /**