summaryrefslogtreecommitdiff
path: root/Source/Core/DeadVarElim.cs
diff options
context:
space:
mode:
authorGravatar Valentin Wüstholz <wuestholz@gmail.com>2015-05-17 13:06:58 +0200
committerGravatar Valentin Wüstholz <wuestholz@gmail.com>2015-05-17 13:06:58 +0200
commit6d5ddf853694b2b8014585dd1e40cc10efbaddea (patch)
treeab44edf958ea01a0dee177c65bb8d34d84851a32 /Source/Core/DeadVarElim.cs
parentd4d66e2ad626eb1539e2b3e3aa0e88ad6b7746aa (diff)
Make caching of verification results more fine-grained for changes that affect preconditions.
Diffstat (limited to 'Source/Core/DeadVarElim.cs')
-rw-r--r--Source/Core/DeadVarElim.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 77086f0f..0feb5e35 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -539,7 +539,7 @@ namespace Microsoft.Boogie {
HavocCmd/*!*/ havocCmd = (HavocCmd)cmd;
foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) {
Contract.Assert(expr != null);
- if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##post##"))) {
+ if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) {
liveSet.Remove(expr.Decl);
}
}