summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.ssc
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.ssc')
-rw-r--r--Source/VCGeneration/ConditionGeneration.ssc3
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);