Fixes 2 issues with assignments. The first is constructing an initial assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked. Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars(). Also added a fuzz test that shows both of these problems to the regressions.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 01db59855..57996a510 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -115,7 +115,7 @@ public:
 
   /* */
   void stopRecordingAssignments(bool revert);
-
+  bool isRecording() { return d_savingAssignments;  }
 
   void setUpperBound(TNode x, const DeltaRational& r);
   void setLowerBound(TNode x, const DeltaRational& r);
@@ -144,6 +144,11 @@ public:
   bool assignmentIsConsistent(TNode x);
 
   void printModel(TNode x);
+
+  void initialize(TNode x, const DeltaRational& r);
+  
+  DeltaRational getSavedAssignment(TNode x) const;
+
 };