Fixes crash when modifies set includes a variable twice.

1 files changed, 2 insertions, 1 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc
index 9bfa56ab..836d8c0a 100644
--- a/Source/VCGeneration/ConditionGeneration.ssc
+++ b/Source/VCGeneration/ConditionGeneration.ssc
@@ -513,7 +513,8 @@ namespace VC
       Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();

       assume impl.Proc != null;

       foreach (IdentifierExpr! ie in impl.Proc.Modifies) {

-        oldFrameMap.Add((!)ie.Decl, ie);

+        if (!oldFrameMap.Contains((!)ie.Decl))

+          oldFrameMap.Add(ie.Decl, ie);

       }

       Substitution oldFrameSubst = Substituter.SubstitutionFromHashtable(oldFrameMap);