Fix issue 61. Decreases are by default in ghost context. Therefore,

dontCareAboutCompilation flag should be set to false in the ResolveOpts.

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index be47843f..bf417de7 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3463,7 +3463,7 @@ namespace Microsoft.Dafny
       }

       ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false, true));

       foreach (Expression r in f.Decreases.Expressions) {

-        ResolveExpression(r, new ResolveOpts(f, false));

+        ResolveExpression(r, new ResolveOpts(f, false, true));

         // any type is fine

       }

       if (f.Body != null) {