From 4ba0d73db87df39dd1f3d943ff5415b9f104d3e1 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 26 Oct 2012 21:14:58 +0000
Subject: [PATCH] Fix for bug 430. d_delta in PartialModel was never being
 computed. (Delta remained at its initial non-sensical value of -1.)  There
 was a problem with guarding d_delta with d_deltaIsSafe in PartialModel.

---
 src/theory/arith/partial_model.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 7e4a2daad..73e7943b0 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -91,6 +91,9 @@ void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){
   ++d_mapSize;
 
   d_hasSafeAssignment.push_back( false );
+  // Is wirth mentioning that this is not strictly necessary, but this maintains the internal invariant
+  // that when d_assignment is set this gets set.
+  d_deltaIsSafe = false;
   d_assignment.push_back( r );
   d_safeAssignment.push_back( DeltaRational(0) );
 
@@ -146,6 +149,7 @@ void ArithPartialModel::setLowerBoundConstraint(Constraint c){
   Assert(inMaps(x));
   Assert(greaterThanLowerBound(x, c->getValue()));
 
+  d_deltaIsSafe = false;
   d_lbc.set(x, c);
 }
 
@@ -159,6 +163,7 @@ void ArithPartialModel::setUpperBoundConstraint(Constraint c){
   Assert(inMaps(x));
   Assert(lessThanUpperBound(x, c->getValue()));
 
+  d_deltaIsSafe = false;
   d_ubc.set(x, c);
 }
 
@@ -240,7 +245,7 @@ void ArithPartialModel::clearSafeAssignments(bool revert){
   }
 
   if(revert && !d_history.empty()){
-    d_deltaIsSafe = true;
+    d_deltaIsSafe = false;
   }
 
   d_history.clear();
-- 
2.30.2