Merge.

Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.

12 files changed, 735 insertions, 646 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index e89a385f..dd2eed69 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -4,7 +4,6 @@ using System.Collections.Generic;
 using System.Numerics;

 using System.Diagnostics.Contracts;

 using IToken = Microsoft.Boogie.IToken;

-using System.Linq;

 

 namespace Microsoft.Dafny

 {

@@ -229,6 +228,9 @@ namespace Microsoft.Dafny
     public Attributes CloneAttributes(Attributes attrs) {

       if (attrs == null) {

         return null;

+      } else if (attrs.Name.StartsWith("_")) {

+        // skip this attribute, since it would have been produced during resolution

+        return CloneAttributes(attrs.Prev);

       } else {

         return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));

       }

@@ -366,7 +368,6 @@ namespace Microsoft.Dafny
         return new NamedExpr(Tok(e.tok), e.Name, CloneExpr(e.Body));

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

-

         var tk = Tok(e.tok);

         var bvs = e.BoundVars.ConvertAll(CloneBoundVar);

         var range = CloneExpr(e.Range);

@@ -830,7 +831,7 @@ namespace Microsoft.Dafny
           apply.Args.ForEach(arg => args.Add(CloneExpr(arg)));

           var applyClone = new ApplySuffix(Tok(apply.tok), lhsClone, args);

           var c = new ExprRhs(applyClone);

-          reporter.Info(MessageSource.Cloner, apply.tok, mse.Member.Name);

+          reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name);

           return c;

         }

       }

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index c969ac1f..c94f7836 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1201,13 +1201,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(targs));

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

 

-      string s = "";

-      string sep = "";

-      foreach (TypeParameter tp in targs) {

-        s += sep + "@" + tp.CompileName;

-        sep = ",";

-      }

-      return s;

+      return Util.Comma(targs, tp => "@" + tp.CompileName);

     }

 

     string DefaultValue(Type type)

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 07f8e1c4..954448af 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -2915,10 +2915,10 @@ Expressions<.List<Expression> args.>
   .

 /*------------------------------------------------------------------------*/

 Attribute<ref Attributes attrs>

-= (. string name;

+= (. IToken x; string name;

      var args = new List<Expression>();

   .)

-  "{" ":" ident                            (. name = t.val; .)

+  "{" ":" NoUSIdent<out x>                          (. name = x.val; .)

   [ Expressions<args> ]

   "}"

   (. attrs = new Attributes(name, args, attrs); .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e5d8250b..ffd6df63 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2961,19 +2961,6 @@ namespace Microsoft.Dafny {
     }

   }

 

-  /// <summary>

-  /// A "ThisSurrogate" is used during translation time to make the treatment of the receiver more similar to

-  /// the treatment of other in-parameters.

-  /// </summary>

-  public class ThisSurrogate : Formal

-  {

-    public ThisSurrogate(IToken tok, Type type)

-      : base(tok, "this", type, true, false) {

-      Contract.Requires(tok != null);

-      Contract.Requires(type != null);

-    }

-  }

-

   public class BoundVar : NonglobalVariable {

     public override bool IsMutable {

       get {

@@ -3947,6 +3934,9 @@ namespace Microsoft.Dafny {
       public override bool IsFinite {

         get { return false; }

       }

+      public override int Preference() {

+        return 0;

+      }

     }

 

     /// <summary>

@@ -5758,6 +5748,16 @@ namespace Microsoft.Dafny {
       Contract.Requires(name != null);

       Name = name;

     }

+    /// <summary>

+    /// Constructs a resolved IdentifierExpr.

+    /// </summary>

+    public IdentifierExpr(IVariable v)

+      : base(v.Tok) {

+      Contract.Requires(v != null);

+      Name = v.Name;

+      Var = v;

+      Type = v.Type;

+    }

   }

 

   /// <summary>

@@ -6692,9 +6692,33 @@ namespace Microsoft.Dafny {
       public virtual bool IsFinite {

         get { return true; }  // most bounds are finite

       }

+      public abstract int Preference(); // higher is better

+      

+      public static BoundedPool GetBest(List<BoundedPool> bounds) {

+        Contract.Requires(bounds != null && bounds.Count > 0);

+        var ret = bounds[0];

+        foreach (var bound in bounds) {

+          if (bound.Preference() > ret.Preference()) {

+            ret = bound;

+          } else {            

+            var retInt = ret as ComprehensionExpr.IntBoundedPool;

+            if (retInt != null && (retInt.LowerBound == null || retInt.UpperBound == null)) {

+              var boundInt = bound as ComprehensionExpr.IntBoundedPool;

+              if (boundInt != null) {

+                ret = new ComprehensionExpr.IntBoundedPool(retInt.LowerBound ?? boundInt.LowerBound, 

+                                                           retInt.UpperBound ?? boundInt.UpperBound);

+              }

+            }         

+          }

+        }

+        return ret;

+      }

     }

     public class BoolBoundedPool : BoundedPool

     {

+      public override int Preference() {

+        return 5;

+      }

     }

     public class IntBoundedPool : BoundedPool

     {

@@ -6709,36 +6733,57 @@ namespace Microsoft.Dafny {
           return LowerBound != null && UpperBound != null;

         }

       }

+      public override int Preference() {

+        return 1;

+      }

     }

     public class SetBoundedPool : BoundedPool

     {

       public readonly Expression Set;

       public SetBoundedPool(Expression set) { Set = set; }

+      public override int Preference() {

+        return 10;

+      }

     }

     public class SubSetBoundedPool : BoundedPool

     {

       public readonly Expression UpperBound;

       public SubSetBoundedPool(Expression set) { UpperBound = set; }

+      public override int Preference() {

+        return 1;

+      }

     }

     public class SuperSetBoundedPool : BoundedPool

     {

       public readonly Expression LowerBound;

       public SuperSetBoundedPool(Expression set) { LowerBound = set; }

+      public override int Preference() {

+        return 0;

+      }

     }

     public class MapBoundedPool : BoundedPool

     {

       public readonly Expression Map;

       public MapBoundedPool(Expression map) { Map = map; }

+      public override int Preference() {

+        return 10;

+      }

     }

     public class SeqBoundedPool : BoundedPool

     {

       public readonly Expression Seq;

       public SeqBoundedPool(Expression seq) { Seq = seq; }

+      public override int Preference() {

+        return 10;

+      }

     }

     public class DatatypeBoundedPool : BoundedPool

     {

       public readonly DatatypeDecl Decl;

       public DatatypeBoundedPool(DatatypeDecl d) { Decl = d; }

+      public override int Preference() {

+        return 5;

+      }

     }

 

     public List<BoundedPool> Bounds;  // initialized and filled in by resolver

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 245632ad..1986ea6d 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -313,7 +313,7 @@ namespace Microsoft.Dafny
                 2 - apply induction as requested (by attributes) and also

                     for heuristically chosen quantifiers

                 3 (default) - apply induction as requested, and for

-                    heuristically chosen quantifiers and ghost methods

+                    heuristically chosen quantifiers and lemmas

   /inductionHeuristic:<n>

                 0 - least discriminating induction heuristic (that is, lean

                     toward applying induction more often)

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 2507cacc..7dafb572 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1033,13 +1033,13 @@ bool IsType(ref IToken pt) {
 	}

 

 	void Attribute(ref Attributes attrs) {

-		string name;

+		IToken x; string name;

 		var args = new List<Expression>();

 		

 		Expect(45);

 		Expect(21);

-		Expect(1);

-		name = t.val; 

+		NoUSIdent(out x);

+		name = x.val; 

 		if (StartOf(7)) {

 			Expressions(args);

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 971fe867..ce8b54bb 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -109,6 +109,15 @@ namespace Microsoft.Dafny {
       }

     }

 

+    public static string OneAttributeToString(Attributes a, string nameSubstitution = null) {

+      Contract.Requires(a != null);

+      using (var wr = new System.IO.StringWriter()) {

+        var pr = new Printer(wr);

+        pr.PrintOneAttribute(a, nameSubstitution);

+        return ToStringWithoutNewline(wr);

+      }

+    }

+

     public static string ToStringWithoutNewline(System.IO.StringWriter wr) {

       Contract.Requires(wr != null);

       var sb = wr.GetStringBuilder();

@@ -429,15 +438,20 @@ namespace Microsoft.Dafny {
     public void PrintAttributes(Attributes a) {

       if (a != null) {

         PrintAttributes(a.Prev);

-

-        wr.Write(" {{:{0}", a.Name);

-        if (a.Args != null)

-        {

-          PrintAttributeArgs(a.Args, false);

-        }

-        wr.Write("}");

+        wr.Write(" ");

+        PrintOneAttribute(a);

       }

     }

+    public void PrintOneAttribute(Attributes a, string nameSubstitution = null) {

+      Contract.Requires(a != null);

+      var name = nameSubstitution ?? a.Name;

+      var usAttribute = name.StartsWith("_");

+      wr.Write("{1}{{:{0}", name, usAttribute ? "/*" : "");

+      if (a.Args != null) {

+        PrintAttributeArgs(a.Args, false);

+      }

+      wr.Write("}}{0}", usAttribute ? "*/" : "");

+    }

 

     public void PrintAttributeArgs(List<Expression> args, bool isFollowedBySemicolon) {

       Contract.Requires(args != null);

@@ -1430,7 +1444,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

 

         if (parensNeeded) { wr.Write("("); }

-        PrintExpr(e.Seq, 0x00, false, false, !parensNeeded && isFollowedBySemicolon, indent);  // BOGUS: fix me

+        PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);

         wr.Write("[");

         if (e.SelectOne) {

           Contract.Assert( e.E0 != null);

@@ -1454,7 +1468,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

 

         if (parensNeeded) { wr.Write("("); }

-        PrintExpr(e.Array, 0x00, false, false, !parensNeeded && isFollowedBySemicolon, indent);  // BOGUS: fix me

+        PrintExpr(e.Array, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);

         string prefix = "[";

         foreach (Expression idx in e.Indices) {

           Contract.Assert(idx != null);

@@ -1478,7 +1492,7 @@ namespace Microsoft.Dafny {
           bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

 

           if (parensNeeded) { wr.Write("("); }

-          PrintExpr(e.Seq, 00, false, false, !parensNeeded && isFollowedBySemicolon, indent);  // BOGUS: fix me

+          PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);

           wr.Write("[");

           PrintExpression(e.Index, false);

           wr.Write(" := ");

@@ -1797,9 +1811,12 @@ namespace Microsoft.Dafny {
 

       } else if (expr is LambdaExpr) {

         var e = (LambdaExpr)expr;

-        wr.Write("(");

-        wr.Write(Util.Comma(e.BoundVars, bv => bv.DisplayName + ":" + bv.Type));

-        wr.Write(")");

+        bool parensNeeded = !isRightmost;

+        if (parensNeeded) { wr.Write("("); }

+        var skipSignatureParens = e.BoundVars.Count == 1 && e.BoundVars[0].Type is InferredTypeProxy;

+        if (!skipSignatureParens) { wr.Write("("); }

+        wr.Write(Util.Comma(", ", e.BoundVars, bv => bv.DisplayName + (bv.Type is InferredTypeProxy ? "" : ": " + bv.Type)));

+        if (!skipSignatureParens) { wr.Write(")"); }

         if (e.Range != null) {

           wr.Write(" requires ");

           PrintExpression(e.Range, false);

@@ -1810,6 +1827,7 @@ namespace Microsoft.Dafny {
         }

         wr.Write(e.OneShot ? " -> " : " => ");

         PrintExpression(e.Body, isFollowedBySemicolon);

+        if (parensNeeded) { wr.Write(")"); }

 

       } else if (expr is WildcardExpr) {

         wr.Write("*");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 34d4e5c7..ca667ae0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -237,10 +237,12 @@ namespace Microsoft.Dafny
       rewriters.Add(new TimeLimitRewriter(reporter));

 

       if (DafnyOptions.O.AutoTriggers) {

-        rewriters.Add(new QuantifierSplittingRewriter(this.reporter));

-        rewriters.Add(new TriggerGeneratingRewriter(this.reporter));

+        rewriters.Add(new QuantifierSplittingRewriter(reporter));

+        rewriters.Add(new TriggerGeneratingRewriter(reporter));

       }

 

+      rewriters.Add(new InductionRewriter(reporter));

+

       systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);

       prog.CompileModules.Add(prog.BuiltIns.SystemModule);

 

@@ -481,14 +483,7 @@ namespace Microsoft.Dafny
               showIt = ((Method)m).IsRecursive;

             }

             if (showIt) {

-              s += "decreases ";

-              if (m.Decreases.Expressions.Count != 0) {

-                string sep = "";

-                foreach (var d in m.Decreases.Expressions) {

-                  s += sep + Printer.ExprToString(d);

-                  sep = ", ";

-                }

-              }

+              s += "decreases " + Util.Comma(", ", m.Decreases.Expressions, Printer.ExprToString);

               // Note, in the following line, we use the location information for "clbl", not "m".  These

               // are the same, except in the case where "clbl" is a CoLemma and "m" is a prefix lemma.

               reporter.Info(MessageSource.Resolver, clbl.Tok, s);

@@ -5102,15 +5097,7 @@ 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

+          string text = "havoc {" + Util.Comma(", ", fvs, fv => fv.Name) + "};";  // always terminate with a semi-colon

           reporter.Info(MessageSource.Resolver, s.Tok, text);

         }

 

@@ -5209,7 +5196,7 @@ namespace Microsoft.Dafny
               // add the conclusion of the calc as a free postcondition

               var result = ((CalcStmt)s0).Result;

               s.Ens.Add(new MaybeFreeExpression(result, true));

-              reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(result) + ";");

+              reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(result));

             } else {

               s.Kind = ForallStmt.ParBodyKind.Proof;

               if (s.Body is BlockStmt && ((BlockStmt)s.Body).Body.Count == 0) {

@@ -5408,7 +5395,7 @@ namespace Microsoft.Dafny
       }

       if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {

         // We could complain about the syntactic omission of constructors:

-        //   Error(stmt, "match statement does not cover all constructors");

+        //   reporter.Error(MessageSource.Resolver, stmt, "match statement does not cover all constructors");

         // but instead we let the verifier do a semantic check.

         // So, for now, record the missing constructors:

         foreach (var ctr in dtd.Ctors) {

@@ -5815,15 +5802,7 @@ namespace Microsoft.Dafny
         loopStmt.InferredDecreases = true;

       }

       if (loopStmt.InferredDecreases) {

-        string s = "decreases ";

-        if (theDecreases.Count != 0) {

-          string sep = "";

-          foreach (var d in theDecreases) {

-            s += sep + Printer.ExprToString(d);

-            sep = ", ";

-          }

-        }

-        s += ";";  // always terminate with a semi-colon, even in the case of an empty decreases clause

+        string s = "decreases " + Util.Comma(", ", theDecreases, Printer.ExprToString);

         reporter.Info(MessageSource.Resolver, loopStmt.Tok, s);

       }

     }

@@ -6002,8 +5981,7 @@ namespace Microsoft.Dafny
           s.Bounds = new List<ComprehensionExpr.BoundedPool>();

           foreach (var pair in allBounds) {

             Contract.Assert(1 <= pair.Item2.Count);

-            // TODO: The following could be improved by picking the bound that is most likely to give rise to an efficient compiled program

-            s.Bounds.Add(pair.Item2[0]);

+            s.Bounds.Add(ComprehensionExpr.BoundedPool.GetBest(pair.Item2));

           }

         }

       }

@@ -7899,7 +7877,7 @@ namespace Microsoft.Dafny
       }

       if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {

         // We could complain about the syntactic omission of constructors:

-        //   Error(expr, "match expression does not cover all constructors");

+        //   reporter.Error(MessageSource.Resolver, expr, "match expression does not cover all constructors");

         // but instead we let the verifier do a semantic check.

         // So, for now, record the missing constructors:

         foreach (var ctr in dtd.Ctors) {

@@ -8447,7 +8425,7 @@ namespace Microsoft.Dafny
           receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);

         } else {

           if (!scope.AllowInstance) {

-            Error(expr.tok, "'this' is not allowed in a 'static' context");

+            reporter.Error(MessageSource.Resolver, expr.tok, "'this' is not allowed in a 'static' context");

             // nevertheless, set "receiver" to a value so we can continue resolution

           }

           receiver = new ImplicitThisExpr(expr.tok);

@@ -8473,7 +8451,7 @@ namespace Microsoft.Dafny
         // ----- 3. static member of the enclosing module

         Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default

         if (ReallyAmbiguousThing(ref member)) {

-          Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());

+          reporter.Error(MessageSource.Resolver, expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());

         } else {

           var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);

           r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);

@@ -8749,7 +8727,7 @@ namespace Microsoft.Dafny
           // ----- 1. static member of the specified module

           Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default

           if (ReallyAmbiguousThing(ref member)) {

-            Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());

+            reporter.Error(MessageSource.Resolver, expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());

           } else {

             var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);

             r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);

@@ -9375,136 +9353,148 @@ namespace Microsoft.Dafny
         expr = polarity ? Expression.CreateAnd(c, expr) : Expression.CreateImplies(c, expr);

       }

       for (int j = 0; j < bvars.Count; j++) {

-        var bv = bvars[j];

-        var bounds = new List<ComprehensionExpr.BoundedPool>();

-        if (bv.Type.IsBoolType) {

-          // easy

-          bounds.Add(new ComprehensionExpr.BoolBoundedPool());

-        } else {

-          bool foundBoundsForBv = false;

-          if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) {

-            bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

-            foundBoundsForBv = true;

+        VT bv;

+        List<ComprehensionExpr.BoundedPool> bounds;

+        foundError = DiscoverAuxSingle<VT>(bvars, expr, polarity, returnAllBounds, true, allowAnyIntegers, missingBounds, foundError, j, out bv, out bounds);

+        if (!returnAllBounds && bounds.Count > 1) {

+          var best = ComprehensionExpr.BoundedPool.GetBest(bounds);

+          bounds = new List<ComprehensionExpr.BoundedPool>() { best };

+        }

+

+        allBounds.Add(new Tuple<VT, List<ComprehensionExpr.BoundedPool>>(bv, bounds));

+      }

+      return foundError ? null : allBounds;

+    }

+

+    private static bool DiscoverAuxSingle<VT>(List<VT> bvars, Expression expr, bool polarity, bool allowPartialBounds, bool returnAllBounds, bool allowAnyIntegers, List<VT> missingBounds, bool foundError, int j, out VT bv, out List<ComprehensionExpr.BoundedPool> bounds) where VT : IVariable {

+      bv = bvars[j];

+      bounds = new List<ComprehensionExpr.BoundedPool>();

+      if (bv.Type.IsBoolType) {

+        // easy

+        bounds.Add(new ComprehensionExpr.BoolBoundedPool());

+      } else {

+        bool foundBoundsForBv = false;

+        if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) {

+          bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

+          foundBoundsForBv = true;

+        }

+        // Go through the conjuncts of the range expression to look for bounds.

+        Expression lowerBound = null;

+        Expression upperBound = null;

+        if ((allowPartialBounds || returnAllBounds) && lowerBound != null) {

+          bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

+          lowerBound = null;

+          foundBoundsForBv = true;

+        }

+        foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {

+          var c = conjunct as BinaryExpr;

+          if (c == null) {

+            goto CHECK_NEXT_CONJUNCT;

+          }

+          var e0 = c.E0;

+          var e1 = c.E1;

+          int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);

+          if (whereIsBv < 0) {

+            goto CHECK_NEXT_CONJUNCT;

+          }

+          switch (c.ResolvedOp) {

+            case BinaryExpr.ResolvedOpcode.InSet:

+              if (whereIsBv == 0) {

+                bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

+                foundBoundsForBv = true;

+                if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+              }

+              break;

+            case BinaryExpr.ResolvedOpcode.Subset:

+              if (returnAllBounds) {

+                if (whereIsBv == 0) {

+                  bounds.Add(new ComprehensionExpr.SubSetBoundedPool(e1));

+                } else {

+                  bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(e0));

+                }

+                foundBoundsForBv = true;

+              }

+              break;

+            case BinaryExpr.ResolvedOpcode.InMultiSet:

+              if (whereIsBv == 0) {

+                bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

+                foundBoundsForBv = true;

+                if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+              }

+              break;

+            case BinaryExpr.ResolvedOpcode.InSeq:

+              if (whereIsBv == 0) {

+                bounds.Add(new ComprehensionExpr.SeqBoundedPool(e1));

+                foundBoundsForBv = true;

+                if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+              }

+              break;

+            case BinaryExpr.ResolvedOpcode.InMap:

+              if (whereIsBv == 0 && e1.Type.AsMapType.Finite) {

+                bounds.Add(new ComprehensionExpr.MapBoundedPool(e1));

+                foundBoundsForBv = true;

+                if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+              }

+              break;

+            case BinaryExpr.ResolvedOpcode.EqCommon:

+              if (bv.Type is IntType) {

+                var otherOperand = whereIsBv == 0 ? e1 : e0;

+                bounds.Add(new ComprehensionExpr.IntBoundedPool(otherOperand, Expression.CreateIncrement(otherOperand, 1)));

+                foundBoundsForBv = true;

+                if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+              } else if (returnAllBounds && bv.Type is SetType) {

+                var otherOperand = whereIsBv == 0 ? e1 : e0;

+                bounds.Add(new ComprehensionExpr.SubSetBoundedPool(otherOperand));

+                foundBoundsForBv = true;

+              }

+              break;

+            case BinaryExpr.ResolvedOpcode.Gt:

+            case BinaryExpr.ResolvedOpcode.Ge:

+              Contract.Assert(false); throw new cce.UnreachableException();  // promised by postconditions of NormalizedConjunct

+            case BinaryExpr.ResolvedOpcode.Lt:

+              if (e0.Type.IsNumericBased(Type.NumericPersuation.Int)) {

+                if (whereIsBv == 0 && upperBound == null) {

+                  upperBound = e1;  // bv < E

+                } else if (whereIsBv == 1 && lowerBound == null) {

+                  lowerBound = Expression.CreateIncrement(e0, 1);  // E < bv

+                }

+              }

+              break;

+            case BinaryExpr.ResolvedOpcode.Le:

+              if (e0.Type.IsNumericBased(Type.NumericPersuation.Int)) {

+                if (whereIsBv == 0 && upperBound == null) {

+                  upperBound = Expression.CreateIncrement(e1, 1);  // bv <= E

+                } else if (whereIsBv == 1 && lowerBound == null) {

+                  lowerBound = e0;  // E <= bv

+                }

+              }

+              break;

+            default:

+              break;

           }

-          // Go through the conjuncts of the range expression to look for bounds.

-          Expression lowerBound = null;

-          Expression upperBound = null;

-          if (returnAllBounds && lowerBound != null) {

+          if ((lowerBound != null && upperBound != null) ||

+              (allowPartialBounds && (lowerBound != null || upperBound != null))) {

+            // we have found two halves (or, in the case of returnAllBounds, we have found some bound)

             bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

             lowerBound = null;

+            upperBound = null;

             foundBoundsForBv = true;

+            if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

           }

-          foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {

-            var c = conjunct as BinaryExpr;

-            if (c == null) {

-              goto CHECK_NEXT_CONJUNCT;

-            }

-            var e0 = c.E0;

-            var e1 = c.E1;

-            int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);

-            if (whereIsBv < 0) {

-              goto CHECK_NEXT_CONJUNCT;

-            }

-            switch (c.ResolvedOp) {

-              case BinaryExpr.ResolvedOpcode.InSet:

-                if (whereIsBv == 0) {

-                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

-                  foundBoundsForBv = true;

-                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-                }

-                break;

-              case BinaryExpr.ResolvedOpcode.Subset:

-                if (returnAllBounds) {

-                  if (whereIsBv == 0) {

-                    bounds.Add(new ComprehensionExpr.SubSetBoundedPool(e1));

-                  } else {

-                    bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(e0));

-                  }

-                  foundBoundsForBv = true;

-                }

-                break;

-              case BinaryExpr.ResolvedOpcode.InMultiSet:

-                if (whereIsBv == 0) {

-                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

-                  foundBoundsForBv = true;

-                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-                }

-                break;

-              case BinaryExpr.ResolvedOpcode.InSeq:

-                if (whereIsBv == 0) {

-                  bounds.Add(new ComprehensionExpr.SeqBoundedPool(e1));

-                  foundBoundsForBv = true;

-                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-                }

-                break;

-              case BinaryExpr.ResolvedOpcode.InMap:

-                if (whereIsBv == 0 && e1.Type.AsMapType.Finite) {

-                  bounds.Add(new ComprehensionExpr.MapBoundedPool(e1));

-                  foundBoundsForBv = true;

-                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-                }

-                break;

-              case BinaryExpr.ResolvedOpcode.EqCommon:

-                if (bv.Type is IntType) {

-                  var otherOperand = whereIsBv == 0 ? e1 : e0;

-                  bounds.Add(new ComprehensionExpr.IntBoundedPool(otherOperand, Expression.CreateIncrement(otherOperand, 1)));

-                  foundBoundsForBv = true;

-                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-                } else if (returnAllBounds && bv.Type is SetType) {

-                  var otherOperand = whereIsBv == 0 ? e1 : e0;

-                  bounds.Add(new ComprehensionExpr.SubSetBoundedPool(otherOperand));

-                  foundBoundsForBv = true;

-                }

-                break;

-              case BinaryExpr.ResolvedOpcode.Gt:

-              case BinaryExpr.ResolvedOpcode.Ge:

-                Contract.Assert(false); throw new cce.UnreachableException();  // promised by postconditions of NormalizedConjunct

-              case BinaryExpr.ResolvedOpcode.Lt:

-                if (e0.Type.IsNumericBased(Type.NumericPersuation.Int)) {

-                  if (whereIsBv == 0 && upperBound == null) {

-                    upperBound = e1;  // bv < E

-                  } else if (whereIsBv == 1 && lowerBound == null) {

-                    lowerBound = Expression.CreateIncrement(e0, 1);  // E < bv

-                  }

-                }

-                break;

-              case BinaryExpr.ResolvedOpcode.Le:

-                if (e0.Type.IsNumericBased(Type.NumericPersuation.Int)) {

-                  if (whereIsBv == 0 && upperBound == null) {

-                    upperBound = Expression.CreateIncrement(e1, 1);  // bv <= E

-                  } else if (whereIsBv == 1 && lowerBound == null) {

-                    lowerBound = e0;  // E <= bv

-                  }

-                }

-                break;

-              default:

-                break;

-            }

-            if ((lowerBound != null && upperBound != null) ||

-                (returnAllBounds && (lowerBound != null || upperBound != null))) {

-              // we have found two halves (or, in the case of returnAllBounds, we have found some bound)

-              bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

-              lowerBound = null;

-              upperBound = null;

-              foundBoundsForBv = true;

-              if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-            }

-          CHECK_NEXT_CONJUNCT: ;

-          }

-          if (!foundBoundsForBv) {

-            // we have checked every conjunct in the range expression and still have not discovered good bounds

-            if (allowAnyIntegers && bv.Type is IntType) {

-              bounds.Add(new AssignSuchThatStmt.WiggleWaggleBound());

-            } else {

-              missingBounds.Add(bv);  // record failing bound variable

-              foundError = true;

-            }

+        CHECK_NEXT_CONJUNCT: ;

+        }

+        if (!foundBoundsForBv) {

+          // we have checked every conjunct in the range expression and still have not discovered good bounds

+          if (allowAnyIntegers && bv.Type is IntType) {

+            bounds.Add(new AssignSuchThatStmt.WiggleWaggleBound());

+          } else {

+            missingBounds.Add(bv);  // record failing bound variable

+            foundError = true;

           }

         }

-      CHECK_NEXT_BOUND_VARIABLE: ;  // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)

-      allBounds.Add(new Tuple<VT, List<ComprehensionExpr.BoundedPool>>(bv, bounds));

       }

-      return foundError ? null : allBounds;

+    CHECK_NEXT_BOUND_VARIABLE: ;  // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)

+      return foundError;

     }

 

     static Expression TypeConstraint(IVariable bv, Type ty, ErrorReporter reporter) {

@@ -9777,7 +9767,6 @@ namespace Microsoft.Dafny
 

       if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

-

         return new HashSet<IVariable>() { e.Var };

 

       } else if (expr is QuantifierExpr) {

@@ -10378,7 +10367,7 @@ namespace Microsoft.Dafny
             // this call is disqualified from being a co-call, because it has a postcondition

             // (a postcondition could be allowed, as long as it does not get to be used with

             // co-recursive calls, because that could be unsound; for example, consider

-            // "ensures false;")

+            // "ensures false")

             if (!dealsWithCodatatypes) {

               e.CoCall = FunctionCallExpr.CoCallResolution.No;

             } else {

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index b6409b96..83f49a12 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -1290,6 +1290,347 @@ namespace Microsoft.Dafny
       return new AutoGeneratedToken(tok);

     }

   }

+

+  // ===========================================================================================

+

+  public class InductionRewriter : IRewriter {

+    internal InductionRewriter(ErrorReporter reporter) : base(reporter) {

+      Contract.Requires(reporter != null);

+    }

+

+    internal override void PostCyclicityResolve(ModuleDefinition m) {

+      if (DafnyOptions.O.Induction == 0) {

+        // Don't bother inferring :induction attributes.  This will also have the effect of not warning about malformed :induction attributes

+      } else {

+        foreach (var decl in m.TopLevelDecls) {

+          if (decl is ClassDecl) {

+            var cl = (ClassDecl)decl;

+            foreach (var member in cl.Members) {

+              if (member is FixpointLemma) {

+                var method = (FixpointLemma)member;

+                ProcessMethodExpressions(method);

+                ComputeLemmaInduction(method.PrefixLemma);

+                ProcessMethodExpressions(method.PrefixLemma);

+              } else if (member is Method) {

+                var method = (Method)member;

+                ComputeLemmaInduction(method);

+                ProcessMethodExpressions(method);

+              } else if (member is FixpointPredicate) {

+                var function = (FixpointPredicate)member;

+                ProcessFunctionExpressions(function);

+                ProcessFunctionExpressions(function.PrefixPredicate);

+              } else if (member is Function) {

+                var function = (Function)member;

+                ProcessFunctionExpressions(function);

+              }

+            }

+          } else if (decl is NewtypeDecl) {

+            var nt = (NewtypeDecl)decl;

+            if (nt.Constraint != null) {

+              var visitor = new Induction_Visitor(this);

+              visitor.Visit(nt.Constraint);

+            }

+          }

+        }

+      }

+    }

+

+    void ProcessMethodExpressions(Method method) {

+      Contract.Requires(method != null);

+      var visitor = new Induction_Visitor(this);

+      method.Req.ForEach(mfe => visitor.Visit(mfe.E));

+      method.Ens.ForEach(mfe => visitor.Visit(mfe.E));

+      if (method.Body != null) {

+        visitor.Visit(method.Body);

+      }

+    }

+

+    void ProcessFunctionExpressions(Function function) {

+      Contract.Requires(function != null);

+      var visitor = new Induction_Visitor(this);

+      function.Req.ForEach(visitor.Visit);

+      function.Ens.ForEach(visitor.Visit);

+      if (function.Body != null) {

+        visitor.Visit(function.Body);

+      }

+    }

+

+    void ComputeLemmaInduction(Method method) {

+      Contract.Requires(method != null);

+      if (method.Body != null && method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 && !(method is FixpointLemma)) {

+        var specs = new List<Expression>();

+        method.Req.ForEach(mfe => specs.Add(mfe.E));

+        method.Ens.ForEach(mfe => specs.Add(mfe.E));

+        ComputeInductionVariables(method.tok, method.Ins, specs, method, ref method.Attributes);

+      }

+    }

+

+    void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, List<Expression> searchExprs, Method lemma, ref Attributes attributes) where VarType : class, IVariable {

+      Contract.Requires(tok != null);

+      Contract.Requires(boundVars != null);

+      Contract.Requires(searchExprs != null);

+      Contract.Requires(DafnyOptions.O.Induction != 0);

+

+      var args = Attributes.FindExpressions(attributes, "induction");  // we only look at the first one we find, since it overrides any other ones

+      if (args == null) {

+        if (DafnyOptions.O.Induction < 2) {

+          // No explicit induction variables and we're asked not to infer anything, so we're done

+          return;

+        } else if (DafnyOptions.O.Induction == 2 && lemma != null) {

+          // We're asked to infer induction variables only for quantifiers, not for lemmas

+          return;

+        }

+        // GO INFER below (only select boundVars)

+      } else if (args.Count == 0) {

+        // {:induction} is treated the same as {:induction true}, which says to automatically infer induction variables

+        // GO INFER below (all boundVars)

+      } else if (args.Count == 1 && args[0] is LiteralExpr && ((LiteralExpr)args[0]).Value is bool) {

+        // {:induction false} or {:induction true}

+        if (!(bool)((LiteralExpr)args[0]).Value) {

+          // we're told not to infer anything

+          return;

+        }

+        // GO INFER below (all boundVars)

+      } else {

+        // Here, we're expecting the arguments to {:induction args} to be a sublist of "boundVars".

+        var goodArguments = new List<Expression>();

+        var i = 0;

+        foreach (var arg in args) {

+          var ie = arg.Resolved as IdentifierExpr;

+          if (ie != null) {

+            var j = boundVars.FindIndex(i, v => v == ie.Var);

+            if (i <= j) {

+              goodArguments.Add(ie);

+              i = j;

+              continue;

+            }

+            if (0 <= boundVars.FindIndex(v => v == ie.Var)) {

+              reporter.Warning(MessageSource.Rewriter, arg.tok, "{0}s given as :induction arguments must be given in the same order as in the {1}; ignoring attribute",

+                lemma != null ? "lemma parameter" : "bound variable", lemma != null ? "lemma" : "quantifier");

+              return;

+            }

+          }

+          reporter.Warning(MessageSource.Rewriter, arg.tok, "invalid :induction attribute argument; expected {0}{1}; ignoring attribute",

+            i == 0 ? "'false' or 'true' or " : "",

+            lemma != null ? "lemma parameter" : "bound variable");

+          return;

+        }

+        // The argument list was legal, so let's use it for the _induction attribute

+        attributes = new Attributes("_induction", goodArguments, attributes);

+        return;

+      }

+

+      // Okay, here we go, coming up with good induction setting for the given situation

+      var inductionVariables = new List<Expression>();

+      foreach (IVariable n in boundVars) {

+        if (!n.Type.IsTypeParameter && (args != null || searchExprs.Exists(expr => VarOccursInArgumentToRecursiveFunction(expr, n)))) {

+          inductionVariables.Add(new IdentifierExpr(n));

+        }

+      }

+      if (inductionVariables.Count != 0) {

+        // We found something usable, so let's record that in an attribute

+        attributes = new Attributes("_induction", inductionVariables, attributes);

+        // And since we're inferring something, let's also report that in a hover text.

+        var s = Printer.OneAttributeToString(attributes, "induction");

+        if (lemma is PrefixLemma) {

+          s = lemma.Name + " " + s;

+        }

+        reporter.Info(MessageSource.Rewriter, tok, s);

+      }

+    }

+    class Induction_Visitor : BottomUpVisitor

+    {

+      readonly InductionRewriter IndRewriter;

+      public Induction_Visitor(InductionRewriter inductionRewriter) {

+        Contract.Requires(inductionRewriter != null);

+        IndRewriter = inductionRewriter;

+      }

+      protected override void VisitOneExpr(Expression expr) {

+        var q = expr as QuantifierExpr;

+        if (q != null && q.SplitQuantifier == null) {

+          IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List<Expression>() { q.LogicalBody() }, null, ref q.Attributes);

+        }

+      }

+      void VisitInductionStmt(Statement stmt) {

+        Contract.Requires(stmt != null);

+        // visit a selection of subexpressions

+        if (stmt is AssertStmt) {

+          var s = (AssertStmt)stmt;

+          Visit(s.Expr);

+        }

+        // recursively visit all substatements

+        foreach (var s in stmt.SubStatements) {

+          VisitInductionStmt(s);

+        }

+      }

+    }

+

+    /// <summary>

+    /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'.

+    /// More precisely:

+    ///   DafnyInductionHeuristic      Return 'true'

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

+    ///        0                       always

+    ///        1    if 'n' occurs as   any subexpression (of 'expr')

+    ///        2    if 'n' occurs as   any subexpression of          any index argument of an array/sequence select expression or any                       argument to a recursive function

+    ///        3    if 'n' occurs as   a prominent subexpression of  any index argument of an array/sequence select expression or any                       argument to a recursive function

+    ///        4    if 'n' occurs as   any subexpression of                                                                       any                       argument to a recursive function

+    ///        5    if 'n' occurs as   a prominent subexpression of                                                               any                       argument to a recursive function

+    ///        6    if 'n' occurs as   a prominent subexpression of                                                               any decreases-influencing argument to a recursive function

+    /// Parameter 'n' is allowed to be a ThisSurrogate.

+    /// </summary>

+    public static bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {

+      switch (DafnyOptions.O.InductionHeuristic) {

+        case 0: return true;

+        case 1: return Translator.ContainsFreeVariable(expr, false, n);

+        default: return VarOccursInArgumentToRecursiveFunction(expr, n, false);

+      }

+    }

+

+    /// <summary>

+    /// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or

+    /// not 'expr' has prominent status in its context.

+    /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).

+    /// Parameter 'n' is allowed to be a ThisSurrogate.

+    /// </summary>

+    static bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, bool exprIsProminent) {

+      Contract.Requires(expr != null);

+      Contract.Requires(n != null);

+

+      // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.

+      var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;

+

+      if (expr is IdentifierExpr) {

+        var e = (IdentifierExpr)expr;

+        return exprIsProminent && e.Var == n;

+      } else if (expr is SeqSelectExpr) {

+        var e = (SeqSelectExpr)expr;

+        var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;

+        return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) ||  // this subexpression does not acquire "prominent" status

+          (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) ||  // this one does (unless arrays/sequences are excluded)

+          (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q));    // ditto

+      } else if (expr is MultiSelectExpr) {

+        var e = (MultiSelectExpr)expr;

+        var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;

+        return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) ||

+          e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));

+      } else if (expr is FunctionCallExpr) {

+        var e = (FunctionCallExpr)expr;

+        // For recursive functions:  arguments are "prominent"

+        // For non-recursive function:  arguments are "prominent" if the call is

+        var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes;

+        var decr = e.Function.Decreases.Expressions;

+        bool variantArgument;

+        if (DafnyOptions.O.InductionHeuristic < 6) {

+          variantArgument = rec;

+        } else {

+          // The receiver is considered to be "variant" if the function is recursive and the receiver participates

+          // in the effective decreases clause of the function.  The receiver participates if it's a free variable

+          // of a term in the explicit decreases clause.

+          variantArgument = rec && decr.Exists(ee => Translator.ContainsFreeVariable(ee, true, null));

+        }

+        if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument || subExprIsProminent)) {

+          return true;

+        }

+        Contract.Assert(e.Function.Formals.Count == e.Args.Count);

+        for (int i = 0; i < e.Function.Formals.Count; i++) {

+          var f = e.Function.Formals[i];

+          var exp = e.Args[i];

+          if (DafnyOptions.O.InductionHeuristic < 6) {

+            variantArgument = rec;

+          } else if (rec) {

+            // The argument position is considered to be "variant" if the function is recursive and...

+            // ... it has something to do with why the callee is well-founded, which happens when...

+            if (f is ImplicitFormal) {

+              // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or

+              variantArgument = true;

+            } else if (decr.Exists(ee => Translator.ContainsFreeVariable(ee, false, f))) {

+              // ... it participates in the effective decreases clause of the function, which happens when it is

+              // a free variable of a term in the explicit decreases clause, or

+              variantArgument = true;

+            } else {

+              // ... the callee is a prefix predicate.

+              variantArgument = true;

+            }

+          }

+          if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) {

+            return true;

+          }

+        }

+        return false;

+      } else if (expr is TernaryExpr) {

+        var e = (TernaryExpr)expr;

+        switch (e.Op) {

+          case TernaryExpr.Opcode.PrefixEqOp:

+          case TernaryExpr.Opcode.PrefixNeqOp:

+            return VarOccursInArgumentToRecursiveFunction(e.E0, n, true) ||

+              VarOccursInArgumentToRecursiveFunction(e.E1, n, subExprIsProminent) ||

+              VarOccursInArgumentToRecursiveFunction(e.E2, n, subExprIsProminent);

+          default:

+            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected ternary expression

+        }

+      } else if (expr is DatatypeValue) {

+        var e = (DatatypeValue)expr;

+        var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype

+        return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));

+      } else if (expr is UnaryExpr) {

+        var e = (UnaryExpr)expr;

+        // both Not and SeqLength preserve prominence

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);

+      } else if (expr is BinaryExpr) {

+        var e = (BinaryExpr)expr;

+        bool q;

+        switch (e.ResolvedOp) {

+          case BinaryExpr.ResolvedOpcode.Add:

+          case BinaryExpr.ResolvedOpcode.Sub:

+          case BinaryExpr.ResolvedOpcode.Mul:

+          case BinaryExpr.ResolvedOpcode.Div:

+          case BinaryExpr.ResolvedOpcode.Mod:

+          case BinaryExpr.ResolvedOpcode.Union:

+          case BinaryExpr.ResolvedOpcode.Intersection:

+          case BinaryExpr.ResolvedOpcode.SetDifference:

+          case BinaryExpr.ResolvedOpcode.Concat:

+            // these operators preserve prominence

+            q = exprIsProminent;

+            break;

+          default:

+            // whereas all other binary operators do not

+            q = subExprIsProminent;

+            break;

+        }

+        return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||

+          VarOccursInArgumentToRecursiveFunction(e.E1, n, q);

+      } else if (expr is StmtExpr) {

+        var e = (StmtExpr)expr;

+        // ignore the statement

+        return VarOccursInArgumentToRecursiveFunction(e.E, n);

+

+      } else if (expr is ITEExpr) {

+        var e = (ITEExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) ||  // test is not "prominent"

+          VarOccursInArgumentToRecursiveFunction(e.Thn, n, exprIsProminent) ||  // but the two branches are

+          VarOccursInArgumentToRecursiveFunction(e.Els, n, exprIsProminent);

+      } else if (expr is OldExpr ||

+                 expr is ConcreteSyntaxExpression ||

+                 expr is BoxingCastExpr ||

+                 expr is UnboxingCastExpr) {

+        foreach (var exp in expr.SubExpressions) {

+          if (VarOccursInArgumentToRecursiveFunction(exp, n, exprIsProminent)) {  // maintain prominence

+            return true;

+          }

+        }

+        return false;

+      } else {

+        // in all other cases, reset the prominence status and recurse on the subexpressions

+        foreach (var exp in expr.SubExpressions) {

+          if (VarOccursInArgumentToRecursiveFunction(exp, n, subExprIsProminent)) {

+            return true;

+          }

+        }

+        return false;

+      }

+    }

+  }

 }

 

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 50324002..23c0c3f6 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -93,12 +93,10 @@ namespace Microsoft.Dafny {
   }

 

   public class Translator {

-    readonly ErrorReporter reporter;

+    ErrorReporter reporter;

 

     [NotDelayed]

     public Translator(ErrorReporter reporter) {

-      Contract.Requires(reporter != null);

-      

       this.reporter = reporter;

       InsertChecksums = 0 < CommandLineOptions.Clo.VerifySnapshots;

       Bpl.Program boogieProgram = ReadPrelude();

@@ -2760,126 +2758,100 @@ namespace Microsoft.Dafny {
 

       Bpl.StmtList stmts;

       if (!wellformednessProc) {

-        if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is FixpointLemma)) {

-          var posts = new List<Expression>();

-          m.Ens.ForEach(mfe => posts.Add(mfe.E));

-          var allIns = new List<Formal>();

-          if (!m.IsStatic) {

-            allIns.Add(new ThisSurrogate(m.tok, Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass)));

-          }

-          allIns.AddRange(m.Ins);

-          var inductionVars = ApplyInduction(allIns, m.Attributes, posts, delegate(System.IO.TextWriter wr) { wr.Write(m.FullName); });

-          if (inductionVars.Count != 0) {

-            // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns this,y.

-            // Also, let Pre be the precondition and VF be the decreases clause.

-            // Then, insert into the method body what amounts to:

-            //     assume case-analysis-on-parameter[[ y' ]];

-            //     forall (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {

-            //       this'.M(x, y');

-            //     }

-            // Generate bound variables for the forall statement, and a substitution for the Pre and VF

-

-            // assume case-analysis-on-parameter[[ y' ]];

-            foreach (var inFormal in m.Ins) {

-              var dt = inFormal.Type.AsDatatype;

-              if (dt != null) {

-                var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool));

-                var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type));

-                builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List<Bpl.Expr> { f })));

-              }

-            }

-

-            var parBoundVars = new List<BoundVar>();

-            Expression receiverReplacement = null;

-            var substMap = new Dictionary<IVariable, Expression>();

-            foreach (var iv in inductionVars) {

-              BoundVar bv;

-              IdentifierExpr ie;

-              CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie);

-              parBoundVars.Add(bv);

-              if (iv is ThisSurrogate) {

-                Contract.Assert(receiverReplacement == null && substMap.Count == 0);  // the receiver comes first, if at all

-                receiverReplacement = ie;

-              } else {

-                substMap.Add(iv, ie);

-              }

-            }

+        var inductionVars = ApplyInduction(m.Ins, m.Attributes);

+        if (inductionVars.Count != 0) {

+          // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns y.

+          // Also, let Pre be the precondition and VF be the decreases clause.

+          // Then, insert into the method body what amounts to:

+          //     assume case-analysis-on-parameter[[ y' ]];

+          //     forall (y' | Pre(this, x, y') && VF(this, x, y') << VF(this, x, y)) {

+          //       this.M(x, y');

+          //     }

+          // Generate bound variables for the forall statement, and a substitution for the Pre and VF

+

+          // assume case-analysis-on-parameter[[ y' ]];

+          foreach (var inFormal in m.Ins) {

+            var dt = inFormal.Type.AsDatatype;

+            if (dt != null) {

+              var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool));

+              var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type));

+              builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List<Bpl.Expr> { f })));

+            }

+          }

+

+          var parBoundVars = new List<BoundVar>();

+          var substMap = new Dictionary<IVariable, Expression>();

+          foreach (var iv in inductionVars) {

+            BoundVar bv;

+            IdentifierExpr ie;

+            CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie);

+            parBoundVars.Add(bv);

+            substMap.Add(iv, ie);

+          }

 

 

-            // Generate a CallStmt for the recursive call

-            Expression recursiveCallReceiver;

-            if (receiverReplacement != null) {

-              recursiveCallReceiver = receiverReplacement;

-            } else if (m.IsStatic) {

-              recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass, true);  // this also resolves it

+          // Generate a CallStmt for the recursive call

+          Expression recursiveCallReceiver;

+          if (m.IsStatic) {

+            recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass, true);  // this also resolves it

+          } else {

+            recursiveCallReceiver = new ImplicitThisExpr(m.tok);

+            recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass);  // resolve here

+          }

+          var recursiveCallArgs = new List<Expression>();

+          foreach (var inFormal in m.Ins) {

+            Expression inE;

+            if (substMap.TryGetValue(inFormal, out inE)) {

+              recursiveCallArgs.Add(inE);

             } else {

-              recursiveCallReceiver = new ImplicitThisExpr(m.tok);

-              recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass);  // resolve here

-            }

-            var recursiveCallArgs = new List<Expression>();

-            foreach (var inFormal in m.Ins) {

-              Expression inE;

-              if (substMap.TryGetValue(inFormal, out inE)) {

-                recursiveCallArgs.Add(inE);

-              } else {

-                var ie = new IdentifierExpr(inFormal.tok, inFormal.Name);

-                ie.Var = inFormal;  // resolve here

-                ie.Type = inFormal.Type;  // resolve here

-                recursiveCallArgs.Add(ie);

-              }

-            }

-            var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name);

-            methodSel.Member = m;  // resolve here

-            methodSel.TypeApplication = new List<Type>();

-            methodSel.TypeApplication.AddRange(recursiveCallReceiver.Type.TypeArgs);

-            m.TypeArgs.ForEach(tp => methodSel.TypeApplication.Add(new UserDefinedType(tp)));

-            methodSel.Type = new InferredTypeProxy();  // this is the last step in resolving 'methodSel'

-            var recursiveCall = new CallStmt(m.tok, m.tok, new List<Expression>(), methodSel, recursiveCallArgs);

-            recursiveCall.IsGhost = m.IsGhost;  // resolve here

-

-            Expression parRange = new LiteralExpr(m.tok, true);

-            parRange.Type = Type.Bool;  // resolve here

-            if (receiverReplacement != null) {

-              // add "this' != null" to the range

-              var nil = new LiteralExpr(receiverReplacement.tok);

-              nil.Type = receiverReplacement.Type;  // resolve here

-              var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil);

-              neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon;  // resolve here

-              neqNull.Type = Type.Bool;  // resolve here

-              parRange = Expression.CreateAnd(parRange, neqNull);

-            }

-            foreach (var pre in m.Req) {

-              if (!pre.IsFree) {

-                parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverReplacement, substMap));

-              }

-            }

-            // construct an expression (generator) for:  VF' << VF

-            ExpressionConverter decrCheck = delegate(Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {

-              var decrToks = new List<IToken>();

-              var decrTypes = new List<Type>();

-              var decrCallee = new List<Expr>();

-              var decrCaller = new List<Expr>();

-              foreach (var ee in m.Decreases.Expressions) {

-                decrToks.Add(ee.tok);

-                decrTypes.Add(ee.Type.NormalizeExpand());

-                decrCaller.Add(exprTran.TrExpr(ee));

-                Expression es = Substitute(ee, receiverReplacement, substMap);

-                es = Substitute(es, null, decrSubstMap);

-                decrCallee.Add(exprTran.TrExpr(es));

-              }

-              return DecreasesCheck(decrToks, decrTypes, decrTypes, decrCallee, decrCaller, null, null, false, true);

-            };

+              var ie = new IdentifierExpr(inFormal.tok, inFormal.Name);

+              ie.Var = inFormal;  // resolve here

+              ie.Type = inFormal.Type;  // resolve here

+              recursiveCallArgs.Add(ie);

+            }

+          }

+          var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name);

+          methodSel.Member = m;  // resolve here

+          methodSel.TypeApplication = new List<Type>();

+          methodSel.TypeApplication.AddRange(recursiveCallReceiver.Type.TypeArgs);

+          m.TypeArgs.ForEach(tp => methodSel.TypeApplication.Add(new UserDefinedType(tp)));

+          methodSel.Type = new InferredTypeProxy();  // this is the last step in resolving 'methodSel'

+          var recursiveCall = new CallStmt(m.tok, m.tok, new List<Expression>(), methodSel, recursiveCallArgs);

+          recursiveCall.IsGhost = m.IsGhost;  // resolve here

+

+          Expression parRange = new LiteralExpr(m.tok, true);

+          parRange.Type = Type.Bool;  // resolve here

+          foreach (var pre in m.Req) {

+            if (!pre.IsFree) {

+              parRange = Expression.CreateAnd(parRange, Substitute(pre.E, null, substMap));

+            }

+          }

+          // construct an expression (generator) for:  VF' << VF

+          ExpressionConverter decrCheck = delegate(Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {

+            var decrToks = new List<IToken>();

+            var decrTypes = new List<Type>();

+            var decrCallee = new List<Expr>();

+            var decrCaller = new List<Expr>();

+            foreach (var ee in m.Decreases.Expressions) {

+              decrToks.Add(ee.tok);

+              decrTypes.Add(ee.Type.NormalizeExpand());

+              decrCaller.Add(exprTran.TrExpr(ee));

+              Expression es = Substitute(ee, null, substMap);

+              es = Substitute(es, null, decrSubstMap);

+              decrCallee.Add(exprTran.TrExpr(es));

+            }

+            return DecreasesCheck(decrToks, decrTypes, decrTypes, decrCallee, decrCaller, null, null, false, true);

+          };

 

 #if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE

-            var definedness = new Bpl.StmtListBuilder();

-            var exporter = new Bpl.StmtListBuilder();

-            TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);

-            // All done, so put the two pieces together

-            builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));

+          var definedness = new Bpl.StmtListBuilder();

+          var exporter = new Bpl.StmtListBuilder();

+          TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);

+          // All done, so put the two pieces together

+          builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));

 #else

-            TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);

+          TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);

 #endif

-          }

         }

         // translate the body of the method

         Contract.Assert(m.Body != null);  // follows from method precondition and the if guard

@@ -11554,58 +11526,56 @@ namespace Microsoft.Dafny {
           return TrExpr(((NamedExpr)expr).Body);

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

+          List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);

+          List<Variable> bvars = new List<Variable>();

 

-          if (e.SplitQuantifier != null) {

-            return TrExpr(e.SplitQuantifierExpression);

-          } else {

-            List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);

-            List<Variable> bvars = new List<Variable>();

-

-            var initEtran = this;

-            var bodyEtran = this;

-            bool _scratch = true;

-

-            Bpl.Expr antecedent = Bpl.Expr.True;

-

-            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);

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

-            }

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

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

-              bodyEtran = new ExpressionTranslator(bodyEtran, h);

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

-                antecedent,

-                translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h),

-                translator.HeapSameOrSucc(initEtran.HeapExpr, h)

-              });

-            }

+          var initEtran = this;

+          var bodyEtran = this;

+          bool _scratch = true;

 

-            antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars));

+          Bpl.Expr antecedent = Bpl.Expr.True;

 

-            Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

-            Bpl.Trigger tr = null;

-            var argsEtran = bodyEtran.WithNoLits();

-            foreach (var aa in e.Attributes.AsEnumerable().Where(aa => aa.Name == "trigger")) {

+          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);

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

+          }

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

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

+            bodyEtran = new ExpressionTranslator(bodyEtran, h);

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

+              antecedent,

+              translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h),

+              translator.HeapSameOrSucc(initEtran.HeapExpr, h)

+            });

+          }

+

+          antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars));

+

+          Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

+          Bpl.Trigger tr = null;

+          var argsEtran = bodyEtran.WithNoLits();

+          foreach (var aa in e.Attributes.AsEnumerable()) {

+            if (aa.Name == "trigger") {

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

               foreach (var arg in aa.Args) {

                 tt.Add(argsEtran.TrExpr(arg));

               }

               tr = new Bpl.Trigger(expr.tok, true, tt, tr);

             }

-            if (e.Range != null) {

-              antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range));

-            }

-            Bpl.Expr body = bodyEtran.TrExpr(e.Term);

+          }

+          if (e.Range != null) {

+            antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range));

+          }

+          Bpl.Expr body = bodyEtran.TrExpr(e.Term);

           

-            if (e is ForallExpr) {

-              return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));

-            } else {

-              Contract.Assert(e is ExistsExpr);

-              return new Bpl.ExistsExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body));

-            }

+          if (e is ForallExpr) {

+            return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));

+          } else {

+            Contract.Assert(e is ExistsExpr);

+            return new Bpl.ExistsExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body));

           }

+

         } else if (expr is SetComprehension) {

           var e = (SetComprehension)expr;

           // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))".

@@ -12994,8 +12964,8 @@ namespace Microsoft.Dafny {
         /* NB: only for type arg less quantifiers for now: */

             && ((QuantifierExpr)expr).TypeArgs.Count == 0) {

         var e = (QuantifierExpr)expr;

-        var inductionVariables = ApplyInduction(e);

-        if (apply_induction && 2 <= DafnyOptions.O.Induction && inductionVariables.Count != 0) {

+        var inductionVariables = ApplyInduction(e.BoundVars, e.Attributes);

+        if (apply_induction && inductionVariables.Count != 0) {

           // From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation

           //   (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))

           // For an existential (exists n :: P(n)), it is

@@ -13200,298 +13170,29 @@ namespace Microsoft.Dafny {
       return RefinementToken.IsInherited(expr.tok, currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule);

     }

 

-    List<BoundVar> ApplyInduction(QuantifierExpr e) {

-      Contract.Requires(e.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

-      Contract.Requires(e.TypeArgs.Count == 0);

-      return ApplyInduction(e.BoundVars, e.Attributes, new List<Expression>() { e.LogicalBody() },

-        delegate(System.IO.TextWriter wr) { new Printer(wr).PrintExpression(e, true); });

-    }

-

-    delegate void TracePrinter(System.IO.TextWriter wr);

-

     /// <summary>

     /// Return a subset of "boundVars" (in the order giving in "boundVars") to which to apply induction to,

-    /// according to :induction attributes in "attributes" and heuristically interesting subexpressions of

-    /// "searchExprs".

+    /// according to :_induction attribute in "attributes".

     /// </summary>

-    List<VarType> ApplyInduction<VarType>(List<VarType> boundVars, Attributes attributes, List<Expression> searchExprs, TracePrinter tracePrinter) where VarType : class, IVariable

+    List<VarType> ApplyInduction<VarType>(List<VarType> boundVars, Attributes attributes) where VarType : class, IVariable

     {

       Contract.Requires(boundVars != null);

-      Contract.Requires(searchExprs != null);

-      Contract.Requires(tracePrinter != null);

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

 

-      if (DafnyOptions.O.Induction == 0) {

+      var args = Attributes.FindExpressions(attributes, "_induction");

+      if (args == null) {

         return new List<VarType>();  // don't apply induction

       }

 

-      foreach (var a in attributes.AsEnumerable()) {

-        if (a.Name == "induction") {

-          // Here are the supported forms of the :induction attribute.

-          //    :induction           -- apply induction to all bound variables

-          //    :induction false     -- suppress induction, that is, don't apply it to any bound variable

-          //    :induction L       where L is a list consisting entirely of bound variables:

-          //                         -- apply induction to the specified bound variables

-          //    :induction X       where X is anything else

-          //                         -- treat the same as {:induction}, that is, apply induction to all

-          //                            bound variables

-

-          // Handle {:induction false}

-          if (a.Args.Count == 1) {

-            var arg = a.Args[0] as LiteralExpr;

-            if (arg != null && arg.Value is bool && !(bool)arg.Value) {

-              if (CommandLineOptions.Clo.Trace) {

-                Console.Write("Suppressing automatic induction for: ");

-                tracePrinter(Console.Out);

-                Console.WriteLine();

-              }

-              return new List<VarType>();

-            }

-          }

-

-          // Handle {:induction L}

-          if (a.Args.Count != 0) {

-            // check that all attribute arguments refer to bound variables; otherwise, go to default_form

-            var argsAsVars = new List<VarType>();

-            foreach (var arg in a.Args) {

-              var theArg = arg.Resolved;

-              if (theArg is ThisExpr) {

-                foreach (var bv in boundVars) {

-                  if (bv is ThisSurrogate) {

-                    argsAsVars.Add(bv);

-                    goto TRY_NEXT_ATTRIBUTE_ARGUMENT;

-                  }

-                }

-              } else if (theArg is IdentifierExpr) {

-                var id = (IdentifierExpr)theArg;

-                var bv = id.Var as VarType;

-                if (bv != null && boundVars.Contains(bv)) {

-                  argsAsVars.Add(bv);

-                  goto TRY_NEXT_ATTRIBUTE_ARGUMENT;

-                }

-              }

-              // the attribute argument was not one of the possible induction variables

-              goto USE_DEFAULT_FORM;

-            TRY_NEXT_ATTRIBUTE_ARGUMENT:

-              ;

-            }

-            // so, all attribute arguments are variables; add them to L in the order of the bound variables (not necessarily the order in the attribute)

-            var L = new List<VarType>();

-            foreach (var bv in boundVars) {

-              if (argsAsVars.Contains(bv)) {

-                L.Add(bv);

-              }

-            }

-            if (CommandLineOptions.Clo.Trace) {

-              string sep = "Applying requested induction on ";

-              foreach (var bv in L) {

-                Console.Write("{0}{1}", sep, bv.Name);

-                sep = ", ";

-              }

-              Console.Write(" of: ");

-              tracePrinter(Console.Out);

-              Console.WriteLine();

-            }

-            return L;

-          USE_DEFAULT_FORM: ;

-          }

-

-          // We have the {:induction} case, or something to be treated in the same way

-          if (CommandLineOptions.Clo.Trace) {

-            Console.Write("Applying requested induction on all bound variables of: ");

-            tracePrinter(Console.Out);

-            Console.WriteLine();

-          }

-          return boundVars;

-        }

-      }

-

-      if (DafnyOptions.O.Induction < 2) {

-        return new List<VarType>();  // don't apply induction

-      }

-

-      // consider automatically applying induction

-      var inductionVariables = new List<VarType>();

-      foreach (var n in boundVars) {

-        if (!n.Type.IsTypeParameter && searchExprs.Exists(expr => VarOccursInArgumentToRecursiveFunction(expr, n))) {

-          if (CommandLineOptions.Clo.Trace) {

-            Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);

-            tracePrinter(Console.Out);

-            Console.WriteLine();

-          }

-          inductionVariables.Add(n);

-        }

-      }

-

-      return inductionVariables;

-    }

-

-    /// <summary>

-    /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'.

-    /// More precisely:

-    ///   DafnyInductionHeuristic      Return 'true'

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

-    ///        0                       always

-    ///        1    if 'n' occurs as   any subexpression (of 'expr')

-    ///        2    if 'n' occurs as   any subexpression of          any index argument of an array/sequence select expression or any                       argument to a recursive function

-    ///        3    if 'n' occurs as   a prominent subexpression of  any index argument of an array/sequence select expression or any                       argument to a recursive function

-    ///        4    if 'n' occurs as   any subexpression of                                                                       any                       argument to a recursive function

-    ///        5    if 'n' occurs as   a prominent subexpression of                                                               any                       argument to a recursive function

-    ///        6    if 'n' occurs as   a prominent subexpression of                                                               any decreases-influencing argument to a recursive function

-    /// Parameter 'n' is allowed to be a ThisSurrogate.

-    /// </summary>

-    bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {

-      switch (DafnyOptions.O.InductionHeuristic) {

-        case 0: return true;

-        case 1: return ContainsFreeVariable(expr, false, n);

-        default: return VarOccursInArgumentToRecursiveFunction(expr, n, false);

-      }

-    }

-

-    /// <summary>

-    /// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or

-    /// not 'expr' has prominent status in its context.

-    /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).

-    /// Parameter 'n' is allowed to be a ThisSurrogate.

-    /// </summary>

-    bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, bool exprIsProminent) {

-      Contract.Requires(expr != null);

-      Contract.Requires(n != null);

-

-      // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.

-      var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;

-

-      if (expr is ThisExpr) {

-        return exprIsProminent && n is ThisSurrogate;

-      } else if (expr is IdentifierExpr) {

-        var e = (IdentifierExpr)expr;

-        return exprIsProminent && e.Var == n;

-      } else if (expr is SeqSelectExpr) {

-        var e = (SeqSelectExpr)expr;

-        var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;

-        return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) ||  // this subexpression does not acquire "prominent" status

-          (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) ||  // this one does (unless arrays/sequences are excluded)

-          (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q));    // ditto

-      } else if (expr is MultiSelectExpr) {

-        var e = (MultiSelectExpr)expr;

-        var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;

-        return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) ||

-          e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));

-      } else if (expr is FunctionCallExpr) {

-        var e = (FunctionCallExpr)expr;

-        // For recursive functions:  arguments are "prominent"

-        // For non-recursive function:  arguments are "prominent" if the call is

-        var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes;

-        var decr = e.Function.Decreases.Expressions;

-        bool variantArgument;

-        if (DafnyOptions.O.InductionHeuristic < 6) {

-          variantArgument = rec;

-        } else {

-          // The receiver is considered to be "variant" if the function is recursive and the receiver participates

-          // in the effective decreases clause of the function.  The receiver participates if it's a free variable

-          // of a term in the explicit decreases clause.

-          variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, true, null));

-        }

-        if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument || subExprIsProminent)) {

-          return true;

-        }

-        Contract.Assert(e.Function.Formals.Count == e.Args.Count);

-        for (int i = 0; i < e.Function.Formals.Count; i++) {

-          var f = e.Function.Formals[i];

-          var exp = e.Args[i];

-          if (DafnyOptions.O.InductionHeuristic < 6) {

-            variantArgument = rec;

-          } else if (rec) {

-            // The argument position is considered to be "variant" if the function is recursive and...

-            // ... it has something to do with why the callee is well-founded, which happens when...

-            if (f is ImplicitFormal) {

-              // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or

-              variantArgument = true;

-            } else if (decr.Exists(ee => ContainsFreeVariable(ee, false, f))) {

-              // ... it participates in the effective decreases clause of the function, which happens when it is

-              // a free variable of a term in the explicit decreases clause, or

-              variantArgument = true;

-            } else {

-              // ... the callee is a prefix predicate.

-              variantArgument = true;

-            }

-          }

-          if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) {

-            return true;

-          }

-        }

-        return false;

-      } else if (expr is TernaryExpr) {

-        var e = (TernaryExpr)expr;

-        switch (e.Op) {

-          case TernaryExpr.Opcode.PrefixEqOp:

-          case TernaryExpr.Opcode.PrefixNeqOp:

-            return VarOccursInArgumentToRecursiveFunction(e.E0, n, true) ||

-              VarOccursInArgumentToRecursiveFunction(e.E1, n, subExprIsProminent) ||

-              VarOccursInArgumentToRecursiveFunction(e.E2, n, subExprIsProminent);

-          default:

-            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected ternary expression

-        }

-      } else if (expr is DatatypeValue) {

-        var e = (DatatypeValue)expr;

-        var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype

-        return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));

-      } else if (expr is UnaryExpr) {

-        var e = (UnaryExpr)expr;

-        // both Not and SeqLength preserve prominence

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);

-      } else if (expr is BinaryExpr) {

-        var e = (BinaryExpr)expr;

-        bool q;

-        switch (e.ResolvedOp) {

-          case BinaryExpr.ResolvedOpcode.Add:

-          case BinaryExpr.ResolvedOpcode.Sub:

-          case BinaryExpr.ResolvedOpcode.Mul:

-          case BinaryExpr.ResolvedOpcode.Div:

-          case BinaryExpr.ResolvedOpcode.Mod:

-          case BinaryExpr.ResolvedOpcode.Union:

-          case BinaryExpr.ResolvedOpcode.Intersection:

-          case BinaryExpr.ResolvedOpcode.SetDifference:

-          case BinaryExpr.ResolvedOpcode.Concat:

-            // these operators preserve prominence

-            q = exprIsProminent;

-            break;

-          default:

-            // whereas all other binary operators do not

-            q = subExprIsProminent;

-            break;

-        }

-        return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||

-          VarOccursInArgumentToRecursiveFunction(e.E1, n, q);

-      } else if (expr is StmtExpr) {

-        var e = (StmtExpr)expr;

-        // ignore the statement

-        return VarOccursInArgumentToRecursiveFunction(e.E, n);

-

-      } else if (expr is ITEExpr) {

-        var e = (ITEExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) ||  // test is not "prominent"

-          VarOccursInArgumentToRecursiveFunction(e.Thn, n, exprIsProminent) ||  // but the two branches are

-          VarOccursInArgumentToRecursiveFunction(e.Els, n, exprIsProminent);

-      } else if (expr is OldExpr ||

-                 expr is ConcreteSyntaxExpression ||

-                 expr is BoxingCastExpr ||

-                 expr is UnboxingCastExpr) {

-        foreach (var exp in expr.SubExpressions) {

-          if (VarOccursInArgumentToRecursiveFunction(exp, n, exprIsProminent)) {  // maintain prominence

-            return true;

-          }

-        }

-        return false;

-      } else {

-        // in all other cases, reset the prominence status and recurse on the subexpressions

-        foreach (var exp in expr.SubExpressions) {

-          if (VarOccursInArgumentToRecursiveFunction(exp, n, subExprIsProminent)) {

-            return true;

-          }

-        }

-        return false;

+      var argsAsVars = new List<VarType>();

+      foreach (var arg in args) {

+        // We expect each "arg" to be an IdentifierExpr among "boundVars"

+        var id = (IdentifierExpr)arg;

+        var bv = (VarType)id.Var;

+        Contract.Assume(boundVars.Contains(bv));

+        argsAsVars.Add(bv);

       }

+      return argsAsVars;

     }

 

     IEnumerable<Bpl.Expr> InductionCases(Type ty, Bpl.Expr expr, ExpressionTranslator etran) {

@@ -13538,12 +13239,12 @@ namespace Microsoft.Dafny {
     /// Parameter 'v' is allowed to be a ThisSurrogate, in which case the method return true iff 'this'

     /// occurs in 'expr'.

     /// </summary>

-    static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) {

+    public static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) {

       Contract.Requires(expr != null);

       Contract.Requires(lookForReceiver || v != null);

 

       if (expr is ThisExpr) {

-        return lookForReceiver || v is ThisSurrogate;

+        return lookForReceiver;

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

         return e.Var == v;

diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs
index d6c3f5c7..952f71c5 100644
--- a/Source/DafnyServer/DafnyHelper.cs
+++ b/Source/DafnyServer/DafnyHelper.cs
@@ -62,7 +62,7 @@ namespace Microsoft.Dafny {
     }

 

     private bool Translate() {

-      var translator = new Dafny.Translator(reporter) { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix

+      var translator = new Dafny.Translator(reporter) { InsertChecksums = true, UniqueIdPrefix = fname };

       boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported?

       return true;

     }

diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
index 96254a3d..5bd6e7d5 100644
--- a/Source/DafnyServer/Utilities.cs
+++ b/Source/DafnyServer/Utilities.cs
@@ -53,7 +53,7 @@ namespace Microsoft.Dafny {
         Dafny.DafnyOptions.O.UnicodeOutput = true;

         Dafny.DafnyOptions.O.VerifySnapshots = 2;

         Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);

-        Dafny.DafnyOptions.Clo.Trace = trace;

+        Dafny.DafnyOptions.O.Trace = trace;

       } else {

         throw new ServerException("Invalid command line options");

       }