diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-10-27 14:47:39 -0700 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-10-27 14:47:39 -0700 |
| commit | a00a390c15af08d71aa836540a5f1af1a65b82c2 (patch) | |
| tree | b1bafc98700e13f39f6cd2873035ddeaeaab8ddf /Source/Dafny/Rewriter.cs | |
| parent | 91986ee21cb9738ef7d3b93a52011e5bf7963ba4 (diff) | |
Fix fixup to opaque-function revealer to deal with zero-argument lemmas
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 53baf8e7..66cad286 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -637,6 +637,12 @@ namespace Microsoft.Dafny reqs = Expression.CreateAnd(reqs, expr);
}
+ if (fn.Formals.Count == 0)
+ {
+ lem.Ens[0] = new MaybeFreeExpression(Expression.CreateImplies(reqs, lem.Ens[0].E));
+ return;
+ }
+
var origForall = (ForallExpr)lem.Ens[0].E;
var origImpl = (BinaryExpr)origForall.Term;
|