summaryrefslogtreecommitdiff
path: root/Source/Concurrency
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-02-24 21:21:55 -0800
committerGravatar qadeer <unknown>2014-02-24 21:21:55 -0800
commitd9dc7b51a3c1af9177f5b70cf7425b1990d25e77 (patch)
tree5c3c38d9b86ceb8110cc6964537ed39b1b678984 /Source/Concurrency
parentbf2a30fd04828fcf3480707ba2916a4d037a4cf3 (diff)
added ReadOnlyStandardVisitor
made the default phase of assertions be 0
Diffstat (limited to 'Source/Concurrency')
-rw-r--r--Source/Concurrency/OwickiGries.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 911258ff..96ee34d6 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -1186,7 +1186,7 @@ namespace Microsoft.Boogie
HashSet<int> attrs = QKeyValue.FindIntAttributes(kv, "phase");
if (attrs.Count == 0)
{
- attrs.Add(int.MaxValue);
+ attrs.Add(0); // default phase of requires, ensures and assertions is 0
}
return attrs;
}