Dafny: Fixed bug in autocontracts where the post resolver was run even if there were resolution errors.

1 files changed, 6 insertions, 3 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1463c4c0..81d79085 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -174,11 +174,14 @@ namespace Microsoft.Dafny {
           literalDecl.Signature.Refines = refinedSig;

           var sig = literalDecl.Signature;

           // set up environment

+          var errorCount = ErrorCount;

           ResolveModuleDefinition(m, sig);

 

-          refinementTransformer.PostResolve(m);

-          // give rewriter a chance to do processing

-          rewriter.PostResolve(m);

+          if (ErrorCount == errorCount) {

+            refinementTransformer.PostResolve(m);

+            // give rewriter a chance to do processing

+            rewriter.PostResolve(m);

+          }

         } else if (decl is AliasModuleDecl) {

           var alias = (AliasModuleDecl)decl;

           // resolve the path