From 31ec9bc299901a1a85abbd091c3293af00354030 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 31 Mar 2016 09:10:34 -0700
Subject: Fix issue 75. Adjust the fuel for existentials to use more fuel in an
 assume context and less in an assert.

---
 Source/Dafny/Resolver.cs | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Source/Dafny/Resolver.cs')

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;
-- 
cgit v1.2.3