Dafny: fixed bug in checking postconditions of functions that mention the result the function itself

1 files changed, 4 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 1b8a23ee..c8cc11f6 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1605,8 +1605,10 @@ namespace Microsoft.Dafny {
       // check that postconditions hold

       var ens = new Bpl.EnsuresSeq();

       foreach (Expression p in f.Ens) {

-        bool splitHappened;  // we actually don't care

-        foreach (var s in TrSplitExpr(p, etran, out splitHappened)) {

+        var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f);

+        var splits = new List<SplitExprInfo>();

+        bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, etran);

+        foreach (var s in splits) {

           if (!s.IsFree) {

             ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));

           }