1 files changed, 58 insertions, 0 deletions
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 403803a3..eb27c82a 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -265,6 +265,48 @@ namespace Microsoft.Boogie {
       public readonly Hashtable /*string->Variable*//*!*/ VarSymbols = new Hashtable /*string->Variable*/();
       public /*maybe null*/ VarContextNode ParentContext;
       public readonly bool Opaque;
+      readonly ISet<string> assignedAssumptionVariables = new HashSet<string>();
+
+      public bool HasVariableBeenAssigned(string name)
+      {
+        Contract.Requires(name != null);
+
+        if (assignedAssumptionVariables.Contains(name))
+        {
+          return true;
+        }
+        else if (ParentContext != null)
+        {
+          return ParentContext.HasVariableBeenAssigned(name);
+        }
+        else
+        {
+          return false;
+        }
+      }
+
+      public bool MarkVariableAsAssigned(string name)
+      {
+        Contract.Requires(name != null);
+
+        if (VarSymbols.Contains(name))
+        {
+          if (assignedAssumptionVariables.Contains(name))
+          {
+            return false;
+          }
+          assignedAssumptionVariables.Add(name);
+          return true;
+        }
+        else if (ParentContext != null)
+        {
+          return ParentContext.MarkVariableAsAssigned(name);
+        }
+        else
+        {
+          return false;
+        }
+      }
 
       public VarContextNode(/*maybe null*/ VarContextNode parentContext, bool opaque) {
         ParentContext = parentContext;
@@ -349,6 +391,22 @@ namespace Microsoft.Boogie {
       // not present in the relevant levels
       return null;
     }
+
+    public bool HasVariableBeenAssigned(string name)
+    {
+      Contract.Requires(name != null);
+
+      return varContext.HasVariableBeenAssigned(name);
+    }
+
+    public void MarkVariableAsAssigned(string name)
+    {
+      Contract.Requires(name != null);
+
+      var success = varContext.MarkVariableAsAssigned(name);
+      Contract.Assume(success);
+    }
+
     Hashtable axioms = new Hashtable();
 
     public void AddAxiom(Axiom axiom) {