Merge

12 files changed, 163 insertions, 109 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 0d77ecc6..60e737b1 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -105,7 +105,7 @@ namespace Microsoft.Dafny
         if (d is DefaultClassDecl) {

           return new DefaultClassDecl(m, mm);

         } else {

-            return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), new List<IToken> { dd.TraitId });

+            return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitTyp);

         }

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 1aa15145..0e8b886b 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -247,9 +247,9 @@ namespace Microsoft.Dafny {
           else if (d is ClassDecl) {

             var cl = (ClassDecl)d;

             Indent(indent);

-            if (cl.Trait != null && cl.Trait is TraitDecl)

+            if (cl.TraitObj != null && cl.TraitObj is TraitDecl)

             {

-                wr.WriteLine("public class @{0} : @{1}", cl.CompileName, cl.TraitId.val);

+                wr.WriteLine("public class @{0} : @{1}", cl.CompileName, ((UserDefinedType)cl.TraitTyp).tok);

             }

             else

                 wr.Write("public class @{0}", cl.CompileName);

@@ -487,7 +487,7 @@ namespace Microsoft.Dafny {
 

         Indent(indent);  wr.WriteLine("}");

       }

-      constructorIndex ++;

+      constructorIndex++;

     }

 

     void CompileDatatypeStruct(DatatypeDecl dt, int indent) {

@@ -767,7 +767,7 @@ namespace Microsoft.Dafny {
                   {

                       Indent(indent);

                       wr.WriteLine("public {0} @{1};", TypeName(f.Type), f.CompileName);

-                      wr.Write("{0} @{1}.@{2}", TypeName(f.Type), c.Trait.CompileName, f.CompileName);

+                      wr.Write("{0} @{1}.@{2}", TypeName(f.Type), c.TraitObj.CompileName, f.CompileName);

                       wr.WriteLine(" {");

                       wr.WriteLine(" get { ");

                       wr.Write("return this.@{0};", f.CompileName);

@@ -1179,7 +1179,7 @@ namespace Microsoft.Dafny {
               if (!(rhs is HavocRhs)) {

                 lvalues.Add(CreateLvalue(lhs, indent));

 

-                string target = "_rhs" + FreshTmpVarCount();

+                string target = VariableNameGenerator.FreshVariableName("_rhs");

                 rhss.Add(target);

                 TrRhs("var " + target, null, rhs, indent);

               }

@@ -1240,7 +1240,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(s.Bounds != null);  // follows from s.MissingBounds == null

           var n = s.Lhss.Count;

           Contract.Assert(s.Bounds.Count == n);

-          var c = FreshTmpVarCount();

+          var c = VariableNameGenerator.FreshVariableCount();

           var doneLabel = "_ASSIGN_SUCH_THAT_" + c;

           var iterLimit = "_iterLimit_" + c;

 

@@ -1259,7 +1259,7 @@ namespace Microsoft.Dafny {
               Indent(ind);

               wr.WriteLine("var {0}_{1} = {0};", iterLimit, i);

             }

-            var tmpVar = "_assign_such_that_" + FreshTmpVarCount();

+            var tmpVar = VariableNameGenerator.FreshVariableName("_assign_such_that_");

             Indent(ind);

             if (bound is ComprehensionExpr.BoolBoundedPool) {

               wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);

@@ -1475,7 +1475,7 @@ namespace Microsoft.Dafny {
         // be nested.

 

         // Temporary names

-        var c = FreshTmpVarCount();

+        var c = VariableNameGenerator.FreshVariableCount();

         string ingredients = "_ingredients" + c;

         string tup = "_tup" + c;

 

@@ -1628,7 +1628,7 @@ namespace Microsoft.Dafny {
         //   ...

         // }

         if (s.Cases.Count != 0) {

-          string source = "_source" + FreshTmpVarCount();

+          string source = VariableNameGenerator.FreshVariableName("_source");

           Indent(indent);

           wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type)), source);

           TrExpr(s.Source);

@@ -1671,7 +1671,7 @@ namespace Microsoft.Dafny {
         return "@" + ll.Var.CompileName;

       } else if (lhs is MemberSelectExpr) {

         var ll = (MemberSelectExpr)lhs;

-        string obj = "_obj" + FreshTmpVarCount();

+        string obj = VariableNameGenerator.FreshVariableName("_obj");

         Indent(indent);

         wr.Write("var {0} = ", obj);

         TrExpr(ll.Obj);

@@ -1679,7 +1679,7 @@ namespace Microsoft.Dafny {
         return string.Format("{0}.@{1}", obj, ll.Member.CompileName);

       } else if (lhs is SeqSelectExpr) {

         var ll = (SeqSelectExpr)lhs;

-        var c = FreshTmpVarCount();

+        var c = VariableNameGenerator.FreshVariableCount();

         string arr = "_arr" + c;

         string index = "_index" + c;

         Indent(indent);

@@ -1693,7 +1693,7 @@ namespace Microsoft.Dafny {
         return string.Format("{0}[(int){1}]", arr, index);

       } else {

         var ll = (MultiSelectExpr)lhs;

-        var c = FreshTmpVarCount();

+        var c = VariableNameGenerator.FreshVariableCount();

         string arr = "_arr" + c;

         Indent(indent);

         wr.Write("var {0} = ", arr);

@@ -1720,7 +1720,7 @@ namespace Microsoft.Dafny {
       Contract.Requires((target == null) != (targetExpr == null));

       var tRhs = rhs as TypeRhs;

       if (tRhs != null && tRhs.InitCall != null) {

-        string nw = "_nw" + FreshTmpVarCount();

+        string nw = VariableNameGenerator.FreshVariableName("_nw");

         Indent(indent);

         wr.Write("var {0} = ", nw);

         TrAssignmentRhs(rhs);  // in this case, this call will not require us to spill any let variables first

@@ -1771,7 +1771,7 @@ namespace Microsoft.Dafny {
           // TODO:  What to do here?  When does this happen, what does it mean?

         } else if (!s.Method.IsStatic) {

 

-          string inTmp = "_in" + FreshTmpVarCount();

+          string inTmp = VariableNameGenerator.FreshVariableName("_in");

           inTmps.Add(inTmp);

           Indent(indent);

           wr.Write("var {0} = ", inTmp);

@@ -1781,7 +1781,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < s.Method.Ins.Count; i++) {

           Formal p = s.Method.Ins[i];

           if (!p.IsGhost) {

-            string inTmp = "_in" + FreshTmpVarCount();

+            string inTmp = VariableNameGenerator.FreshVariableName("_in");

             inTmps.Add(inTmp);

             Indent(indent);

             wr.Write("var {0} = ", inTmp);

@@ -1823,7 +1823,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < s.Method.Outs.Count; i++) {

           Formal p = s.Method.Outs[i];

           if (!p.IsGhost) {

-            string target = "_out" + FreshTmpVarCount();

+            string target = VariableNameGenerator.FreshVariableName("_out");

             outTmps.Add(target);

             Indent(indent);

             wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);

@@ -1879,11 +1879,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    int tmpVarCount = 0;

-    int FreshTmpVarCount()

-    {

-      return tmpVarCount++;

-    }

+    FreshVariableNameGenerator VariableNameGenerator = new FreshVariableNameGenerator();

 

     /// <summary>

     /// Before calling TrAssignmentRhs(rhs), the caller must have spilled the let variables declared in "rhs".

@@ -2249,7 +2245,7 @@ namespace Microsoft.Dafny {
               string arg;

               var fce = actual as FunctionCallExpr;

               if (fce == null || fce.CoCall != FunctionCallExpr.CoCallResolution.Yes) {

-                string varName = "_ac" + FreshTmpVarCount();

+                string varName = VariableNameGenerator.FreshVariableName("_ac");

                 arg = varName;

 

                 wr.Write("var {0} = ", varName);

@@ -2258,7 +2254,7 @@ namespace Microsoft.Dafny {
               } else {

                 var sw = new StringWriter();

                 CompileFunctionCallExpr(fce, sw, (exp) => {

-                  string varName = "_ac" + FreshTmpVarCount();

+                  string varName = VariableNameGenerator.FreshVariableName("_ac");

                   sw.Write(varName);

 

                   wr.Write("var {0} = ", varName);

@@ -2571,7 +2567,7 @@ namespace Microsoft.Dafny {
         //   }

         // }(src)

 

-        string source = "_source" + FreshTmpVarCount();

+        string source = VariableNameGenerator.FreshVariableName("_source");

         wr.Write("new Dafny.Helpers.Function<{0}, {1}>(delegate ({0} {2}) {{ ", TypeName(e.Source.Type), TypeName(e.Type), source);

 

         if (e.Cases.Count == 0) {

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index edbac407..68a24e6c 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -355,7 +355,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
 = (. Contract.Requires(module != null);

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

      IToken/*!*/ id;

-     List<IToken>/*!*/ traitId=null;

+     Type/*!*/ trait = null;

 	 Attributes attrs = null;

      List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();

      List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

@@ -366,12 +366,12 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
   { Attribute<ref attrs> }

   NoUSIdent<out id>

   [ GenericParameters<typeArgs> ]

-  ["extends" QualifiedName<out traitId>]

-  "{"                                            (. bodyStart = t; .)

+  ["extends" Type<out trait>]         

+  "{"                                            (. bodyStart = t;  .)

   { ClassMemberDecl<members, true>

   }

   "}"

-  (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);

+  (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, trait);

      c.BodyStartTok = bodyStart;

      c.BodyEndTok = t;

   .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 18e64b98..58666c6a 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1688,8 +1688,8 @@ namespace Microsoft.Dafny {
 

   public class ClassDecl : TopLevelDecl {

     public readonly List<MemberDecl> Members;

-    public TraitDecl Trait;

-    public readonly IToken TraitId;

+    public TraitDecl TraitObj;

+    public readonly Type TraitTyp;

     public bool HasConstructor;  // filled in (early) during resolution; true iff there exists a member that is a Constructor

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -1697,7 +1697,7 @@ namespace Microsoft.Dafny {
     }

 

     public ClassDecl(IToken tok, string name, ModuleDefinition module,

-      List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, List<IToken> traitId)

+      List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, Type trait)

       : base(tok, name, module, typeArgs, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -1705,8 +1705,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(typeArgs));

       Contract.Requires(cce.NonNullElements(members));

       Members = members;

-      if (traitId != null && traitId.Count > 0)

-          TraitId = traitId[0]; //there are at most one inheriting trait at the moment

+      if (trait != null)

+          TraitTyp = trait; //there are at most one inheriting trait at the moment

     }

     public virtual bool IsDefaultClass {

       get {

@@ -6195,6 +6195,7 @@ namespace Microsoft.Dafny {
 

   public abstract class QuantifierExpr : ComprehensionExpr, TypeParameter.ParentType {

     public List<TypeParameter> TypeArgs;

+    // TODO(wuestholz): Can we make this non-static?

     private static int quantCount = 0;

     private readonly int quantUnique;

     public string FullName {

@@ -6202,11 +6203,11 @@ namespace Microsoft.Dafny {
         return "q$" + quantUnique;

       }

     }

-    public String Refresh(String s, int counter) {

-      return s + "#" + counter + FullName;

+    public String Refresh(string prefix, FreshVariableNameGenerator freshVarNameGen) {

+      return freshVarNameGen.FreshVariableName(prefix + "#") + FullName;

     }

-    public TypeParameter Refresh(TypeParameter p, int counter) {

-      var cp = new TypeParameter(p.tok, counter + "#" + p.Name, p.EqualitySupport);

+    public TypeParameter Refresh(TypeParameter p, FreshVariableNameGenerator freshVarNameGen) {

+      var cp = new TypeParameter(p.tok, freshVarNameGen.FreshVariableCount() + "#" + p.Name, p.EqualitySupport);

       cp.Parent = this;

       return cp;

     }

@@ -6302,6 +6303,7 @@ namespace Microsoft.Dafny {
 

   public class LambdaExpr : ComprehensionExpr

   {

+    // TODO(wuestholz): Can we make this non-static?

     private static int lamUniques = 0;

 

     public readonly bool OneShot;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 5135712d..d710b72b 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -466,7 +466,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		Contract.Requires(module != null);

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

 		IToken/*!*/ id;

-		List<IToken>/*!*/ traitId=null;

+		Type/*!*/ trait = null;

 		Attributes attrs = null;

 		List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();

 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

@@ -483,15 +483,15 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		}

 		if (la.kind == 36) {

 			Get();

-			QualifiedName(out traitId);

+			Type(out trait);

 		}

 		Expect(20);

-		bodyStart = t; 

+		bodyStart = t;  

 		while (StartOf(2)) {

 			ClassMemberDecl(members, true);

 		}

 		Expect(21);

-		c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);

+		c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, trait);

 		c.BodyStartTok = bodyStart;

 		c.BodyEndTok = t;

 		

@@ -838,6 +838,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		Expect(52);

 	}

 

+	void Type(out Type ty) {

+		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; 

+		TypeAndToken(out tok, out ty);

+	}

+

 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

 		Contract.Requires(cce.NonNullElements(mm));

 		Attributes attrs = null;

@@ -1165,11 +1170,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		}

 	}

 

-	void Type(out Type ty) {

-		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; 

-		TypeAndToken(out tok, out ty);

-	}

-

 	void Expression(out Expression e, bool allowSemi, bool allowLambda) {

 		Expression e0; IToken endTok; 

 		EquivExpression(out e, allowSemi, allowLambda);

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 9e569ef1..36eeb554 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -298,8 +298,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(c != null);

       Indent(indent);

       PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);

-      if (c.TraitId != null) {

-        wr.Write(" extends {0}", c.TraitId.val);

+      if (c.TraitTyp != null) {

+          wr.Write(" extends {0}", ((UserDefinedType)(c.TraitTyp)).tok);

       }

       if (c.Members.Count == 0) {

         wr.WriteLine(" { }");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d93da698..b6b0ab0b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -492,17 +492,17 @@ namespace Microsoft.Dafny
       return anyChangeToDecreases;

     }

 

-    public static Expression FrameArrowToObjectSet(Expression e, Func<int> freshTmp) {

+    public static Expression FrameArrowToObjectSet(Expression e, FreshVariableNameGenerator freshVarNameGen) {

       var arrTy = e.Type.AsArrowType;

       if (arrTy != null) {

         var bvars = new List<BoundVar>();

         var bexprs = new List<Expression>();

         foreach (var t in arrTy.Args) {

-          var bv = new BoundVar(e.tok, "_x" + freshTmp(), t);

+          var bv = new BoundVar(e.tok, freshVarNameGen.FreshVariableName("_x"), t);

           bvars.Add(bv);

           bexprs.Add(new IdentifierExpr(e.tok, bv.Name) { Type = bv.Type, Var = bv });

         }

-        var oVar = new BoundVar(e.tok, "_o" + freshTmp(), new ObjectType());

+        var oVar = new BoundVar(e.tok, freshVarNameGen.FreshVariableName("_o"), new ObjectType());

         var obj = new IdentifierExpr(e.tok, oVar.Name) { Type = oVar.Type, Var = oVar };

         bvars.Add(oVar);

 

@@ -531,13 +531,13 @@ namespace Microsoft.Dafny
 

       List<Expression> sets = new List<Expression>();

       List<Expression> singletons = null;

-      int tmpVarCount = 0;

+      var freshVarNameGen = new FreshVariableNameGenerator();

       foreach (FrameExpression fe in fexprs) {

         Contract.Assert(fe != null);

         if (fe.E is WildcardExpr) {

           // drop wildcards altogether

         } else {

-          Expression e = FrameArrowToObjectSet(fe.E, () => ++tmpVarCount);  // keep only fe.E, drop any fe.Field designation

+          Expression e = FrameArrowToObjectSet(fe.E, freshVarNameGen);  // keep only fe.E, drop any fe.Field designation

           Contract.Assert(e.Type != null);  // should have been resolved already

           var eType = e.Type.NormalizeExpand();

           if (eType.IsRefType) {

@@ -549,7 +549,7 @@ namespace Microsoft.Dafny
           } else if (eType is SeqType) {

             // e represents a sequence

             // Add:  set x :: x in e

-            var bv = new BoundVar(e.tok, "_s2s_" + (++tmpVarCount), ((SeqType)eType).Arg);

+            var bv = new BoundVar(e.tok, freshVarNameGen.FreshVariableName("_s2s_"), ((SeqType)eType).Arg);

             var bvIE = new IdentifierExpr(e.tok, bv.Name);

             bvIE.Var = bv;  // resolve here

             bvIE.Type = bv.Type;  // resolve here

@@ -2657,21 +2657,22 @@ namespace Microsoft.Dafny
       currentClass = cl;

 

       // Resolve names of traits extended

-      if (cl.TraitId != null) {

-        var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val);

+      if (cl.TraitTyp != null && cl.TraitTyp is UserDefinedType)

+      {

+          var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == ((UserDefinedType)(cl.TraitTyp)).FullCompileName);

         if (trait == null) {

-          Error(cl.TraitId, "unresolved identifier: {0}", cl.TraitId.val);

+            Error(((UserDefinedType)(cl.TraitTyp)).tok, "unresolved identifier: {0}", ((UserDefinedType)(cl.TraitTyp)).tok.val);

         } else if (!(trait is TraitDecl)) {

-          Error(cl.TraitId, "identifier '{0}' does not denote a trait", cl.TraitId.val);

+            Error(((UserDefinedType)(cl.TraitTyp)).tok, "identifier '{0}' does not denote a trait", ((UserDefinedType)(cl.TraitTyp)).tok.val);

         } else {

           //disallowing inheritance in multi module case

           string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty);

           string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty);

           if (clModName != traitModName) {

-            Error(cl.TraitId, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module",

+              Error(((UserDefinedType)(cl.TraitTyp)).tok, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module",

                 cl.FullName, trait.FullName));

           } else {

-            cl.Trait = (TraitDecl)trait;

+            cl.TraitObj = (TraitDecl)trait;

           }

         }

       }

@@ -2730,9 +2731,9 @@ namespace Microsoft.Dafny
       Contract.Requires(cl != null);

 

       //merging class members with parent members if any

-      if (cl.Trait != null) {

+      if (cl.TraitObj != null) {

         var clMembers = classMembers[cl];

-        var traitMembers = classMembers[cl.Trait];

+        var traitMembers = classMembers[cl.TraitObj];

         //merging current class members with the inheriting trait

         foreach (KeyValuePair<string, MemberDecl> traitMem in traitMembers) {

           MemberDecl clMember;

@@ -2815,7 +2816,7 @@ namespace Microsoft.Dafny
         //checking to make sure all body-less methods/functions have been implemented in the child class

         if (refinementTransformer == null)

           refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null);

-        foreach (MemberDecl traitMember in cl.Trait.Members.Where(mem => mem is Function || mem is Method)) {

+        foreach (MemberDecl traitMember in cl.TraitObj.Members.Where(mem => mem is Function || mem is Method)) {

           if (traitMember is Function) {

             Function traitFunc = (Function)traitMember;

             if (traitFunc.Body == null) //we do this check only if trait function body is null

@@ -4021,9 +4022,9 @@ namespace Microsoft.Dafny
           }

           return successSoFar;

         } else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) {

-          return ((ClassDecl)bb.ResolvedClass).Trait.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;

+          return ((ClassDecl)bb.ResolvedClass).TraitObj.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;

         } else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) {

-          return ((ClassDecl)aa.ResolvedClass).Trait.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName;

+          return ((ClassDecl)aa.ResolvedClass).TraitObj.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName;

         } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {

           // type parameters

           if (aa.TypeArgs.Count != bb.TypeArgs.Count) {

@@ -4717,11 +4718,15 @@ namespace Microsoft.Dafny
       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

         bool bodyMustBeSpecOnly = specContextOnly;

+        var fvs = new HashSet<IVariable>();

+        bool usesHeap = false, usesOldHeap = false;

+        Type usesThis = null;

         if (s.Guard != null) {

           int prevErrorCount = ErrorCount;

           ResolveExpression(s.Guard, new ResolveOpts(codeContext, true));

           Contract.Assert(s.Guard.Type != null);  // follows from postcondition of ResolveExpression

           bool successfullyResolved = ErrorCount == prevErrorCount;

+          Translator.ComputeFreeVariables(s.Guard, fvs, ref usesHeap, ref usesOldHeap, ref usesThis, false);

           if (!UnifyTypes(s.Guard.Type, Type.Bool)) {

             Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);

           }

@@ -4734,6 +4739,7 @@ namespace Microsoft.Dafny
           ResolveAttributes(inv.Attributes, new ResolveOpts(codeContext, true));

           ResolveExpression(inv.E, new ResolveOpts(codeContext, true));

           Contract.Assert(inv.E.Type != null);  // follows from postcondition of ResolveExpression

+          Translator.ComputeFreeVariables(inv.E, fvs, ref usesHeap, ref usesOldHeap, ref usesThis, false);

           if (!UnifyTypes(inv.E.Type, Type.Bool)) {

             Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);

           }

@@ -4756,6 +4762,7 @@ namespace Microsoft.Dafny
           ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true));

           foreach (FrameExpression fe in s.Mod.Expressions) {

             ResolveFrameExpression(fe, "modifies", bodyMustBeSpecOnly, codeContext);

+            Translator.ComputeFreeVariables(fe.E, fvs, ref usesHeap, ref usesOldHeap, ref usesThis, false);

           }

         }

         s.IsGhost = s.Body == null || bodyMustBeSpecOnly;

@@ -4767,6 +4774,17 @@ namespace Microsoft.Dafny
 

           ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);

           loopStack.RemoveAt(loopStack.Count - 1);  // pop

+        } else {

+          string text = "havoc {";

+          if (fvs.Count != 0) {

+            string sep = "";

+            foreach (var fv in fvs) {

+              text += sep + fv.Name;

+              sep = ", ";

+            }

+          }

+          text += "};";  // always terminate with a semi-colon

+          ReportAdditionalInformation(s.Tok, text, s.Tok.val.Length);

         }

 

       } else if (stmt is AlternativeLoopStmt) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4f57d5f9..cdf9eb86 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -14,6 +14,33 @@ using System.Text;
 using Microsoft.Boogie;

 

 namespace Microsoft.Dafny {

+

+  public class FreshVariableNameGenerator

+  {

+    readonly Dictionary<string, int> PrefixToCount = new Dictionary<string, int>();

+

+    public void Reset()

+    {

+      PrefixToCount.Clear();

+    }

+

+    public string FreshVariableName(string prefix = "")

+    {

+      return prefix + FreshVariableCount(prefix);

+    }

+

+    public int FreshVariableCount(string prefix = "")

+    {

+      int old;

+      if (!PrefixToCount.TryGetValue(prefix, out old))

+      {

+        old = 0;

+      }

+      PrefixToCount[prefix] = old + 1;

+      return old;

+    }

+  }

+

   public class Translator {

 

     [NotDelayed]

@@ -482,7 +509,7 @@ namespace Microsoft.Dafny {
     {

         foreach (ModuleDefinition m in program.Modules)

         {

-            if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).Trait != null) || (d is TraitDecl)))

+            if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitObj != null) || (d is TraitDecl)))

             {

                 //adding const unique NoTraitAtAll: ClassName;

                 Token tNoTrait = new Token();

@@ -500,12 +527,12 @@ namespace Microsoft.Dafny {
                     if (d is ClassDecl)

                     {

                         var c = (ClassDecl)d;

-                        if (c is ClassDecl && c.Trait != null)

+                        if (c is ClassDecl && c.TraitObj != null)

                         {

                             //this adds: axiom TraitParent(class.A) == class.J; Where A extends J

-                            Bpl.TypedIdent trait_id = new Bpl.TypedIdent(c.Trait.tok, string.Format("class.{0}", c.Trait.FullSanitizedName), predef.ClassNameType);

-                            Bpl.Constant trait = new Bpl.Constant(c.Trait.tok, trait_id, true);

-                            Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(c.Trait.tok, trait);

+                            Bpl.TypedIdent trait_id = new Bpl.TypedIdent(c.TraitObj.tok, string.Format("class.{0}", c.TraitObj.FullSanitizedName), predef.ClassNameType);

+                            Bpl.Constant trait = new Bpl.Constant(c.TraitObj.tok, trait_id, true);

+                            Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(c.TraitObj.tok, trait);

 

                             var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);

                             var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), false);

@@ -515,7 +542,7 @@ namespace Microsoft.Dafny {
 

                             sink.AddTopLevelDeclaration(traitParentAxiom);

                         }

-                        else if (c is ClassDecl && c.Trait == null)

+                        else if (c is ClassDecl && c.TraitObj == null)

                         {

                             //this adds: axiom TraitParent(class.B) == NoTraitAtAll; Where B does not extend any traits

                             Bpl.TypedIdent noTraitAtAll_id = new Bpl.TypedIdent(c.tok, "NoTraitAtAll", predef.ClassNameType);

@@ -1161,7 +1188,7 @@ namespace Microsoft.Dafny {
       args = new List<Bpl.Expr>();

       foreach (Formal arg in formals) {

         Contract.Assert(arg != null);

-        var nm = string.Format("a{0}#{1}", bvs.Count, FreshOtherTmpVarCount());

+        var nm = string.Format("a{0}#{1}", bvs.Count, FreshVarNameGenerator.FreshVariableName());

         Bpl.Variable bv = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, nm, TrType(arg.Type)));

         bvs.Add(bv);

         args.Add(new Bpl.IdentifierExpr(arg.tok, bv));

@@ -1298,14 +1325,14 @@ namespace Microsoft.Dafny {
       //this adds: axiom implements$J(class.C);

       else if (c is ClassDecl)

       {

-          if (c.Trait != null)

+          if (c.TraitObj != null)

           {

               //var dtypeFunc = FunctionCall(c.tok, BuiltinFunction.DynamicType, null, o);

               //Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });

 

               var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);

               var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

-              var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + c.TraitId.val, new List<Variable> { args }, ret_value));

+              var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + ((UserDefinedType)(c.TraitTyp)).tok, new List<Variable> { args }, ret_value));

               var expr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });

               var implements_axiom = new Bpl.Axiom(c.tok, expr);

               sink.AddTopLevelDeclaration(implements_axiom);

@@ -1709,7 +1736,7 @@ namespace Microsoft.Dafny {
       currentModule = null;

       codeContext = null;

       loopHeapVarCount = 0;

-      otherTmpVarCount = 0;

+      FreshVarNameGenerator.Reset();

       _tmpIEs.Clear();

     }

 

@@ -2527,16 +2554,15 @@ namespace Microsoft.Dafny {
     ICallable codeContext = null;  // the method/iterator whose implementation is currently being translated or the function whose specification is being checked for well-formedness

     Bpl.LocalVariable yieldCountVariable = null;  // non-null when an iterator body is being translated

     bool assertAsAssume = false; // generate assume statements instead of assert statements

+

     int loopHeapVarCount = 0;

     int FreshLoopHeadVarCount()

     {

       return loopHeapVarCount++;

     }

-    int otherTmpVarCount = 0;

-    int FreshOtherTmpVarCount()

-    {

-      return otherTmpVarCount++;

-    }

+

+    public readonly FreshVariableNameGenerator FreshVarNameGenerator = new FreshVariableNameGenerator();

+

     Dictionary<string, Bpl.IdentifierExpr> _tmpIEs = new Dictionary<string, Bpl.IdentifierExpr>();

     Bpl.IdentifierExpr GetTmpVar_IdExpr(IToken tok, string name, Bpl.Type ty, List<Variable> locals)  // local variable that's shared between statements that need it

     {

@@ -3802,7 +3828,7 @@ namespace Microsoft.Dafny {
           e = Substitute(e, receiverReplacement, substMap);

         }

 

-        e = Resolver.FrameArrowToObjectSet(e, FreshOtherTmpVarCount);

+        e = Resolver.FrameArrowToObjectSet(e, FreshVarNameGenerator);

 

         Bpl.Expr disjunct;

         var eType = e.Type.NormalizeExpand();

@@ -4127,7 +4153,7 @@ namespace Microsoft.Dafny {
       var args = new List<Bpl.Expr>();

       foreach (Formal arg in ctor.Formals) {

         Contract.Assert(arg != null);

-        var nm = string.Format("a{0}#{1}", args.Count, FreshOtherTmpVarCount());

+        var nm = string.Format("a{0}#{1}", args.Count, FreshVarNameGenerator.FreshVariableCount());

         Bpl.Variable bv = new Bpl.LocalVariable(arg.tok, new Bpl.TypedIdent(arg.tok, nm, TrType(arg.Type)));

         locals.Add(bv);

         args.Add(new Bpl.IdentifierExpr(arg.tok, bv));

@@ -4296,7 +4322,7 @@ namespace Microsoft.Dafny {
 

         List<Bpl.Variable> bvars = new List<Bpl.Variable>();

 

-        Func<string, string> MkName = s => "$l" + FreshOtherTmpVarCount() + "#" + s;

+        Func<string, string> MkName = s => "$l" + FreshVarNameGenerator.FreshVariableCount() + "#" + s;

 

         Bpl.Expr heap; var hVar = BplBoundVar(MkName("heap"), predef.HeapType, out heap);

         bvars.Add(hVar);

@@ -4468,7 +4494,7 @@ namespace Microsoft.Dafny {
       public Action<IToken, Bpl.Expr, string, Bpl.QKeyValue> AssertSink(Translator tran, StmtListBuilder builder) {

         return (t, e, s, qk) => {

           if (Locals != null) {

-            var b = BplLocalVar("b$reqreads#" + tran.FreshOtherTmpVarCount(), Bpl.Type.Bool, Locals);

+            var b = BplLocalVar(tran.FreshVarNameGenerator.FreshVariableName("b$reqreads#"), Bpl.Type.Bool, Locals);

             Asserts.Add(tran.Assert(t, b, s, qk));

             builder.Add(Bpl.Cmd.SimpleAssign(e.tok, (Bpl.IdentifierExpr)b, e));

           } else {

@@ -4933,7 +4959,7 @@ namespace Microsoft.Dafny {
           for (int i = 0; i < e.LHSs.Count; i++) {

             var pat = e.LHSs[i];

             var rhs = e.RHSs[i];

-            var nm = string.Format("let{0}#{1}", i, FreshOtherTmpVarCount());

+            var nm = string.Format("let{0}#{1}", i, FreshVarNameGenerator.FreshVariableCount());

             var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(rhs.Type)));

             locals.Add(r);

             var rIe = new Bpl.IdentifierExpr(pat.tok, r);

@@ -5000,7 +5026,7 @@ namespace Microsoft.Dafny {
         var typeMap = new Dictionary<TypeParameter, Type>();

         var copies = new List<TypeParameter>();

         if (q != null) {

-          copies = Map(q.TypeArgs, tp => q.Refresh(tp, FreshOtherTmpVarCount()));

+          copies = Map(q.TypeArgs, tp => q.Refresh(tp, FreshVarNameGenerator));

           typeMap = Util.Dict(q.TypeArgs, Map(copies, tp => (Type)new UserDefinedType(tp)));

         }

         locals.AddRange(Map(copies,

@@ -5019,7 +5045,7 @@ namespace Microsoft.Dafny {
             // Havoc heap, unless oneShot

             if (!lam.OneShot) {

               Bpl.Expr oldHeap;

-              locals.Add(BplLocalVar("$oldHeap#" + FreshOtherTmpVarCount(), predef.HeapType, out oldHeap));

+              locals.Add(BplLocalVar(FreshVarNameGenerator.FreshVariableName("$oldHeap#"), predef.HeapType, out oldHeap));

               newBuilder.Add(BplSimplestAssign(oldHeap, etran.HeapExpr));

               newBuilder.Add(new HavocCmd(expr.tok, Singleton((Bpl.IdentifierExpr)etran.HeapExpr)));

               newBuilder.Add(new AssumeCmd(expr.tok,

@@ -5028,7 +5054,7 @@ namespace Microsoft.Dafny {
             }

 

             // Set up a new frame

-            var frameName = "$_Frame#l" + FreshOtherTmpVarCount();

+            var frameName = FreshVarNameGenerator.FreshVariableName("$_Frame#l");

             reads = lam.Reads.ConvertAll(s.SubstFrameExpr);

             DefineFrame(e.tok, reads, newBuilder, locals, frameName);

             newEtran = new ExpressionTranslator(newEtran, frameName);

@@ -5170,7 +5196,7 @@ namespace Microsoft.Dafny {
         return;

       }

 

-      var oVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "newtype$check#" + FreshOtherTmpVarCount(), TrType(expr.Type)));

+      var oVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, FreshVarNameGenerator.FreshVariableName("newtype$check#"), TrType(expr.Type)));

       locals.Add(oVar);

       var o = new Bpl.IdentifierExpr(tok, oVar);

       builder.Add(Bpl.Cmd.SimpleAssign(tok, o, etran.TrExpr(expr)));

@@ -5231,7 +5257,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.ValueAtReturn(out bv) != null);

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

 

-      bv = new BoundVar(tok, prefix + FreshOtherTmpVarCount(), iv.Type); // use this temporary variable counter, but for a Dafny name (the idea being that the number and the initial "_" in the name might avoid name conflicts)

+      bv = new BoundVar(tok, prefix + FreshVarNameGenerator.FreshVariableCount(), iv.Type); // use this temporary variable counter, but for a Dafny name (the idea being that the number and the initial "_" in the name might avoid name conflicts)

       ie = new IdentifierExpr(tok, bv.Name);

       ie.Var = bv;  // resolve here

       ie.Type = bv.Type;  // resolve here

@@ -6158,7 +6184,7 @@ namespace Microsoft.Dafny {
         var bLhs = m.Outs[i];

         if (!ModeledAsBoxType(method.Outs[i].Type) && ModeledAsBoxType(bLhs.Type)) {

           // we need an Box

-          Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp##" + FreshOtherTmpVarCount(), TrType(method.Outs[i].Type)));

+          Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, FreshVarNameGenerator.FreshVariableName("$tmp##"), TrType(method.Outs[i].Type)));

           localVariables.Add(var);

           Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(bLhs.tok, var.Name, TrType(method.Outs[i].Type));

           tmpOuts.Add(varIdE);

@@ -7920,7 +7946,7 @@ namespace Microsoft.Dafny {
 

       // Now for the other branch, where the postcondition of the call is exported.

       {

-        var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$initHeapForallStmt#" + FreshOtherTmpVarCount(), predef.HeapType));

+        var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, FreshVarNameGenerator.FreshVariableName("$initHeapForallStmt#"), predef.HeapType));

         locals.Add(initHeapVar);

         var initHeap = new Bpl.IdentifierExpr(tok, initHeapVar);

         var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr);

@@ -7982,7 +8008,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

       // Add all newly allocated objects to the set this._new

-      var updatedSet = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$iter_newUpdate" + FreshOtherTmpVarCount(), predef.SetType(iter.tok, predef.BoxType)));

+      var updatedSet = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, FreshVarNameGenerator.FreshVariableName("$iter_newUpdate"), predef.SetType(iter.tok, predef.BoxType)));

       locals.Add(updatedSet);

       var updatedSetIE = new Bpl.IdentifierExpr(iter.tok, updatedSet);

       // call $iter_newUpdate := $IterCollectNewObjects(initHeap, $Heap, this, _new);

@@ -8059,7 +8085,7 @@ namespace Microsoft.Dafny {
 

       // Now for the other branch, where the ensures clauses are exported.

 

-      var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$initHeapForallStmt#" + FreshOtherTmpVarCount(), predef.HeapType));

+      var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, FreshVarNameGenerator.FreshVariableName("$initHeapForallStmt#"), predef.HeapType));

       locals.Add(initHeapVar);

       var initHeap = new Bpl.IdentifierExpr(s.Tok, initHeapVar);

       var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr);

@@ -8341,7 +8367,7 @@ namespace Microsoft.Dafny {
         builder.Add(new CommentCmd("TrCallStmt: Adding lhs " + lhs + " with type " + lhs.Type));

         if (bLhss[i] == null) {  // (in the current implementation, the second parameter "true" to ProcessLhss implies that all bLhss[*] will be null)

           // create temporary local and assign it to bLhss[i]

-          string nm = "$rhs##" + FreshOtherTmpVarCount();

+          string nm = FreshVarNameGenerator.FreshVariableName("$rhs##");

           var ty = TrType(lhs.Type);

           Bpl.Expr wh = GetWhereClause(lhs.tok, new Bpl.IdentifierExpr(lhs.tok, nm, ty), lhs.Type, etran);

           Bpl.LocalVariable var = new Bpl.LocalVariable(lhs.tok, new Bpl.TypedIdent(lhs.tok, nm, ty, wh));

@@ -8352,7 +8378,7 @@ namespace Microsoft.Dafny {
       Bpl.IdentifierExpr initHeap = null;

       if (codeContext is IteratorDecl) {

         // var initHeap := $Heap;

-        var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$initHeapCallStmt#" + FreshOtherTmpVarCount(), predef.HeapType));

+        var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, FreshVarNameGenerator.FreshVariableName("$initHeapCallStmt#"), predef.HeapType));

         locals.Add(initHeapVar);

         initHeap = new Bpl.IdentifierExpr(s.Tok, initHeapVar);

         // initHeap := $Heap;

@@ -8525,7 +8551,7 @@ namespace Microsoft.Dafny {
         var bLhs = Lhss[i];

         if (ModeledAsBoxType(callee.Outs[i].Type) && !ModeledAsBoxType(LhsTypes[i])) {

           // we need an Unbox

-          Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp##" + FreshOtherTmpVarCount(), predef.BoxType));

+          Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, FreshVarNameGenerator.FreshVariableName("$tmp##"), predef.BoxType));

           locals.Add(var);

           Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(bLhs.tok, var.Name, predef.BoxType);

           tmpOuts.Add(varIdE);

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

 

       if (bLhs == null) {

-        var nm = string.Format("$rhs#{0}", FreshOtherTmpVarCount());

+        var nm = FreshVarNameGenerator.FreshVariableName("$rhs#");

         var v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, nm, lhsType == null ? predef.BoxType : TrType(lhsType)));

         locals.Add(v);

         bLhs = new Bpl.IdentifierExpr(tok, v);

@@ -10940,12 +10966,12 @@ 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("$ly", translator.FreshOtherTmpVarCount()), predef.LayerType, bvars);

+            var ly = BplBoundVar(e.Refresh("$ly", translator.FreshVarNameGenerator), predef.LayerType, bvars);

             Expr layer = translator.LayerSucc(ly);

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

           }

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

-            var h = BplBoundVar(e.Refresh("$heap", translator.FreshOtherTmpVarCount()), predef.HeapType, bvars);

+            var h = BplBoundVar(e.Refresh("$heap", translator.FreshVarNameGenerator), predef.HeapType, bvars);

             bodyEtran = new ExpressionTranslator(bodyEtran, h);

             antecedent = BplAnd(new List<Bpl.Expr> {

               antecedent,

@@ -10986,7 +11012,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);

           Bpl.QKeyValue kv = TrAttributes(e.Attributes, null);

 

-          var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.FreshOtherTmpVarCount(), predef.BoxType));

+          var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, translator.FreshVarNameGenerator.FreshVariableName("$y#"), predef.BoxType));

           Bpl.Expr y = new Bpl.IdentifierExpr(expr.tok, yVar);

 

           var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term), e.Term.Type));

@@ -11006,7 +11032,7 @@ namespace Microsoft.Dafny {
 

           Bpl.QKeyValue kv = TrAttributes(e.Attributes, null);

 

-          var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.FreshOtherTmpVarCount(), predef.BoxType));

+          var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, translator.FreshVarNameGenerator.FreshVariableName("$y#"), predef.BoxType));

 

           Bpl.Expr unboxy = translator.UnboxIfBoxed(new Bpl.IdentifierExpr(expr.tok, yVar), bv.Type);

           Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, unboxy, bv.Type, this);

@@ -12277,7 +12303,7 @@ namespace Microsoft.Dafny {
           foreach (var n in inductionVariables) {

             toks.Add(n.tok);

             types.Add(n.Type.NormalizeExpand());

-            BoundVar k = new BoundVar(n.tok, n.Name + "$ih#" + FreshOtherTmpVarCount(), n.Type);

+            BoundVar k = new BoundVar(n.tok, n.Name + "$ih#" + FreshVarNameGenerator.FreshVariableCount(), n.Type);

             kvars.Add(k);

 

             IdentifierExpr ieK = new IdentifierExpr(k.tok, k.AssignUniqueName(currentDeclaration));

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 2bda7cf0..16349ccc 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Dafny
     public static int ThreadMain(string[] args)

     {

       Contract.Requires(cce.NonNullElements(args));

-

+         

       printer = new DafnyConsolePrinter();

       ExecutionEngine.printer = printer;

 

@@ -51,7 +51,7 @@ namespace Microsoft.Dafny
         exitValue = ExitValue.PREPROCESSING_ERROR;

         goto END;

       }

-      //CommandLineOptions.Clo.Files = new List<string> { @"C:\dafny\Test\dafny0\Trait\TraitOverride1.dfy" };

+      //CommandLineOptions.Clo.Files = new List<string> { @"C:\dafny\Test\dafny0\Trait\TraitExtend.dfy" };

 

       if (CommandLineOptions.Clo.Files.Count == 0)

       {

@@ -109,6 +109,7 @@ namespace Microsoft.Dafny
           // TODO(wuestholz): We should probably add a separate flag for this. This is currently only used by the new testing infrastructure.

           return 0;

         }

+        //Console.ReadKey();

         return (int)exitValue;

     }

 

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 91044397..5a2b6e13 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -86,8 +86,8 @@ class Benchmark3 {
    

     while (j < n)

       invariant j <= n;

+      invariant 0 <= k < n && old(q.contents)[k] == m;

       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated

-      invariant 0 <= k < |old(q.contents)| && old(q.contents)[k] == m;

       invariant forall i :: 0 <= i < j ==> m <= old(q.contents)[i]; //m is min so far

     {

       var x := q.Dequeue();

@@ -104,7 +104,6 @@ class Benchmark3 {
       var x := q.Dequeue();

       q.Enqueue(x);

       j := j+1;

-      assert q.contents == old(q.contents)[j..] + old(q.contents)[..j];

     }

 

     m := q.Dequeue();

diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy
index d3164fa9..b283756b 100644
--- a/Test/dafny0/DirtyLoops.dfy
+++ b/Test/dafny0/DirtyLoops.dfy
@@ -19,3 +19,15 @@ method M2(x: int)
     invariant i <= x;

     decreases i;

 }

+

+var f: int;

+

+method M3(x: int)

+  requires f <= x;

+  modifies `f;

+{

+  while (0 < f)

+    invariant f <= x;

+    decreases f;

+    modifies `f;

+}

diff --git a/Test/dafny0/DirtyLoops.dfy.expect b/Test/dafny0/DirtyLoops.dfy.expect
index 060f3287..99fb4165 100644
--- a/Test/dafny0/DirtyLoops.dfy.expect
+++ b/Test/dafny0/DirtyLoops.dfy.expect
@@ -1,4 +1,4 @@
 

-Dafny program verifier finished with 6 verified, 0 errors

+Dafny program verifier finished with 8 verified, 0 errors

 

 Dafny program verifier finished with 0 verified, 0 errors