diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-10-27 14:57:20 -0700 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-10-27 14:57:20 -0700 |
| commit | f85de495b15cfccc8496092d50133368ac35454c (patch) | |
| tree | b80f8cf72bc84800fdcf1fcbe1becda9f0d58db6 /Source/Dafny/Rewriter.cs | |
| parent | 2baf2a8c527599f43de99688f92402f9d979bc48 (diff) | |
Make autoreqs of free requires not free
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 14ea65fa..6034e207 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -742,7 +742,7 @@ namespace Microsoft.Dafny List<Expression> local_auto_reqs = generateAutoReqs(req.E);
foreach (Expression local_auto_req in local_auto_reqs)
{
- auto_reqs.Add(new MaybeFreeExpression(local_auto_req, req.IsFree));
+ auto_reqs.Add(new MaybeFreeExpression(local_auto_req, !req.IsFree));
}
}
method.Req.InsertRange(0, auto_reqs); // Need to come before the actual requires
|