Fixed bug, where prefix predicate was not included in CheckTypeInference visitor

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 738aa71c..9b7e1a98 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1541,6 +1541,7 @@ namespace Microsoft.Dafny
         }

       } else if (member is Function) {

         var f = (Function)member;

+        var errorCount = ErrorCount;

         f.Req.Iter(CheckTypeInference);

         f.Ens.Iter(CheckTypeInference);

         f.Reads.Iter(fe => CheckTypeInference(fe.E));

@@ -1552,6 +1553,10 @@ namespace Microsoft.Dafny
             Error(f.tok, "sorry, tail-call functions are not supported");

           }

         }

+        if (errorCount == ErrorCount && f is CoPredicate) {

+          var cop = (CoPredicate)f;

+          CheckTypeInference_Member(cop.PrefixPredicate);

+        }

       }

     }

     void CheckTypeInference(Expression expr) {