From a00a390c15af08d71aa836540a5f1af1a65b82c2 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@microsoft.com>
Date: Mon, 27 Oct 2014 14:47:39 -0700
Subject: Fix fixup to opaque-function revealer to deal with zero-argument
 lemmas

---
 Source/Dafny/Rewriter.cs | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Source/Dafny')

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;
 
-- 
cgit v1.2.3