diff options
author | qadeer <unknown> | 2014-04-25 16:51:43 -0700 |
---|---|---|
committer | qadeer <unknown> | 2014-04-25 16:51:43 -0700 |
commit | 121071b9f87d23eaeba176897b9655cd540fb694 (patch) | |
tree | 45ae54e9354509ad6e490e5cbd9beaf0c6bfdf2e /Source/Concurrency/MoverCheck.cs | |
parent | 1a114f457299c87f9e9548992659ffc726fe5e7a (diff) |
bug fix in the last update
Diffstat (limited to 'Source/Concurrency/MoverCheck.cs')
-rw-r--r-- | Source/Concurrency/MoverCheck.cs | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 73c1163a..df2eeffd 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -643,10 +643,13 @@ namespace Microsoft.Boogie foreach (AssertCmd assertCmd in first.thatGate)
{
gateExpr = Expr.And(gateExpr, assertCmd.Expr);
+ gateExpr.Type = Type.Bool;
}
- requires.Add(new Requires(false, Expr.Not(gateExpr)));
+ gateExpr = Expr.Not(gateExpr);
+ gateExpr.Type = Type.Bool;
+ requires.Add(new Requires(false, gateExpr));
List<Ensures> ensures = new List<Ensures>();
- Ensures ensureCheck = new Ensures(false, Expr.Not(gateExpr));
+ Ensures ensureCheck = new Ensures(false, gateExpr);
ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);
ensures.Add(ensureCheck);
foreach (AssertCmd assertCmd in second.thisGate)
|