summaryrefslogtreecommitdiff
path: root/Source/Core/OwickiGries.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/OwickiGries.cs')
-rw-r--r--Source/Core/OwickiGries.cs3
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index ed4d8dbb..92529f8f 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -708,8 +708,11 @@ namespace Microsoft.Boogie
if (proc == null) continue;
if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
{
+ HashSet<Variable> modifiedVars = new HashSet<Variable>();
+ proc.Modifies.Iter(x => modifiedVars.Add(x.Decl));
foreach (GlobalVariable g in program.GlobalVariables())
{
+ if (modifiedVars.Contains(g)) continue;
proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));
}
}