Fix issue #3

Don't need to record whether codeContext contains QuantifierExpr except
for functions (which is used to adjust fuel for function calls in
assume/assert context).
Closes #3

Source/Dafny/DafnyAst.cs

@@ -2407,7 +2407,6 @@ public interface ICodeContext
     bool MustReverify { get; }
     string FullSanitizedName { get; }
     bool AllowsNontermination { get; }
-    bool ContainsQuantifier { get;  set; }
   }
   /// <summary>
   /// An ICallable is a Function, Method, IteratorDecl, or RedirectingTypeDecl.
@@ -2443,10 +2442,6 @@ public class DontUseICallable : ICallable
       get { throw new cce.UnreachableException(); }
       set { throw new cce.UnreachableException(); }
     }
-    public bool ContainsQuantifier {
-      get { throw new cce.UnreachableException(); }
-      set { throw new cce.UnreachableException(); }
-    }
   }
   /// <summary>
   /// An IMethodCodeContext is a Method or IteratorDecl.
@@ -2475,11 +2470,6 @@ public NoContext(ModuleDefinition module)
     bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
     public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
     public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
-    public bool ContainsQuantifier { 
-      get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); }
-      set { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); }
-    }
-
   }
 
   public class IteratorDecl : ClassDecl, IMethodCodeContext
@@ -2507,8 +2497,7 @@ public class IteratorDecl : ClassDecl, IMethodCodeContext
     public Predicate Member_Valid;  // created during registration phase of resolution; its specification is filled in during resolution
     public Method Member_MoveNext;  // created during registration phase of resolution; its specification is filled in during resolution
     public readonly LocalVariable YieldCountVariable;
-    bool containsQuantifier;
-
+
     public IteratorDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,
                         List<Formal> ins, List<Formal> outs,
                         Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> decreases,
@@ -2624,10 +2613,7 @@ public class EverIncreasingType : BasicType
       set { _inferredDecr = value; }
       get { return _inferredDecr; }
     }
-    bool ICodeContext.ContainsQuantifier {
-      set { containsQuantifier = value; }
-      get { return containsQuantifier; }
-    }
+
     ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }
     bool ICodeContext.MustReverify { get { return false; } }
     public bool AllowsNontermination {
@@ -2881,10 +2867,6 @@ public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv
       get { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases
       set { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases
     }
-    bool ICodeContext.ContainsQuantifier {
-      get { throw new cce.UnreachableException(); }
-      set { throw new cce.UnreachableException(); }
-    }
     public new NewtypeDecl ClonedFrom {
       get {
         return (NewtypeDecl)base.ClonedFrom;
@@ -2942,10 +2924,6 @@ public TypeSynonymDecl(IToken tok, string name, List<TypeParameter> typeArgs, Mo
       get { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases
       set { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases
     }
-    bool ICodeContext.ContainsQuantifier {
-      get { throw new cce.UnreachableException(); }
-      set { throw new cce.UnreachableException(); }
-    }
   }
 
   [ContractClass(typeof(IVariableContracts))]
@@ -3499,8 +3477,7 @@ public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext
     public bool IsTailRecursive;  // filled in during resolution
     public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();
     public Method OverriddenMethod;
-    public bool containsQuantifier;
-
+
     public override IEnumerable<Expression> SubExpressions {
       get {
         foreach (var e in Req) {
@@ -3574,10 +3551,6 @@ public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext
       set { _inferredDecr = value; }
       get { return _inferredDecr; }
     }
-    bool ICodeContext.ContainsQuantifier {
-      set { containsQuantifier = value; }
-      get { return containsQuantifier; }
-    }
 
     ModuleDefinition ICodeContext.EnclosingModule {
       get {

Source/Dafny/Resolver.cs

@@ -8249,7 +8249,9 @@ public class ResolveOpts
         e.Type = e.Body.Type;
       } else if (expr is QuantifierExpr) {
         var e = (QuantifierExpr)expr;
-        opts.codeContext.ContainsQuantifier = true;
+        if (opts.codeContext is Function) {
+          ((Function)opts.codeContext).ContainsQuantifier = true;
+        }
         Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
         int prevErrorCount = reporter.Count(ErrorLevel.Error);
         bool _val = true;

Test/dafny4/git-issue3.dfy

@@ -0,0 +1,7 @@
+// RUN: %dafny /compile:0  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+newtype Even = n: int | exists h :: h * 2 == n
+
+
+

Test/dafny4/git-issue3.dfy.expect

@@ -0,0 +1,5 @@
+git-issue3.dfy(4,8): Error: cannot find witness that shows type is inhabited (sorry, for now, only tried 0)
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 0 verified, 1 error