From 8b9126340fb1b5c5c4abe67b940911b675d22c63 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 31 Mar 2016 10:54:30 -0700
Subject: Fix issue 143. The list that stores the function fuel constants was
 declared as static field and not initialized correctly. Make it an instance
 field instead.

---
 Source/Dafny/Translator.cs | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b2b63a07..99571a8c 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -113,7 +113,7 @@ namespace Microsoft.Dafny {
     readonly Dictionary<TopLevelDecl, string>/*!*/ classConstants = new Dictionary<TopLevelDecl, string>();
     readonly Dictionary<int, string> functionConstants = new Dictionary<int, string>();
     readonly Dictionary<Function, string> functionHandles = new Dictionary<Function, string>();
-    readonly static List<FuelConstant> FunctionFuel = new List<FuelConstant>();
+    readonly List<FuelConstant> functionFuel = new List<FuelConstant>();
     readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();
     readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();
     readonly Dictionary<string, Bpl.Constant> fieldConstants = new Dictionary<string,Constant>();
@@ -603,7 +603,7 @@ namespace Microsoft.Dafny {
                   Bpl.Constant startFuelAssert = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuelAssert_" + f.FullName, predef.LayerType), false);
                   sink.AddTopLevelDeclaration(startFuelAssert);
                   Bpl.Expr startFuelAssert_expr = new Bpl.IdentifierExpr(f.tok, startFuelAssert);
-                  Translator.FunctionFuel.Add(new FuelConstant(f, baseFuel_expr, startFuel_expr, startFuelAssert_expr));
+                  this.functionFuel.Add(new FuelConstant(f, baseFuel_expr, startFuel_expr, startFuelAssert_expr));
                 }
               }
             }
@@ -2971,9 +2971,11 @@ namespace Microsoft.Dafny {
     }
 
     void InitializeFuelConstant(IToken tok, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
-      builder.Add(new CommentCmd("initialize fuel constant"));
+      if (this.functionFuel.Count > 0) {
+        builder.Add(new CommentCmd("initialize fuel constant"));
+      }
       FuelContext fuelContext = this.fuelContext;
-      foreach (FuelConstant fuelConstant in Translator.FunctionFuel) {
+      foreach (FuelConstant fuelConstant in this.functionFuel) {
         Function f = fuelConstant.f;
         Bpl.Expr baseFuel = fuelConstant.baseFuel;
         Bpl.Expr startFuel = fuelConstant.startFuel;
@@ -3001,7 +3003,7 @@ namespace Microsoft.Dafny {
       foreach (KeyValuePair<Function, FuelSettingPair> fuel in fuelContext) {
         Function f = fuel.Key;
         FuelSettingPair settings = fuel.Value;
-        FuelConstant fuelConstant = Translator.FunctionFuel.Find(x => x.f == f);
+        FuelConstant fuelConstant = this.functionFuel.Find(x => x.f == f);
         if (fuelConstant != null) {
           Bpl.Expr startFuel = fuelConstant.startFuel;
           Bpl.Expr startFuelAssert = fuelConstant.startFuelAssert;
@@ -10530,7 +10532,7 @@ namespace Microsoft.Dafny {
             setting = FuelAttrib(f, out found);
           }
 
-          FuelConstant fuelConstant = Translator.FunctionFuel.Find(x => x.f == f);
+          FuelConstant fuelConstant = translator.functionFuel.Find(x => x.f == f);
           if (this.amount == (int)FuelAmount.LOW) {
             return GetFunctionFuel(setting.low, found, fuelConstant);
           } else if (this.amount == (int)FuelAmount.HIGH) {
-- 
cgit v1.2.3