summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar stasiran <unknown>2014-01-13 17:23:16 -0800
committerGravatar stasiran <unknown>2014-01-13 17:23:16 -0800
commitdca5ebaacf57702e3270df74a2965e08d9a7d1cb (patch)
treeacdd78ec2d0bb52c9b172800b956fc91203db5b7 /Source
parent64f99060b72b3c56e33e9a1523e24dacf9830288 (diff)
Existential failure checker replaced with universal.
Diffstat (limited to 'Source')
-rw-r--r--Source/Concurrency/MoverCheck.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 61e3bf02..75e1f7e3 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -462,7 +462,7 @@ namespace Microsoft.Boogie
this.decls.Add(proc);
}
- private void CreateFailurePreservationCheckerForall(Program program, ActionInfo first, ActionInfo second)
+ private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
{
Debug.Assert(second.isNonBlocking);
if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
@@ -505,7 +505,7 @@ namespace Microsoft.Boogie
this.decls.Add(proc);
}
- private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ private void CreateFailurePreservationCheckerExists(Program program, ActionInfo first, ActionInfo second)
{
if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0 && second.isNonBlocking)
return;