Fix issue 75. Adjust the fuel for existentials to use more fuel in an assume

context and less in an assert.

1 files changed, 1 insertions, 0 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index aa9ce148..b6e783b4 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -8173,6 +8173,7 @@ namespace Microsoft.Dafny
         e.Type = e.Body.Type;

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

+        opts.codeContext.ContainsQuantifier = true;

         Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution

         int prevErrorCount = reporter.Count(ErrorLevel.Error);

         bool _val = true;