Add the ability to specify how much "fuel" a function should have,

i.e., how many times Z3 is permitted to unfold it's definition.  The
new {:fuel} annotation can be added to the function itself, it which
case it will apply to all uses of that function, or it can overridden
within the scope of a module, function, method, iterator, calc, forall,
while, assert, or assume.  The general format is:

{:fuel functionName,lowFuel,highFuel}

When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.

The default fuel setting for recursive functions is 1,2.  Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care.  Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.

10 files changed, 967 insertions, 155 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index f13aa2f4..e313ffac 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -545,7 +545,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is CalcStmt) {

           var s = (CalcStmt)stmt;

-          r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp));

+          r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));

 

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 6cc0af5a..5d4a4321 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1965,6 +1965,7 @@ ModifyStmt<out Statement s>
 CalcStmt<out Statement s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

      Token x;

+     Attributes attrs = null;

      CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;

      var lines = new List<Expression>();

      var hints = new List<BlockStmt>();

@@ -1976,6 +1977,7 @@ CalcStmt<out Statement s>
      IToken danglingOperator = null;

   .)

   "calc"                                                  (. x = t; .)

+  { IF(IsAttribute()) Attribute<ref attrs> }

   [ CalcOp<out opTok, out calcOp>                         (. maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)

                                                              if (maybeOp == null) {

                                                                SemErr(opTok, "the main operator of a calculation must be transitive");

@@ -2024,7 +2026,7 @@ CalcStmt<out Statement s>
       // Repeat the last line to create a dummy line for the dangling hint

       lines.Add(lines[lines.Count - 1]);

     }

-    s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);

+    s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp, attrs);

   .)

   .

 CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b8660f98..c9c9ccc8 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -314,6 +314,22 @@ namespace Microsoft.Dafny {
       return null;

     }

 

+

+    /// <summary>

+    /// Same as FindExpressions, but returns all matches

+    /// </summary>

+    public static List<List<Expression>> FindAllExpressions(Attributes attrs, string nm) {

+      Contract.Requires(nm != null);

+      List<List<Expression>> ret = null;

+      for (; attrs != null; attrs = attrs.Prev) {

+        if (attrs.Name == nm) {

+          ret = ret ?? new List<List<Expression>>();   // Avoid allocating the list in the common case where we don't find nm

+          ret.Add(attrs.Args);

+        }

+      }

+      return ret;

+    }

+

     /// <summary>

     /// Returns true if "nm" is a specified attribute whose arguments match the "allowed" parameter.

     /// - if "nm" is not found in attrs, return false and leave value unmodified.  Otherwise,

@@ -2874,6 +2890,7 @@ namespace Microsoft.Dafny {
     public override string WhatKind { get { return "function"; } }

     public readonly bool IsProtected;

     public bool IsRecursive;  // filled in during resolution

+    public bool IsFueled;  // filled in during resolution if anyone tries to adjust this function's fuel

     public readonly List<TypeParameter> TypeArgs;

     public readonly List<Formal> Formals;

     public readonly Type ResultType;

@@ -2899,7 +2916,7 @@ namespace Microsoft.Dafny {
         return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr);

       }

     }

-

+    

     /// <summary>

     /// The "AllCalls" field is used for non-FixpointPredicate, non-PrefixPredicate functions only (so its value should not be relied upon for FixpointPredicate and PrefixPredicate functions).

     /// It records all function calls made by the Function, including calls made in the body as well as in the specification.

@@ -2944,6 +2961,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(decreases != null);

       this.IsProtected = isProtected;

+      this.IsFueled = false;  // Defaults to false.  Only set to true if someone mentions this function in a fuel annotation

       this.TypeArgs = typeArgs;

       this.Formals = formals;

       this.ResultType = resultType;

@@ -2968,6 +2986,8 @@ namespace Microsoft.Dafny {
     }

     ModuleDefinition ICodeContext.EnclosingModule { get { return this.EnclosingClass.Module; } }

     bool ICodeContext.MustReverify { get { return false; } }

+

+    public bool IsFuelAware() { return IsRecursive || IsFueled; }

   }

 

   public class Predicate : Function

@@ -4640,7 +4660,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(StepOps.Count == Hints.Count);

     }

 

-    public CalcStmt(IToken tok, IToken endTok, CalcOp op, List<Expression> lines, List<BlockStmt> hints, List<CalcOp> stepOps, CalcOp resultOp)

+    public CalcStmt(IToken tok, IToken endTok, CalcOp op, List<Expression> lines, List<BlockStmt> hints, List<CalcOp> stepOps, CalcOp resultOp, Attributes attrs)

       : base(tok, endTok)

     {

       Contract.Requires(tok != null);

@@ -4665,6 +4685,7 @@ namespace Microsoft.Dafny {
       }

       this.Steps = new List<Expression>();

       this.Result = null;

+      this.Attributes = attrs;

     }

 

     public override IEnumerable<Statement> SubStatements

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index b183fff1..c4047819 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -74,8 +74,8 @@ public class Parser {
 	public const int _ellipsis = 58;

 	public const int maxT = 137;

 

-	const bool _T = true;

-	const bool _x = false;

+	const bool T = true;

+	const bool x = false;

 	const int minErrDist = 2;

 

 	public Scanner/*!*/ scanner;

@@ -2565,6 +2565,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void CalcStmt(out Statement s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);

 		Token x;

+		Attributes attrs = null;

 		CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;

 		var lines = new List<Expression>();

 		var hints = new List<BlockStmt>();

@@ -2577,6 +2578,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(31);

 		x = t; 

+		while (IsAttribute()) {

+			Attribute(ref attrs);

+		}

 		if (StartOf(25)) {

 			CalcOp(out opTok, out calcOp);

 			maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)

@@ -2631,7 +2635,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		 // Repeat the last line to create a dummy line for the dangling hint

 		 lines.Add(lines[lines.Count - 1]);

 		}

-		s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);

+		s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp, attrs);

 		

 	}

 

@@ -3988,7 +3992,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			S = Util.RemoveUnderscores(t.val);

 			try {

-             n = BigIntegerParser.Parse(S);

+			 n = BigIntegerParser.Parse(S);

 			} catch (System.FormatException) {

 			 SemErr("incorrectly formatted number");

 			 n = BigInteger.Zero;

@@ -3999,7 +4003,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			S = Util.RemoveUnderscores(t.val.Substring(2));

 			try {

 			 // note: leading 0 required when parsing positive hex numbers

-             n = BigIntegerParser.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);

+			 n = BigIntegerParser.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);

 			} catch (System.FormatException) {

 			 SemErr("incorrectly formatted number");

 			 n = BigInteger.Zero;

@@ -4364,38 +4368,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	static readonly bool[,]/*!*/ set = {

-		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_T, _x,_x,_T,_T, _T,_x,_x,_T, _T,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_T,_T, _T,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_T,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_T, _x,_T,_x,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_T,_T,_T, _x,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_x, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_T, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_T,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_T,_T,_T, _x,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_x,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_T,_T,_T, _x,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _x,_T,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_x,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_T,_T,_T, _x,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _x,_T,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_x,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_T,_T, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_x,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_T,_T,_T, _x,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _x,_T,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _T,_T,_x,_T, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_x,_x,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x},

-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},

-		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x},

-		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x}

+		{T,T,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,T, x,x,T,T, T,x,x,T, T,x,x,T, T,x,T,T, T,T,T,x, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,T,T, x,x,T,T, T,x,x,T, x,x,T,T, T,T,T,T, T,x,T,T, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,T,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,T,x,T, x,T,x,x, T,x,T,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,T,T,T, T,x,x,x, T,x,T,x, x,T,T,T, x,T,T,T, T,x,x,T, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,T, x,x,T,T, T,T,T,T, x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,T, T,T,x,T, T,T,T,x, x,T,x,T, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,T,T,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,T,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,T,T,T, T,x,x,x, T,x,T,x, x,T,T,T, x,T,T,T, T,x,x,T, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,T,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,T, x,x,T,T, T,T,T,T, x,x,x},

+		{T,T,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x},

+		{x,T,T,T, T,x,x,x, T,x,T,x, x,T,T,T, x,T,T,T, T,x,x,T, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,T, x,x,T,T, T,T,T,T, x,x,x},

+		{x,T,T,T, T,x,x,x, T,x,T,x, x,T,T,T, x,T,T,T, T,x,x,T, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,T, x,x,T,T, T,T,T,T, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,T,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x},

+		{x,T,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,T, T,x,T,T, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{x,T,T,T, T,x,x,x, T,x,T,x, x,T,T,T, x,T,T,T, T,x,x,T, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, T,T,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,T, x,x,T,T, T,T,T,T, x,x,x},

+		{x,x,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x},

+		{T,T,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

+		{T,T,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,T,T, T,T,T,T, x,T,T,T, x,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,x,x},

+		{T,T,T,T, T,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,T, T,T,T,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,T,T, T,T,T,T, x,T,T,x, x,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,x,x}

 

 	};

 } // end Parser

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 835871d9..e48a7932 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -455,6 +455,25 @@ namespace Microsoft.Dafny
           }

         }

       }

+

+      // Determine, for each function, whether someone tries to adjust its fuel parameter

+      foreach (var module in prog.Modules) {

+        CheckForFuelAdjustments(module.tok, module.Attributes, module, this);

+        foreach (var clbl in ModuleDefinition.AllItersAndCallables(module.TopLevelDecls)) {

+          Statement body = null;

+          if (clbl is Method) {

+            body = ((Method)clbl).Body;

+            CheckForFuelAdjustments(clbl.Tok,((Method)clbl).Attributes, module, this);

+          } else if (clbl is IteratorDecl) {

+            body = ((IteratorDecl)clbl).Body;

+            CheckForFuelAdjustments(clbl.Tok, ((IteratorDecl)clbl).Attributes, module, this);

+          }

+          if (body != null) {

+            var c = new FuelAdjustment_Visitor(this);

+            c.Visit(body, new FuelAdjustment_Context(module, this));

+          }

+        }

+      }

     }

 

     void FillInDefaultDecreasesClauses(Program prog)

@@ -683,8 +702,8 @@ namespace Microsoft.Dafny
       var datatypeDependencies = new Graph<IndDatatypeDecl>();

       var codatatypeDependencies = new Graph<CoDatatypeDecl>();

       int prevErrorCount = ErrorCount;

-      ResolveAttributes(m.Attributes, new ResolveOpts(new NoContext(m.Module), false));

       ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);

+      ResolveAttributes(m.Attributes, new ResolveOpts(new NoContext(m.Module), false)); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members

       if (ErrorCount == prevErrorCount) {

         ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);

       }

@@ -2336,6 +2355,59 @@ namespace Microsoft.Dafny
     #endregion CheckTailRecursive

 

     // ------------------------------------------------------------------------------------------------------

+    // ----- FuelAdjustmentChecks ---------------------------------------------------------------------------

+    // ------------------------------------------------------------------------------------------------------

+    #region FuelAdjustmentChecks

+

+    protected static void CheckForFuelAdjustments(IToken tok, Attributes attrs, ModuleDefinition currentModule, ResolutionErrorReporter reporter) {

+      List<List<Expression>> results = Attributes.FindAllExpressions(attrs, "fuel");

+

+      if (results != null) {

+        foreach (List<Expression> args in results) {

+          if (args != null && args.Count >= 2) {

+            // Try to extract the function from the first argument

+            MemberSelectExpr selectExpr = args[0].Resolved as MemberSelectExpr;

+            if (selectExpr != null) {

+              Function f = selectExpr.Member as Function;

+              if (f != null) {

+                f.IsFueled = true;

+                if (f.IsProtected && currentModule != f.EnclosingClass.Module) {

+                  reporter.Error(tok, "cannot adjust fuel for protected function {0} from another module", f.Name);

+                }

+              }

+            }

+          }

+        }

+      }

+    }

+

+    public class FuelAdjustment_Context

+    {

+      public ModuleDefinition currentModule;

+      public ResolutionErrorReporter reporter;

+      public FuelAdjustment_Context(ModuleDefinition currentModule, ResolutionErrorReporter reporter) {

+        this.currentModule = currentModule;

+        this.reporter = reporter;

+      }

+    }

+

+    class FuelAdjustment_Visitor : ResolverTopDownVisitor<FuelAdjustment_Context>

+    {

+      public FuelAdjustment_Visitor(Resolver resolver)

+        : base(resolver) {

+        Contract.Requires(resolver != null);

+      }

+

+      protected override bool VisitOneStmt(Statement stmt, ref FuelAdjustment_Context st) {

+        Contract.Requires(stmt != null);

+        Resolver.CheckForFuelAdjustments(stmt.Tok, stmt.Attributes, st.currentModule, st.reporter);

+        return true;

+      }

+    }

+

+    #endregion FuelAdjustmentChecks

+

+    // ------------------------------------------------------------------------------------------------------

     // ----- FixpointPredicateChecks ------------------------------------------------------------------------

     // ------------------------------------------------------------------------------------------------------

     #region FixpointPredicateChecks

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 4c5eedb4..d0d2e4dd 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -217,7 +217,7 @@ public class Scanner {
 

 	[ContractInvariantMethod]

 	void objectInvariant(){

-		Contract.Invariant(this._buffer != null);

+		Contract.Invariant(buffer!=null);

 		Contract.Invariant(t != null);

 		Contract.Invariant(start != null);

 		Contract.Invariant(tokens != null);

@@ -227,18 +227,7 @@ public class Scanner {
 		Contract.Invariant(errorHandler != null);

 	}

 

-	private Buffer/*!*/ _buffer; // scanner buffer

-

-	public Buffer/*!*/ buffer {

-		get {

-			Contract.Ensures(Contract.Result<Buffer>() != null);

-			return this._buffer;

-		}

-		set {

-			Contract.Requires(value != null);

-			this._buffer = value;

-		}

-	}

+	public Buffer/*!*/ buffer; // scanner buffer

 

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

@@ -310,7 +299,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() {

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -318,8 +307,8 @@ public class Scanner {
 		t = new Token(); // dummy because t is a non-null field

 		try {

 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

-			this._buffer = new Buffer(stream, false);

-			Filename = useBaseName? GetBaseName(fileName): fileName;

+			buffer = new Buffer(stream, false);

+			Filename = fileName;

 			Init();

 		} catch (IOException) {

 			throw new FatalError("Cannot open file " + fileName);

@@ -327,22 +316,18 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName = false) : base() {

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

 		pt = tokens = new Token();  // first token is a dummy

 		t = new Token(); // dummy because t is a non-null field

-		this._buffer = new Buffer(s, true);

+		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

-		this.Filename = useBaseName? GetBaseName(fileName) : fileName;

+		this.Filename = fileName;

 		Init();

 	}

 

-    string GetBaseName(string fileName) {

-        return System.IO.Path.GetFileName(fileName); // Return basename

-    }

-

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4324b2b8..9ba11e2f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -114,6 +114,7 @@ namespace Microsoft.Dafny {
     readonly Dictionary<string, Bpl.Constant> fieldConstants = new Dictionary<string,Constant>();

     readonly ISet<string> abstractTypes = new HashSet<string>();

     readonly ISet<string> opaqueTypes = new HashSet<string>();

+    FuelContext fuelContext = null;

     Program program;

 

     [ContractInvariantMethod]

@@ -625,6 +626,11 @@ namespace Microsoft.Dafny {
     }

     void AddTypeDecl(NewtypeDecl dd) {

       Contract.Requires(dd != null);

+      Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));      

+

+      FuelContext oldFuelContext = this.fuelContext;

+      this.fuelContext = FuelSetting.NewFuelContext(dd);

+

       AddTypeDecl_Aux(dd.tok, dd.FullName, new List<TypeParameter>());

       AddWellformednessCheck(dd);

       // Add $Is and $IsAlloc axioms for the newtype

@@ -667,6 +673,7 @@ namespace Microsoft.Dafny {
 

         sink.AddTopLevelDeclaration(new Bpl.Axiom(dd.tok, BplForall(vars, BplTrigger(is_o), body), name));

       });

+      this.fuelContext = oldFuelContext;

     }

     void AddTypeDecl_Aux(IToken tok, string nm, List<TypeParameter> typeArgs) {

       Contract.Requires(tok != null);

@@ -1181,7 +1188,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    Bpl.Expr LayerSucc(Bpl.Expr e, int amt = 1) {

+    public Bpl.Expr LayerSucc(Bpl.Expr e, int amt = 1) {

       if (amt == 0) {

         return e;

       } else if (amt > 0) {

@@ -1301,6 +1308,7 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(c != null);

+      Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));

 

       sink.AddTopLevelDeclaration(GetClass(c));

       if (c is ArrayClassDecl) {

@@ -1387,6 +1395,9 @@ namespace Microsoft.Dafny {
 

         } else if (member is Function) {

           var f = (Function)member;

+          FuelContext oldFuelContext = this.fuelContext;

+          this.fuelContext = FuelSetting.NewFuelContext(f);

+

           AddClassMember_Function(f);

           if (!IsOpaqueFunction(f) && !f.IsBuiltin && !(f.tok is IncludeToken)) { // Opaque function's well-formedness is checked on the full version

             AddWellformednessCheck(f);

@@ -1399,9 +1410,11 @@ namespace Microsoft.Dafny {
             AddClassMember_Function(cop.PrefixPredicate);

             // skip the well-formedness check, because it has already been done for the fixpoint-predicate

           }

-

+          this.fuelContext = oldFuelContext;

         } else if (member is Method) {

           Method m = (Method)member;

+          FuelContext oldFuelContext = this.fuelContext;

+          this.fuelContext = FuelSetting.NewFuelContext(m);

 

           // wellformedness check for method specification

           if (m.EnclosingClass is IteratorDecl && m == ((IteratorDecl)m.EnclosingClass).Member_MoveNext) {

@@ -1434,7 +1447,7 @@ namespace Microsoft.Dafny {
             sink.AddTopLevelDeclaration(proc);

             AddMethodImpl(m, proc, false);

           }

-

+          this.fuelContext = oldFuelContext;

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member

         }

@@ -1467,7 +1480,7 @@ namespace Microsoft.Dafny {
       // declare function

       AddFunction(f);

       // add synonym axiom

-      if (f.IsRecursive) {

+      if (f.IsFuelAware()) {

         AddSynonymAxiom(f);

       }

       // add frame axiom

@@ -1494,6 +1507,10 @@ namespace Microsoft.Dafny {
 

     void AddIteratorSpecAndBody(IteratorDecl iter) {

       Contract.Requires(iter != null);

+      Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));

+

+      FuelContext oldFuelContext = this.fuelContext;      

+      this.fuelContext = FuelSetting.NewFuelContext(iter);

 

       // wellformedness check for method specification

       Bpl.Procedure proc = AddIteratorProc(iter, MethodTranslationKind.SpecWellformedness);

@@ -1506,6 +1523,7 @@ namespace Microsoft.Dafny {
         // ...and its implementation

         AddIteratorImpl(iter, proc);

       }

+      this.fuelContext = oldFuelContext;

     }

 

     Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) {

@@ -1950,7 +1968,7 @@ namespace Microsoft.Dafny {
       var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);

       var args = new List<Bpl.Expr>();

       Bpl.BoundVariable layer;

-      if (f.IsRecursive) {

+      if (f.IsFuelAware()) {

         layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));

         formals.Add(layer);

         // Note, "layer" is not added to "args" here; rather, that's done below, as needed

@@ -2121,7 +2139,7 @@ namespace Microsoft.Dafny {
       var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);

 

       Bpl.BoundVariable layer;

-      if (f.IsRecursive) {

+      if (f.IsFuelAware()) {

         layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));

         formals.Add(layer);

         // Note, "layer" is not added to "args" here; rather, that's done below, as needed

@@ -2317,7 +2335,7 @@ namespace Microsoft.Dafny {
 

     void AddSynonymAxiom(Function f) {

       Contract.Requires(f != null);

-      Contract.Requires(f.IsRecursive);

+      Contract.Requires(f.IsFuelAware());

       Contract.Requires(sink != null && predef != null);

       // axiom  // layer synonym axiom

       //   (forall s, $Heap, formals ::

@@ -2400,7 +2418,7 @@ namespace Microsoft.Dafny {
       var coArgs = new List<Bpl.Expr>(tyexprs);

       var prefixArgs = new List<Bpl.Expr>(tyexprs);

       var prefixArgsLimited = new List<Bpl.Expr>(tyexprs);

-      if (pp.IsRecursive) {

+      if (pp.IsFuelAware()) {

         var sV = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$ly", predef.LayerType));

         var s = new Bpl.IdentifierExpr(tok, sV);

         var succS = FunctionCall(tok, BuiltinFunction.LayerSucc, null, s);

@@ -3073,13 +3091,13 @@ namespace Microsoft.Dafny {
         Bpl.FunctionCall funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));

         List<Bpl.Expr> argsC = new List<Bpl.Expr>();

         List<Bpl.Expr> argsT = new List<Bpl.Expr>();

-        if (f.IsRecursive)

+        if (f.IsFuelAware())

         {

-            argsC.Add(etran.LayerN(1));

+            argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));

         }

-        if (f.OverriddenFunction.IsRecursive)

+        if (f.OverriddenFunction.IsFuelAware())

         {

-            argsT.Add(etran.LayerN(1));

+          argsT.Add(etran.layerInterCluster.GetFunctionFuel(f));

         }

         argsC.Add(etran.HeapExpr);

         argsT.Add(etran.HeapExpr);

@@ -3726,7 +3744,7 @@ namespace Microsoft.Dafny {
         var typeParams = TrTypeParamDecls(f.TypeArgs);

         {

           var formals = new List<Variable>();

-          if (f.IsRecursive) {

+          if (f.IsFuelAware()) {

             formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType), true));

           }

           if (!f.IsStatic) {

@@ -3750,7 +3768,7 @@ namespace Microsoft.Dafny {
         List<Bpl.Expr> argsF = new List<Bpl.Expr>();

         List<Bpl.Expr> argsFFrame = new List<Bpl.Expr>();

         List<Bpl.Expr> argsCanCall = new List<Bpl.Expr>();

-        if (f.IsRecursive) {

+        if (f.IsFuelAware()) {

           var sV = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));

           var s = new Bpl.IdentifierExpr(f.tok, sV);

           bvars.Add(sV);

@@ -3795,7 +3813,7 @@ namespace Microsoft.Dafny {
         sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax));

       } else {

 #else

-        // This is the general case

+      // This is the general case

         Bpl.Expr h0; var h0Var = BplBoundVar("$h0", predef.HeapType, out h0);

         Bpl.Expr h1; var h1Var = BplBoundVar("$h1", predef.HeapType, out h1);

 

@@ -3825,7 +3843,7 @@ namespace Microsoft.Dafny {
         var f1args = new List<Bpl.Expr>(tyexprs);

         var f0argsCanCall = new List<Bpl.Expr>(tyexprs);

         var f1argsCanCall = new List<Bpl.Expr>(tyexprs);

-        if (f.IsRecursive) {

+        if (f.IsFuelAware()) {

           Bpl.Expr s; var sV = BplBoundVar("$ly", predef.LayerType, out s);

           bvars.Add(sV);

           f0args.Add(s); f1args.Add(s);  // but don't add to f0argsCanCall or f1argsCanCall

@@ -4066,8 +4084,8 @@ namespace Microsoft.Dafny {
         foreach (var p in GetTypeParams(f)) {

           args.Add(trTypeParam(p, null));

         }

-        if (f.IsRecursive) {

-          args.Add(etran.LayerN(1));

+        if (f.IsFuelAware()) {

+          args.Add(etran.layerInterCluster.GetFunctionFuel(f));

         }

         args.Add(etran.HeapExpr);

         if (!f.IsStatic) {

@@ -4100,8 +4118,8 @@ namespace Microsoft.Dafny {
         foreach (var p in GetTypeParams(f)) {

           args.Add(trTypeParam(p, null));

         }

-        if (f.IsRecursive) {

-          args.Add(etran.LayerN(1));

+        if (f.IsFuelAware()) {

+          args.Add(etran.layerInterCluster.GetFunctionFuel(f));

         }

         args.Add(etran.HeapExpr);

         foreach (Variable p in implInParams) {

@@ -5572,7 +5590,7 @@ namespace Microsoft.Dafny {
           tyargs.Add(TypeToTy(fm.Type));

         }

         tyargs.Add(TypeToTy(f.ResultType));

-        if (f.IsRecursive) {

+        if (f.IsFuelAware()) {

           Bpl.Expr ly; vars.Add(BplBoundVar("$ly", predef.LayerType, out ly)); args.Add(ly);

           formals.Add(BplFormalVar(null, predef.LayerType, true));

         }

@@ -6135,7 +6153,7 @@ namespace Microsoft.Dafny {
         var typeParams = TrTypeParamDecls(f.TypeArgs);

         var formals = new List<Variable>();

         formals.AddRange(MkTyParamFormals(GetTypeParams(f)));

-        if (f.IsRecursive) {

+        if (f.IsFuelAware()) {

           formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType), true));

         }

         formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", predef.HeapType), true));

@@ -6212,7 +6230,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(predef != null);

       Contract.Requires(currentModule == null && codeContext == null);

       Contract.Ensures(currentModule == null && codeContext == null);

-      Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);

+      Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);      

 

       currentModule = m.EnclosingClass.Module;

       codeContext = m;

@@ -6495,7 +6513,7 @@ namespace Microsoft.Dafny {
       // parameters of the procedure

       List<Variable> inParams = new List<Variable>();

       Bpl.Formal layer;

-      if (f.IsRecursive) {

+      if (f.IsFuelAware()) {

         layer = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType), true);

         inParams.Add(layer);

       } else {

@@ -7018,9 +7036,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

       Contract.Requires(codeContext != null && predef != null);

+      Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));

       if (stmt is PredicateStmt) {

+        this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);

         if (stmt is AssertStmt || DafnyOptions.O.DisallowSoundnessCheating) {

-          AddComment(builder, stmt, "assert statement");

+          AddComment(builder, stmt, "assert statement");          

           PredicateStmt s = (PredicateStmt)stmt;

           TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

           IToken enclosingToken = null;

@@ -7040,13 +7060,14 @@ namespace Microsoft.Dafny {
               }

             }

             builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

-          }

+          }          

         } else if (stmt is AssumeStmt) {

           AddComment(builder, stmt, "assume statement");

           AssumeStmt s = (AssumeStmt)stmt;

           TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

           builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr), etran.TrAttributes(stmt.Attributes, null)));

         }

+        this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is PrintStmt) {

         AddComment(builder, stmt, "print statement");

         PrintStmt s = (PrintStmt)stmt;

@@ -7279,6 +7300,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is WhileStmt) {

         AddComment(builder, stmt, "while statement");

+        this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);

         var s = (WhileStmt)stmt;

         BodyTranslator bodyTr = null;

         if (s.Body != null) {

@@ -7289,7 +7311,7 @@ namespace Microsoft.Dafny {
           };

         }

         TrLoop(s, s.Guard, bodyTr, builder, locals, etran);

-

+        this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is AlternativeLoopStmt) {

         AddComment(builder, stmt, "alternative loop statement");

         var s = (AlternativeLoopStmt)stmt;

@@ -7331,6 +7353,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is ForallStmt) {

         var s = (ForallStmt)stmt;

+        this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);

         if (s.Kind == ForallStmt.ParBodyKind.Assign) {

           AddComment(builder, stmt, "forall statement (assign)");

           Contract.Assert(s.Ens.Count == 0);

@@ -7374,7 +7397,7 @@ namespace Microsoft.Dafny {
         } else {

           Contract.Assert(false);  // unexpected kind

         }

-

+        this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is CalcStmt) {

         /* Translate into:

         if (*) {

@@ -7397,9 +7420,10 @@ namespace Microsoft.Dafny {
         }

         assume line<0> op line<n>;

         */

-        var s = (CalcStmt)stmt;

+        var s = (CalcStmt)stmt;        

         Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver

         AddComment(builder, stmt, "calc statement");

+        this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);

         CurrentIdGenerator.Push();  // put the entire calc statement within its own sub-branch

         if (s.Lines.Count > 0) {

           Bpl.IfCmd ifCmd = null;

@@ -7464,7 +7488,7 @@ namespace Microsoft.Dafny {
           }

         }

         CurrentIdGenerator.Pop();

-

+        this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);

@@ -10262,6 +10286,227 @@ namespace Microsoft.Dafny {
       }

     }

 

+    internal class FuelSettingPair 

+    {

+      public int low;

+      public int high;

+

+      public FuelSettingPair(int low = (int)FuelSetting.FuelAmount.LOW, int high = (int)FuelSetting.FuelAmount.HIGH) {

+        this.low = low;

+        this.high = high;

+      }

+    }

+

+    // C#'s version of a type alias

+    internal class FuelContext : Dictionary<Function, FuelSettingPair> { }

+

+    internal class FuelSetting

+    {

+      public enum FuelAmount { NONE, LOW, HIGH };

+      public static Stack<FuelContext> SavedContexts = new Stack<FuelContext>();

+

+      private static FuelSettingPair FuelAttrib(Function f) {

+        Contract.Requires(f != null);

+        Contract.Ensures(Contract.Result<FuelSettingPair>() != null);

+        FuelSettingPair setting = new FuelSettingPair();

+

+        if (f.Attributes != null) {

+          List<Expression> args = Attributes.FindExpressions(f.Attributes, "fuel");

+          if (args != null && args.Count >= 2) {

+            LiteralExpr literalLow = args[0] as LiteralExpr;

+            LiteralExpr literalHigh = args[1] as LiteralExpr;

+

+            if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) {

+              setting.low = (int)((BigInteger)literalLow.Value);

+              setting.high = (int)((BigInteger)literalHigh.Value);

+            }

+          } else if (args != null && args.Count >= 1) {

+            LiteralExpr literal = args[0] as LiteralExpr;

+            if (literal != null && literal.Value is BigInteger) {

+              setting.low = (int)((BigInteger)literal.Value);

+              setting.high = setting.low + 1;

+            }

+          }

+        }

+

+        return setting;

+      }

+

+      public int amount;        // Amount of fuel above that represented by start

+      private Bpl.Expr start;   // Starting fuel argument (null indicates LZ)      

+      private Translator translator;

+

+      public FuelSetting(Translator translator, int amount, Bpl.Expr start = null) {

+        this.translator = translator;

+        this.amount = amount;

+        this.start = start;

+      }

+

+      public FuelSetting Offset(int offset) {

+        return new FuelSetting(translator, this.amount + offset, start);

+      }

+

+      public Bpl.Expr LayerZero() {

+        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+        return new Bpl.IdentifierExpr(Token.NoToken, "$LZ", translator.predef.LayerType);

+      }

+

+      public Bpl.Expr LayerN(int n) {

+        Contract.Requires(0 <= n);

+        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+        return translator.LayerSucc(LayerZero(), n);

+      }

+

+      private Bpl.Expr ToExpr(int amount) {

+        if (start == null) {

+          return LayerN(amount);

+        } else {

+          return translator.LayerSucc(start, amount);

+        }

+      }

+

+      public Bpl.Expr ToExpr() {

+        return this.ToExpr(this.amount);

+      }

+

+      /// <summary>

+      /// Get the fuel value for this function, given the ambient environment (represented by the fuel setting)

+      /// the function itself, and the function call's context (if any)

+      /// </summary>      

+      public Bpl.Expr GetFunctionFuel(Function f) {

+        Contract.Requires(f != null);

+        if (this.amount == (int)FuelAmount.NONE) {

+          return this.ToExpr();

+        } else {

+          FuelSettingPair setting = null;

+          var found = translator.fuelContext.TryGetValue(f, out setting);

+

+          if (!found) {  // If the context doesn't define fuel for this function, check for a fuel attribute (which supplies a default value if none is found)

+            setting = FuelAttrib(f);

+          }

+

+          if (this.amount == (int)FuelAmount.LOW) {

+            return ToExpr(setting.low);

+          } else if (this.amount == (int)FuelAmount.HIGH) {

+            return ToExpr(setting.high);

+          } else {

+            Contract.Assert(false); // Should not reach here

+            return null;

+          }

+        }

+      }

+

+

+      /// <summary>

+      /// Finds all fuel related attributes of the form {:fuel function low [high]}

+      /// Adds the setting to the context _if_ the context does not already have a setting for that function.

+      /// In other words, it should be called in order from most to least specific contenxt scope.

+      /// </summary>    

+      private static void FindFuelAttributes(Attributes attribs, FuelContext fuelContext) {

+        Function f = null;

+        FuelSettingPair setting = null;

+

+        if (attribs != null) {

+          List<List<Expression>> results = Attributes.FindAllExpressions(attribs, "fuel");

+

+          if (results != null) {

+            foreach (List<Expression> args in results) {

+              if (args != null && args.Count >= 2) {

+                // Try to extract the function from the first argument

+                MemberSelectExpr selectExpr = args[0].Resolved as MemberSelectExpr;

+                if (selectExpr != null) {

+                  f = selectExpr.Member as Function;

+                }

+

+                // Try to extract the lower fuel setting

+                LiteralExpr literalLow = args[1] as LiteralExpr;

+                if (literalLow != null && literalLow.Value is BigInteger) {

+                  setting = new FuelSettingPair();

+                  setting.low = (int)((BigInteger)literalLow.Value);

+                }

+

+                // The user may supply an additional high argument; if not, it defaults to low + 1

+                if (f != null && args.Count >= 3) {

+                  LiteralExpr literalHigh = args[2] as LiteralExpr;

+                  if (setting != null && literalHigh != null && literalHigh.Value is BigInteger) {

+                    setting.high = (int)((BigInteger)literalHigh.Value);

+                    if (!fuelContext.ContainsKey(f)) {

+                      fuelContext.Add(f, setting);

+                    }

+                  }

+                } else if (f != null && setting != null) {

+                  setting.high = setting.low + 1;

+                  if (!fuelContext.ContainsKey(f)) {

+                    fuelContext.Add(f, setting);

+                  }

+                }

+              }

+            }

+          }

+        }

+      }

+

+      /// <summary>

+      /// Extend the given context with fuel information from the declaration itself, and enclosing modules

+      /// </summary>

+      private static void AddFuelContext(FuelContext context, TopLevelDecl decl) {

+        FindFuelAttributes(decl.Attributes, context);

+

+        var module = decl.Module;

+        while (module != null) {

+          FindFuelAttributes(module.Attributes, context);

+          module = module.Module;

+        }

+      }

+

+      /// <summary>

+      /// Creates a summary of all fuel settings in scope, starting from the given class declaration

+      /// </summary>      

+      public static FuelContext NewFuelContext(TopLevelDecl decl) {

+        FuelContext context = new FuelContext();

+        AddFuelContext(context, decl);

+        return context;

+      }

+

+      /// <summary>

+      /// Creates a summary of all fuel settings in scope, starting from the given member declaration      

+      /// </summary>      

+      public static FuelContext NewFuelContext(MemberDecl decl) {

+        FuelContext context = new FuelContext();

+

+        FindFuelAttributes(decl.Attributes, context);

+        AddFuelContext(context, decl.EnclosingClass);

+        

+        return context;

+      }

+

+      /// <summary>

+      /// Extends the given fuel context with any new fuel settings found in attribs

+      /// </summary>    

+      public static FuelContext ExpandFuelContext(Attributes attribs, FuelContext oldFuelContext) {

+        Contract.Ensures(SavedContexts.Count == Contract.OldValue(SavedContexts.Count) + 1);

+        FuelContext newContext = new FuelContext();

+        FindFuelAttributes(attribs, newContext);

+        if (newContext.Count > 0) {

+          foreach (var pair in oldFuelContext) {

+            if (!newContext.ContainsKey(pair.Key)) {    // Local setting takes precedence over old context

+              newContext.Add(pair.Key, pair.Value);              

+            }

+          }          

+        } else {

+          newContext = oldFuelContext;

+        }

+        SavedContexts.Push(oldFuelContext);

+        return newContext;

+      }

+

+      public static FuelContext PopFuelContext() {

+        Contract.Requires(SavedContexts.Count > 0);

+        return SavedContexts.Pop();

+      }

+

+    }

+

     internal class ExpressionTranslator

     {

       public readonly Bpl.Expr HeapExpr;

@@ -10270,8 +10515,8 @@ namespace Microsoft.Dafny {
       public readonly string This;

       public readonly string modifiesFrame; // the name of the context's frame variable.

       readonly Function applyLimited_CurrentFunction;

-      public readonly Bpl.Expr layerInterCluster;

-      public readonly Bpl.Expr layerIntraCluster = null;  // a value of null says to do the same as for inter-cluster calls

+      public readonly FuelSetting layerInterCluster;

+      public readonly FuelSetting layerIntraCluster = null;  // a value of null says to do the same as for inter-cluster calls

       public int Statistics_CustomLayerFunctionCount = 0;

       public readonly bool ProducingCoCertificates = false;

       [ContractInvariantMethod]

@@ -10288,40 +10533,16 @@ namespace Microsoft.Dafny {
       }

 

       /// <summary>

-      /// This is a general constructor, but takes the layerInterCluster as an int.

-      /// </summary>

-      ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,

-        Function applyLimited_CurrentFunction, int layerInterCluster, Bpl.Expr layerIntraCluster, string modifiesFrame) {

-

-        Contract.Requires(translator != null);

-        Contract.Requires(predef != null);

-        Contract.Requires(heap != null);

-        Contract.Requires(thisVar != null);

-        Contract.Requires(0 <= layerInterCluster);

-        Contract.Requires(modifiesFrame != null);

-

-        this.translator = translator;

-        this.predef = predef;

-        this.HeapExpr = heap;

-        this.This = thisVar;

-        this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

-        this.layerInterCluster = LayerN(layerInterCluster);

-        this.layerIntraCluster = layerIntraCluster;

-        this.modifiesFrame = modifiesFrame;

-      }

-

-      /// <summary>

       /// This is the most general constructor.  It is private and takes all the parameters.  Whenever

       /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in.

       /// </summary>

       ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,

-        Function applyLimited_CurrentFunction, Bpl.Expr layerInterCluster, Bpl.Expr layerIntraCluster, string modifiesFrame) {

+        Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string modifiesFrame) {

 

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

         Contract.Requires(heap != null);

-        Contract.Requires(thisVar != null);

-        Contract.Requires(layerInterCluster != null);

+        Contract.Requires(thisVar != null);       

         Contract.Requires(modifiesFrame != null);

 

         this.translator = translator;

@@ -10329,7 +10550,7 @@ namespace Microsoft.Dafny {
         this.HeapExpr = heap;

         this.This = thisVar;

         this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

-        this.layerInterCluster = layerInterCluster;

+        this.layerInterCluster = layerInterCluster;        

         if (layerIntraCluster == null) {

           this.layerIntraCluster = layerInterCluster;

         } else {

@@ -10365,7 +10586,7 @@ namespace Microsoft.Dafny {
       }

 

       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar)

-        : this(translator, predef, heap, thisVar, null, 1, null, "$_Frame") {

+        : this(translator, predef, heap, thisVar, null, new FuelSetting(translator, 1), null, "$_Frame") {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

         Contract.Requires(heap != null);

@@ -10409,7 +10630,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(layerArgument != null);

         Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);

 

-        return new ExpressionTranslator(translator, predef, HeapExpr, This, null, layerArgument, layerArgument, modifiesFrame);

+        return new ExpressionTranslator(translator, predef, HeapExpr, This, null, new FuelSetting(translator, 0, layerArgument), new FuelSetting(translator, 0, layerArgument), modifiesFrame);

       }

 

       public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction, Bpl.Expr layerArgument) {

@@ -10417,16 +10638,16 @@ namespace Microsoft.Dafny {
         Contract.Requires(layerArgument != null);

         Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);

 

-        return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, /* layerArgument */ layerInterCluster, layerArgument, modifiesFrame);

+        return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, /* layerArgument */ layerInterCluster, new FuelSetting(translator, 0, layerArgument), modifiesFrame);

       }

 

       public ExpressionTranslator LayerOffset(int offset) {

         Contract.Requires(0 <= offset);

         Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);

 

-        var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, translator.LayerSucc(layerInterCluster, offset), layerIntraCluster, modifiesFrame);

+        var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.Offset(offset), layerIntraCluster, modifiesFrame);

         if (this.oldEtran != null) {

-          var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, translator.LayerSucc(layerInterCluster, offset), layerIntraCluster, modifiesFrame);

+          var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.Offset(offset), layerIntraCluster, modifiesFrame);

           etOld.oldEtran = etOld;

           et.oldEtran = etOld;

         }

@@ -10465,17 +10686,6 @@ namespace Microsoft.Dafny {
         }

       }

 

-      public Bpl.Expr LayerZero() {

-        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

-        return new Bpl.IdentifierExpr(Token.NoToken, "$LZ", predef.LayerType);

-      }

-

-      public Bpl.Expr LayerN(int n) {

-        Contract.Requires(0 <= n);

-        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

-        return translator.LayerSucc(LayerZero(), n);

-      }

-

       public Bpl.IdentifierExpr ModuleContextHeight() {

         Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);

         return new Bpl.IdentifierExpr(Token.NoToken, "$ModuleContextHeight", Bpl.Type.Int);

@@ -10649,8 +10859,8 @@ namespace Microsoft.Dafny {
             },

             fn => {

               var args = e.TypeApplication.ConvertAll(translator.TypeToTy);

-              if (fn.IsRecursive) {

-                args.Add(layerInterCluster);

+              if (fn.IsFuelAware()) {

+                args.Add(this.layerInterCluster.GetFunctionFuel(fn));

               }

               if (!fn.IsStatic) {

                 args.Add(/* translator.BoxIfUnboxed */(TrExpr(e.Obj)/*, e.Type */));

@@ -10806,15 +11016,15 @@ namespace Microsoft.Dafny {
         } else if (expr is FunctionCallExpr) {

           FunctionCallExpr e = (FunctionCallExpr)expr;

           Bpl.Expr layerArgument;

-          if (e.Function.IsRecursive) {

+          if (e.Function.IsFuelAware()) {

             Statistics_CustomLayerFunctionCount++;

             ModuleDefinition module = e.Function.EnclosingClass.Module;

             if (this.applyLimited_CurrentFunction != null &&

               this.layerIntraCluster != null &&

               ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) {

-              layerArgument = this.layerIntraCluster;

+              layerArgument = this.layerIntraCluster.GetFunctionFuel(e.Function);

             } else {

-              layerArgument = this.layerInterCluster;

+              layerArgument = this.layerInterCluster.GetFunctionFuel(e.Function);

             }

           } else {

             layerArgument = null;

@@ -10992,7 +11202,7 @@ namespace Microsoft.Dafny {
               if (cot != null) {

                 var e0args = e.E0.Type.NormalizeExpand().TypeArgs;

                 var e1args = e.E1.Type.NormalizeExpand().TypeArgs;

-                return translator.CoEqualCall(cot, e0args, e1args, null, LayerN(2), e0, e1, expr.tok);

+                return translator.CoEqualCall(cot, e0args, e1args, null, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, expr.tok);

               }

               typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Eq; break;

@@ -11001,7 +11211,7 @@ namespace Microsoft.Dafny {
               if (cotx != null) {

                 var e0args = e.E0.Type.NormalizeExpand().TypeArgs;

                 var e1args = e.E1.Type.NormalizeExpand().TypeArgs;

-                var x = translator.CoEqualCall(cotx, e0args, e1args, null, LayerN(2), e0, e1, expr.tok);

+                var x = translator.CoEqualCall(cotx, e0args, e1args, null, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, expr.tok);

                 return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, x);

               }

               typ = Bpl.Type.Bool;

@@ -11282,7 +11492,7 @@ namespace Microsoft.Dafny {
               var e2type = e.E2.Type.NormalizeExpand();

               var cot = e1type.AsCoDatatype;

               Contract.Assert(cot != null);  // the argument types of prefix equality (and prefix disequality) are codatatypes

-              var r = translator.CoEqualCall(cot, e1type.TypeArgs, e2type.TypeArgs, e0, LayerN(2), e1, e2);

+              var r = translator.CoEqualCall(cot, e1type.TypeArgs, e2type.TypeArgs, e0, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e1, e2);

               if (e.Op == TernaryExpr.Opcode.PrefixEqOp) {

                 return r;

               } else {

@@ -11315,8 +11525,7 @@ namespace Microsoft.Dafny {
           if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) {

             // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body

             var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars);

-            Expr layer = translator.LayerSucc(ly);

-            bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layer, layer, modifiesFrame);

+            bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame);

           }

           if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) {

             var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars);

@@ -11489,7 +11698,7 @@ namespace Microsoft.Dafny {
                 new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, ebody),

                 new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, reqbody),

                 new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, rdbody))),

-            layerIntraCluster ?? layerInterCluster),

+                layerIntraCluster != null ? layerIntraCluster.ToExpr() : layerInterCluster.ToExpr()),

           predef.HandleType);

       }

 

@@ -12582,15 +12791,14 @@ namespace Microsoft.Dafny {
           //   checked $PrefixEqual#Dt(k, A, B) || (0 < k ==> A.Cons? ==> B.Cons? && A.head == B.head && $PrefixEqual#2#Dt(k - 1, A.tail, B.tail))  // note the #2 in the recursive call, just like for user-defined predicates that are inlined by TrSplitExpr

           //   free $PrefixEqual#Dt(k, A, B);

           var kPos = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);

-          var prefixEqK = CoEqualCall(codecl, e1type.TypeArgs, e2type.TypeArgs, k, etran.LayerN(2), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B);

+          var prefixEqK = CoEqualCall(codecl, e1type.TypeArgs, e2type.TypeArgs, k, etran.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B);

           var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));

           // for the inlining of the definition of prefix equality, translate the two main equality operands arguments with a higher offset (to obtain #2 functions)

           var etran2 = etran.LayerOffset(1);

           var A2 = etran2.TrExpr(e.E1);

           var B2 = etran2.TrExpr(e.E2);

           var needsTokenAdjust = TrSplitNeedsTokenAdjustment(expr);

-          // Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+

-          Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2);

+          Bpl.Expr layer = etran.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH);

           foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e1type.TypeArgs, e2type.TypeArgs, kMinusOne, layer, A2, B2, true)) {

             var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kPos, c));

             splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));

@@ -13944,7 +14152,7 @@ namespace Microsoft.Dafny {
           r = rr;

         } else if (stmt is CalcStmt) {

           var s = (CalcStmt)stmt;

-          var rr = new CalcStmt(s.Tok, s.EndTok, SubstCalcOp(s.Op), s.Lines.ConvertAll(Substitute), s.Hints.ConvertAll(SubstBlockStmt), s.StepOps.ConvertAll(SubstCalcOp), SubstCalcOp(s.ResultOp));

+          var rr = new CalcStmt(s.Tok, s.EndTok, SubstCalcOp(s.Op), s.Lines.ConvertAll(Substitute), s.Hints.ConvertAll(SubstBlockStmt), s.StepOps.ConvertAll(SubstCalcOp), SubstCalcOp(s.ResultOp), SubstAttributes(s.Attributes));

           rr.Steps.AddRange(s.Steps.ConvertAll(Substitute));

           rr.Result = Substitute(s.Result);

           r = rr;

diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy
new file mode 100644
index 00000000..c8a1fc2f
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy
@@ -0,0 +1,423 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+module TestModule1 {

+    function pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    method test(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos(z) == 0;

+        assert pos(-1) == 0;

+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel

+        assert pos(y) == 4 + pos(y - 4);    // Succeeds, thanks to the assume from the preceding assert

+    }

+}

+

+// Test with function-level fuel boost

+module TestModule2 {

+    function {:fuel 3} pos1(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos1(x - 1)

+    }

+

+    function {:fuel 3,5} pos2(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos2(x - 1)

+    }

+

+    function {:fuel 3,5} pos3(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos3(x - 1)

+    }

+

+    function {:opaque} {:fuel 3,5} pos4(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos3(x - 1)

+    }

+

+    method test(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos1(z) == 0;

+        assert pos1(-1) == 0;

+        assert pos1(y) == 3 + pos1(y - 3);

+        assert pos1(y) == 4 + pos1(y - 4);

+

+        assert pos2(z) == 0;

+        assert pos2(-1) == 0;

+        assert pos2(y) == 3 + pos2(y - 3);

+        assert pos2(y) == 4 + pos2(y - 4);

+

+        if (*) {

+            assert pos3(y) == 5 + pos3(y - 5);  // Just enough fuel to get here

+        } else {

+            assert pos3(y) == 6 + pos3(y - 6);  // error: Should fail even with a boost, since boost is too small

+        }

+

+        if (*) {

+            assert pos4(z) == 0;    // error: Fuel shouldn't overcome opaque

+        } else {

+            reveal_pos4();

+            assert pos4(y) == 5 + pos4(y - 5);  // With reveal, everything should work as above

+        }

+

+

+    }

+}

+

+

+module TestModule3 {

+    // This fuel setting is equivalent to opaque, except for literals

+    function {:fuel 0,0} pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    method test(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos(z) == 0;             // error: Opaque setting hides body

+        assert pos(-1) == 0;            // Passes, since Dafny's computation mode for lits ignore fuel

+        assert pos(y) == 3 + pos(y - 3);// error: Opaque setting hides body

+    }

+}

+

+// Test fuel settings via different contexts

+module TestModule4 {

+    function pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    // Should pass

+    method {:fuel pos,3,5} test1(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos(z) == 0;

+        assert pos(-1) == 0;

+        assert pos(y) == 3 + pos(y - 3);

+    }

+

+    method {:fuel pos,0,0} test2(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos(z) == 0;               // error: Should fail due to "opaque" fuel setting

+        assert pos(-1) == 0;

+        assert pos(y) == 3 + pos(y - 3);  // error: Should fail due to "opaque" fuel setting

+    }

+

+    method test3(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert {:fuel pos,0,0} pos(z) == 0;               // error: Should fail due to "opaque" fuel setting

+        assert pos(-1) == 0;

+        if (*) {

+            assert pos(y) == 3 + pos(y - 3);  // error: Should fail without extra fuel setting

+            assert pos(y) == 6 + pos(y - 6);  // error: Should fail even with previous assert turned into assume

+        } else {

+            assert {:fuel pos,3,5} pos(y) == 3 + pos(y - 3);  // Should succeed with extra fuel setting

+            assert pos(y) == 6 + pos(y - 6);  // Should succeed thanks to previous assert turned into assume

+        } 

+    }

+

+    method test4(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        forall t:int {:fuel pos,3} | t > 0 

+            ensures true;

+        {

+            assert pos(y) == 3 + pos(y - 3);    // Expected to pass, due to local fuel boost

+        }

+

+        if (*) {

+            calc {:fuel pos,3} {

+                pos(y);

+                3 + pos(y - 3);

+            }

+        }

+

+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel outside the forall

+    }

+}

+

+// Test fuel settings via different module contexts

+module TestModule5 {

+    // Test module level fuel settings, with nested modules

+

+    module TestModule5a {

+        module {:fuel TestModule5aiA.pos,3} TestModule5ai {

+            module TestModule5aiA {

+                function pos(x:int) : int 

+                {

+                    if x < 0 then 0

+                    else 1 + pos(x - 1)

+                }

+

+                method test(y:int, z:int) 

+                    requires y > 5;

+                    requires z < 0;

+                {

+                    assert pos(z) == 0;

+                    assert pos(-1) == 0;

+                    assert pos(y) == 3 + pos(y - 3);    // Should pass due to intermediate module's fuel setting

+                }

+            }

+

+            method test(y:int, z:int) 

+                requires y > 5;

+                requires z < 0;

+            {

+                assert TestModule5aiA.pos(z) == 0;

+                assert TestModule5aiA.pos(-1) == 0;

+                assert TestModule5aiA.pos(y) == 3 + TestModule5aiA.pos(y - 3);    // Should pass due to module level fuel

+            }

+        }

+  

+        method test(y:int, z:int) 

+            requires y > 5;

+            requires z < 0;

+        {

+            assert TestModule5ai.TestModule5aiA.pos(z) == 0;

+            assert TestModule5ai.TestModule5aiA.pos(-1) == 0;

+            assert TestModule5ai.TestModule5aiA.pos(y) == 3 + TestModule5ai.TestModule5aiA.pos(y - 3);    // error: Should fail, due to lack of fuel

+        }

+    }

+

+    module {:fuel TestModule5bi.TestModule5biA.pos,3} TestModule5b {

+        module  TestModule5bi {

+            module TestModule5biA {

+                function pos(x:int) : int 

+                {

+                    if x < 0 then 0

+                    else 1 + pos(x - 1)

+                }

+

+                method test(y:int, z:int) 

+                    requires y > 5;

+                    requires z < 0;

+                {

+                    assert pos(z) == 0;

+                    assert pos(-1) == 0;

+                    assert pos(y) == 3 + pos(y - 3);    // Should succceed due to outer module fuel setting

+                }

+            }

+        }

+    }

+}

+

+// Test fuel setting for multiple functions

+module TestModule6 {

+    function pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    function neg(x:int) : int

+        decreases 1 - x;

+    {

+        if x > 0 then 0

+        else 1 + neg(x + 1)

+    }

+

+    method test1(y:int, z:int) 

+        requires y > 5;

+        requires z < 5;

+    {

+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel

+

+        assert neg(z) == 3 + neg(z + 3);    // error: Should fail, due to lack of fuel

+    }

+

+    method {:fuel pos,3} {:fuel neg,4} test2(y:int, z:int) 

+        requires y > 5;

+        requires z < -5;

+    {

+        assert pos(y) == 3 + pos(y - 3);    

+

+        assert neg(z) == 3 + neg(z + 3);    

+    }

+}

+

+// Test fuel settings with multiple overlapping contexts

+module TestModule7 {

+    function {:fuel 3} pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    function {:fuel 0,0} neg(x:int) : int

+        decreases 1 - x;

+    {

+        if x > 0 then 0

+        else 1 + neg(x + 1)

+    }

+

+    method {:fuel neg,4} {:fuel pos,0,0} test1(y:int, z:int) 

+        requires y > 5;

+        requires z < -5;

+    {

+        if (*) {

+            assert pos(y) == 3 + pos(y - 3);    // error: Method fuel should override function fuel, so this should fail

+            assert neg(z) == 3 + neg(z + 3);    // Method fuel should override function fuel, so this succeeds

+        }

+

+        forall t:int {:fuel pos,3} | t > 0 

+            ensures true;

+        {

+            assert pos(y) == 3 + pos(y - 3);    // Statement fuel should override method fuel, so this should succeed

+        }

+    }

+}

+

+// Test fuel in a slightly more complicated setting

+module TestModule8 {

+

+    newtype byte = i:int | 0 <= i < 0x100

+    newtype uint64 = i:int | 0 <= i < 0x10000000000000000

+

+    datatype G = GUint64

+               | GArray(elt:G)

+               | GTuple(t:seq<G>)

+               | GByteArray

+               | GTaggedUnion(cases:seq<G>)

+

+        datatype V = VUint64(u:uint64)

+                   | VTuple(t:seq<V>)

+                   | VCase(c:uint64, val:V)

+

+        predicate {:fuel 2} ValInGrammar(val:V, grammar:G)

+        {

+            match val

+                case VUint64(_) => grammar.GUint64?

+                case VTuple(t)  => grammar.GTuple? && |t| == |grammar.t|

+                                      && forall i :: 0 <= i < |t| ==> ValInGrammar(t[i], grammar.t[i])

+                case VCase(c, val) => grammar.GTaggedUnion? && int(c) < |grammar.cases| && ValInGrammar(val, grammar.cases[c])

+        }

+

+        datatype CRequest = CRequest(client:EndPoint, seqno:uint64, request:CAppMessage) | CRequestNoOp()

+

+        type EndPoint

+        function method EndPoint_grammar() : G { GUint64 }

+        function method CRequest_grammar() : G { GTaggedUnion([ GTuple([EndPoint_grammar(), GUint64, CAppMessage_grammar()]), GUint64]) }

+

+        function method parse_EndPoint(val:V) : EndPoint

+            requires ValInGrammar(val, EndPoint_grammar());

+

+        type CAppMessage

+        function method CAppMessage_grammar() : G { GTaggedUnion([GUint64, GUint64, GUint64]) }

+        function method parse_AppMessage(val:V) : CAppMessage

+            requires ValInGrammar(val, CAppMessage_grammar());

+

+        function method {:fuel ValInGrammar,1,2} parse_Request1(val:V) : CRequest

+            requires ValInGrammar(val, CRequest_grammar());

+        {

+            if val.c == 0 then

+                var ep := parse_EndPoint(val.val.t[0]); // With default fuel, error: function precondition, destructor, index

+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]))    // error: index out of range, destructor

+            else 

+                CRequestNoOp()

+        }

+

+        function method parse_Request2(val:V) : CRequest

+            requires ValInGrammar(val, CRequest_grammar());

+        {

+            if val.c == 0 then

+                var ep := parse_EndPoint(val.val.t[0]);                      // With fuel boosted to 2 this succeeds

+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2])) // error: destructor

+            else 

+                CRequestNoOp()

+        }

+

+        function method {:fuel ValInGrammar,3} parse_Request3(val:V) : CRequest

+            requires ValInGrammar(val, CRequest_grammar());

+        {

+            if val.c == 0 then

+                var ep := parse_EndPoint(val.val.t[0]); 

+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]))    // With one more boost, everything succeeds

+            else 

+                CRequestNoOp()

+        }

+

+        // With the method, everything succeeds with one less fuel boost (i.e., 2, rather than 3, as in parse_Request3)

+        method parse_Request4(val:V) returns (req:CRequest)     

+            requires ValInGrammar(val, CRequest_grammar());

+        {

+            if val.c == 0 {

+                var ep := parse_EndPoint(val.val.t[0]);

+                req := CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]));

+            } else {

+                req := CRequestNoOp();

+            }

+        }

+}

+

+

+// Test fuel when it's applied to a non-recursive function

+module TestModule9 {

+    function abs(x:int) : int

+    {

+        if x < 0 then -1 * x else x

+    }

+

+    // All should pass.

+    method test1(y:int, z:int)

+        requires y > 5;

+        requires z < 0;

+    {

+        assert abs(z) == -1*z;

+        assert abs(y) == y;

+        assert abs(-1) == 1;

+    }

+

+    // Method-level fuel override

+    method {:fuel abs,0,0} test2(y:int, z:int)

+        requires y > 5;

+        requires z < 0;

+    {

+        assert abs(z) == -1*z;  // error: Cannot see the body of abs

+        assert abs(y) == y;     // error: Cannot see the body of abs

+        assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed

+    }

+

+    // Statement-level fuel override

+    method test3(y:int, z:int)

+        requires y > 5;

+        requires z < 0;

+    {

+        assert {:fuel abs,0,0} abs(z) == -1*z;  // error: Cannot see the body of abs

+        assert abs(y) == y;     // Normal success

+        assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed

+    }

+

+    // Giving more fuel to a non-recursive function won't help,

+    // but it shouldn't hurt either.

+    method {:fuel abs,5,7} test4(y:int, z:int)

+        requires y > 5;

+        requires z < 0;

+    {

+        assert abs(z) == -1*z;

+        assert abs(y) == y;

+        assert abs(-1) == 1;

+    }

+}

+

diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect
new file mode 100644
index 00000000..4c180a9c
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy.expect
@@ -0,0 +1,95 @@
+Fuel.dfy(17,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(65,28): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+Fuel.dfy(69,28): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+    (0,0): anon7_Then

+Fuel.dfy(92,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(94,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(120,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(122,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(129,39): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(132,27): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+Fuel.dfy(133,27): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+Fuel.dfy(157,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Else

+    (0,0): anon9

+Fuel.dfy(200,56): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(245,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(247,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(280,27): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+Fuel.dfy(335,27): Error: possible violation of function precondition

+Fuel.dfy(324,22): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+Fuel.dfy(335,50): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+Fuel.dfy(335,51): Error: index out of range

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+Fuel.dfy(336,39): Error: index out of range

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+Fuel.dfy(336,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+Fuel.dfy(346,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+Fuel.dfy(397,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(398,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Fuel.dfy(407,39): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 51 verified, 24 errors

diff --git a/Test/dafny4/Circ.dfy b/Test/dafny4/Circ.dfy
index e7609195..d110c05c 100644
--- a/Test/dafny4/Circ.dfy
+++ b/Test/dafny4/Circ.dfy
@@ -16,6 +16,7 @@ function zip(a: Stream, b: Stream): Stream { Cons(a.head, zip(b, a.tail)) }
 colemma BlinkZipProperty()

   ensures zip(zeros(), ones()) == blink();

 {

+    BlinkZipProperty();

 }

 

 // ----- Thue-Morse sequence -----

@@ -75,6 +76,7 @@ colemma FProperty(s: Stream<Bit>)
     // def. zip

     Cons(s.head, Cons(not(s).head, zip(s.tail, not(s).tail)));

   }

+  FProperty(s.tail);

 }

 

 // The fix-point theorem now follows easily.