Merge

41 files changed, 3134 insertions, 2001 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 47c68419..dd65a1f6 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -54,6 +54,15 @@ namespace BytecodeTranslator
       return this.sink.FindOrCreateTypeReference(typeReference);

     }

 

+    private static IMethodDefinition ResolveUnspecializedMethodOrThrow(IMethodReference methodReference) {

+      var resolvedMethod = Sink.Unspecialize(methodReference).ResolvedMethod;

+      if (resolvedMethod == Dummy.Method) { // avoid downstream errors, fail early

+        throw new TranslationException(ExceptionType.UnresolvedMethod, MemberHelper.GetMethodSignature(methodReference, NameFormattingOptions.None));

+      }

+      return resolvedMethod;

+    }

+

+

     #region Constructors

 

     ///// <summary>

@@ -511,12 +520,7 @@ namespace BytecodeTranslator
     /// <param name="methodCall"></param>

     /// <remarks>Stub, This one really needs comments!</remarks>

     public override void TraverseChildren(IMethodCall methodCall) {

-      var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;

-      if (resolvedMethod == Dummy.Method) {

-        throw new TranslationException(

-          ExceptionType.UnresolvedMethod,

-          MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None));

-      }

+      var resolvedMethod = ResolveUnspecializedMethodOrThrow(methodCall.MethodToCall);

 

       Bpl.IToken methodCallToken = methodCall.Token();

 

@@ -707,10 +711,15 @@ namespace BytecodeTranslator
           if (unboxed == null) {

             throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");

           }

-          if (penum.Current.Type is IGenericTypeParameter || penum.Current.Type is IGenericMethodParameter) {

-            Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));

-            toBoxed[unboxed] = boxed;

-            outvars.Add(boxed);

+          if (penum.Current.Type is IGenericParameter) {

+            var boogieType = this.sink.CciTypeToBoogie(penum.Current.Type);

+            if (boogieType == this.sink.Heap.BoxType) {

+              Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));

+              toBoxed[unboxed] = boxed;

+              outvars.Add(boxed);

+            } else {

+              outvars.Add(unboxed);

+            }

           } else {

             outvars.Add(unboxed);

           }

@@ -738,10 +747,15 @@ namespace BytecodeTranslator
         if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

           Bpl.Variable v = this.sink.CreateFreshLocal(methodToCall.ResolvedMethod.Type.ResolvedType);

           Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v);

-          if (resolvedMethod.Type is IGenericTypeParameter || resolvedMethod.Type is IGenericMethodParameter) {

-            Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

-            toBoxed[unboxed] = boxed;

-            outvars.Add(boxed);

+          if (resolvedMethod.Type is IGenericParameter) {

+            var boogieType = this.sink.CciTypeToBoogie(methodToCall.Type);

+            if (boogieType == this.sink.Heap.BoxType) {

+              Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

+              toBoxed[unboxed] = boxed;

+              outvars.Add(boxed);

+            } else {

+              outvars.Add(unboxed);

+            }

           } else {

             outvars.Add(unboxed);

           }

@@ -932,7 +946,8 @@ namespace BytecodeTranslator
     public override void TraverseChildren(ICreateObjectInstance createObjectInstance)

     {

       var ctor = createObjectInstance.MethodToCall;

-      var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;

+      var resolvedMethod = ResolveUnspecializedMethodOrThrow(ctor);

+

       Bpl.IToken token = createObjectInstance.Token();

 

       var a = this.sink.CreateFreshLocal(createObjectInstance.Type);

@@ -974,7 +989,6 @@ namespace BytecodeTranslator
       TranslatedExpressions.Push(Bpl.Expr.Ident(a));

     }

 

-

     public override void TraverseChildren(ICreateArray createArrayInstance)

     {

       Bpl.IToken cloc = createArrayInstance.Token();

@@ -1012,7 +1026,7 @@ namespace BytecodeTranslator
       var a = this.sink.CreateFreshLocal(creationAST.Type);

 

       ITypeDefinition unspecializedType = Microsoft.Cci.MutableContracts.ContractHelper.Unspecialized(type.ResolvedType).ResolvedType;

-      IMethodDefinition unspecializedMethod = Sink.Unspecialize(methodToCall.ResolvedMethod).ResolvedMethod;

+      IMethodDefinition unspecializedMethod = ResolveUnspecializedMethodOrThrow(methodToCall);

       sink.AddDelegate(unspecializedType, unspecializedMethod);

       Bpl.Constant constant = sink.FindOrCreateDelegateMethodConstant(unspecializedMethod);

       Bpl.Expr methodExpr = Bpl.Expr.Ident(constant);

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 4702d5a0..c8300189 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -197,27 +197,35 @@ namespace BytecodeTranslator {
       modules = new List<IModule>();

       var contractExtractors = new Dictionary<IUnit, IContractProvider>();

       var pdbReaders = new Dictionary<IUnit, PdbReader>();

+      #region Load *all* of the assemblies before doing anything else so that they can all vote on unification matters

       foreach (var a in assemblyNames) {

         var module = host.LoadUnitFrom(a) as IModule;

         if (module == null || module == Dummy.Module || module == Dummy.Assembly) {

           Console.WriteLine(a + " is not a PE file containing a CLR module or assembly, or an error occurred when loading it.");

           Console.WriteLine("Skipping it, continuing with other input assemblies");

         }

+        modules.Add(module);

+      }

+      #endregion

+      #region Decompile all of the assemblies

+      var decompiledModules = new List<IModule>();

+      foreach (var m in modules) {

         PdbReader/*?*/ pdbReader = null;

-        string pdbFile = Path.ChangeExtension(module.Location, "pdb");

+        string pdbFile = Path.ChangeExtension(m.Location, "pdb");

         if (File.Exists(pdbFile)) {

           Stream pdbStream = File.OpenRead(pdbFile);

           pdbReader = new PdbReader(pdbStream, host);

         }

-        module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;

+        var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;

         // The decompiler does not turn calls to Assert/Assume into Code Model nodes

-        module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(module);

-

-        host.RegisterAsLatest(module);

-        modules.Add(module);

-        contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));

-        pdbReaders.Add(module, pdbReader);

+        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);

+        decompiledModules.Add(m2);

+        host.RegisterAsLatest(m2);

+        contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));

+        pdbReaders.Add(m2, pdbReader);

       }

+      modules = decompiledModules;

+      #endregion

       #endregion

 

       #region Assemblies to translate (stubs)

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 957b8c38..bcf3ce0b 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -133,9 +133,15 @@ namespace BytecodeTranslator {
         return heap.RefType; // structs are kept on the heap with special rules about assignment

       else if (type.IsEnum)

         return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer

-      else if (type is IGenericTypeParameter || type is IGenericMethodParameter)

+      else if (type is IGenericParameter) {

+        var gp = type as IGenericParameter;

+        if (gp.MustBeReferenceType || gp.MustBeValueType)

+          return heap.RefType;

+        foreach (var c in gp.Constraints){

+          return CciTypeToBoogie(c);

+        }

         return heap.BoxType;

-      else

+      } else

         return heap.RefType;

     }

 

@@ -148,17 +154,19 @@ namespace BytecodeTranslator {
     public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {

       Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

       Bpl.Type t = CciTypeToBoogie(typeReference);

-      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

+      var localName = TranslationHelper.GenerateTempVarName();

+      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, localName, t));

       ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

-      localVarMap.Add(dummy, v);

+      localVarMap.Add(localName, v);

       return v;

     }

 

     public Bpl.Variable CreateFreshLocal(Bpl.Type t) {

       Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

-      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

+      var localName = TranslationHelper.GenerateTempVarName();

+      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, localName, t));

       ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

-      localVarMap.Add(dummy, v);

+      localVarMap.Add(localName, v);

       return v;

     }

 

@@ -182,9 +190,10 @@ namespace BytecodeTranslator {
 

     /// <summary>

     /// State that gets re-initialized per method

+    /// Keys are the mangled names to avoid name clashes.

     /// </summary>

-    private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = null;

-    public Dictionary<ILocalDefinition, Bpl.LocalVariable> LocalVarMap {

+    private Dictionary<string, Bpl.LocalVariable> localVarMap = null;

+    public Dictionary<string, Bpl.LocalVariable> LocalVarMap {

       get { return this.localVarMap; }

     }

     private int localCounter;

@@ -199,11 +208,14 @@ namespace BytecodeTranslator {
       Bpl.LocalVariable v;

       Bpl.IToken tok = local.Token();

       Bpl.Type t = CciTypeToBoogie(local.Type.ResolvedType);

-      if (!localVarMap.TryGetValue(local, out v)) {

-        var name = local.Name.Value;

-        name = TranslationHelper.TurnStringIntoValidIdentifier(name);

+      var name = local.Name.Value;

+      name = TranslationHelper.TurnStringIntoValidIdentifier(name);

+      var typeName = t.ToString();

+      typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);

+      var mangledName = String.Format("{0}_{1}", name, typeName);

+      if (!localVarMap.TryGetValue(mangledName, out v)) {

         v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, t));

-        localVarMap.Add(local, v);

+        localVarMap.Add(mangledName, v);

       }

       return v;

     }

@@ -684,7 +696,15 @@ namespace BytecodeTranslator {
       return procInfo;

     }

 

-    private Dictionary<uint, ProcedureInfo> declaredStructDefaultCtors = new Dictionary<uint, ProcedureInfo>();

+    /// <summary>

+    /// The keys are the mangled names for the ctors. That is avoid generating name conflicts in the translated

+    /// program. This is needed for things like System.Drawing.Rect, which was referenced in both System.Drawing v2

+    /// as well as System.Drawing v4. Since those assemblies are not unified, the two types are distinct, but

+    /// the (generated) name for the default struct ctors clash.

+    /// NB: This means that if there are two different types with the same full name (minus the assembly name),

+    /// then this will implicitly unify them. This could lead to big trouble!

+    /// </summary>

+    private Dictionary<string, ProcedureInfo> declaredStructDefaultCtors = new Dictionary<string, ProcedureInfo>();

     /// <summary>

     /// Struct "creation" (source code that looks like "new S()" for a struct type S) is modeled

     /// by a call to the nullary "ctor" that initializes all of the structs fields to zero-

@@ -699,14 +719,14 @@ namespace BytecodeTranslator {
       Contract.Requires(structType.IsValueType);

 

       ProcedureInfo procAndFormalMap;

-      var key = structType.InternedKey;

-      if (!this.declaredStructDefaultCtors.TryGetValue(key, out procAndFormalMap)) {

-        var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+      var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+      var procName = typename + ".#default_ctor";

+      if (!this.declaredStructDefaultCtors.TryGetValue(procName, out procAndFormalMap)) {

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

         var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

         var invars = new Bpl.Formal[] { selfIn };

-        var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#default_ctor",

+        var proc = new Bpl.Procedure(Bpl.Token.NoToken, procName,

           new Bpl.TypeVariableSeq(),

           new Bpl.VariableSeq(invars),

           new Bpl.VariableSeq(), // out

@@ -716,12 +736,20 @@ namespace BytecodeTranslator {
           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

         procAndFormalMap = new ProcedureInfo(proc, new MethodParameter[0]);

-        this.declaredStructDefaultCtors.Add(key, procAndFormalMap);

+        this.declaredStructDefaultCtors.Add(procName, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

     }

 

-    private Dictionary<uint, ProcedureInfo> declaredStructCopyCtors = new Dictionary<uint, ProcedureInfo>();

+    /// <summary>

+    /// The keys are the mangled names for the ctors. That is avoid generating name conflicts in the translated

+    /// program. This is needed for things like System.Drawing.Rect, which was referenced in both System.Drawing v2

+    /// as well as System.Drawing v4. Since those assemblies are not unified, the two types are distinct, but

+    /// the (generated) name for the default struct ctors clash.

+    /// NB: This means that if there are two different types with the same full name (minus the assembly name),

+    /// then this will implicitly unify them. This could lead to big trouble!

+    /// </summary>

+    private Dictionary<string, ProcedureInfo> declaredStructCopyCtors = new Dictionary<string, ProcedureInfo>();

     private Dictionary<uint, ProcedureInfo> declaredStructEqualityOperators = new Dictionary<uint, ProcedureInfo>();

     /// <summary>

     /// The assignment of one struct value to another is modeled by a method that makes a field-by-field

@@ -736,9 +764,9 @@ namespace BytecodeTranslator {
       Contract.Requires(structType.IsValueType);

 

       ProcedureInfo procAndFormalMap;

-      var key = structType.InternedKey;

-      if (!this.declaredStructCopyCtors.TryGetValue(key, out procAndFormalMap)) {

-        var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+      var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+      var procName = typename + ".#copy_ctor";

+      if (!this.declaredStructCopyCtors.TryGetValue(procName, out procAndFormalMap)) {

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

         var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

@@ -750,7 +778,7 @@ namespace BytecodeTranslator {
         var req = new Bpl.Requires(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, selfInExpr, otherInExpr));

         var ens = new Bpl.Ensures(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, selfInExpr, otherInExpr));

 

-        var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#copy_ctor",

+        var proc = new Bpl.Procedure(Bpl.Token.NoToken, procName,

           new Bpl.TypeVariableSeq(),

           new Bpl.VariableSeq(invars),

           new Bpl.VariableSeq(outvars),

@@ -760,7 +788,7 @@ namespace BytecodeTranslator {
           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

         procAndFormalMap = new ProcedureInfo(proc, new MethodParameter[0]);

-        this.declaredStructCopyCtors.Add(key, procAndFormalMap);

+        this.declaredStructCopyCtors.Add(procName, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

     }

@@ -1124,7 +1152,7 @@ namespace BytecodeTranslator {
     public Dictionary<string, ProcedureInfo> initiallyDeclaredProcedures = new Dictionary<string, ProcedureInfo>();

 

     public void BeginMethod(ITypeReference containingType) {

-      this.localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();

+      this.localVarMap = new Dictionary<string, Bpl.LocalVariable>();

       this.localCounter = 0;

       this.methodBeingTranslated = null;

     }

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 83e6009d..028ff1dd 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -35,8 +35,10 @@ namespace Microsoft.Boogie {
 

     public static void Main(string[] args) {

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

+      CommandLineOptions.Install(new CommandLineOptions());

+

       CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;

-      if (CommandLineOptions.Clo.Parse(args) != 1) {

+      if (!CommandLineOptions.Clo.Parse(args)) {

         goto END;

       }

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

@@ -77,7 +79,6 @@ namespace Microsoft.Boogie {
           goto END;

         }

       }

-      CommandLineOptions.Clo.RunningBoogieOnSsc = false;

       ProcessFiles(CommandLineOptions.Clo.Files);

 

     END:

@@ -223,9 +224,9 @@ namespace Microsoft.Boogie {
       Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);

       Console.WriteLine();

       if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

-        Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

+        Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

       } else {

-        Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

+        Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

       }

       if (inconclusives != 0) {

         Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0c9538d4..32b27ae6 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2112,6 +2112,7 @@ namespace Microsoft.Boogie {
         stream.WriteLine(this, level, "// " + Comment);

       }

       stream.Write(this, level, "{0}ensures ", Free ? "free " : "");

+      Cmd.EmitAttributes(stream, Attributes);

       this.Condition.Emit(stream);

       stream.WriteLine(";");

     }

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 7d3fce84..d2bdee62 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -12,103 +12,353 @@ using System.Diagnostics;
 using System.Diagnostics.Contracts;

 

 namespace Microsoft.Boogie {

-  public class CommandLineOptions {

+  public class CommandLineOptionEngine

+  {

+    public readonly string ToolName;

+    public readonly string DescriptiveToolName;

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(ToolName != null);

+      Contract.Invariant(DescriptiveToolName != null);

+      Contract.Invariant(Environment != null);

+      Contract.Invariant(cce.NonNullElements(Files));

+    }

+

+    public string/*!*/ Environment = "";

+    public List<string/*!*/>/*!*/ Files = new List<string/*!*/>();

+    public bool HelpRequested = false;

+    public bool AttrHelpRequested = false;

+

+    public CommandLineOptionEngine(string toolName, string descriptiveName) {

+      Contract.Requires(toolName != null);

+      Contract.Requires(descriptiveName != null);

+      ToolName = toolName;

+      DescriptiveToolName = descriptiveName;

+    }

+

     public static string/*!*/ VersionNumber {

       get {

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

         return cce.NonNull(cce.NonNull(System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location)).FileVersion);

       }

     }

-    public const string ToolNameBoogie = "Boogie program verifier";

-    public const string ToolNameSpecSharp = "Spec# program verifier";

-    public const string ToolNameDafny = "Dafny program verifier";

     public static string/*!*/ VersionSuffix {

       get {

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

         return " version " + VersionNumber + ", Copyright (c) 2003-2011, Microsoft.";

       }

     }

-    public string/*!*/ InputFileExtension {

-      set {

-        Contract.Requires(value != null);

-        //modifies _toolname, _version;

-        switch (value) {

-          case ".bpl":

-            _toolname = ToolNameBoogie;

-            break;

-          case ".dfy":

-            _toolname = ToolNameDafny;

-            break;

-          default:

-            _toolname = ToolNameSpecSharp;

-            break;

+    public string/*!*/ Version {

+      get {

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

+        return DescriptiveToolName + VersionSuffix;

+      }

+    }

+

+    public string/*!*/ FileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.');

+    public void ExpandFilename(ref string pattern, string logPrefix, string fileTimestamp) {

+      if (pattern != null) {

+        pattern = pattern.Replace("@PREFIX@", logPrefix).Replace("@TIME@", fileTimestamp);

+        string fn = Files.Count == 0 ? "" : Files[Files.Count - 1];

+        fn = fn.Replace('/', '-').Replace('\\', '-');

+        pattern = pattern.Replace("@FILE@", fn);

+      }

+    }

+

+    /// <summary>

+    /// Process the option and modify "ps" accordingly.

+    /// Return true if the option is one that is recognized.

+    /// </summary>

+    protected virtual bool ParseOption(string name, CommandLineParseState ps) {

+      Contract.Requires(name != null);

+      Contract.Requires(ps != null);

+

+      switch (name) {

+        case "help":

+        case "?":

+          if (ps.ConfirmArgumentCount(0)) {

+            HelpRequested = true;

+          }

+          return true;

+        case "attrHelp":

+          if (ps.ConfirmArgumentCount(0)) {

+            AttrHelpRequested = true;

+          }

+          return true;

+        default:

+          break;

+      }

+      return false;  // unrecognized option

+    }

+

+    protected class CommandLineParseState

+    {

+      public string s;

+      public bool hasColonArgument;

+      public readonly string[]/*!*/ args;

+      public int i;

+      public int nextIndex;

+      public bool EncounteredErrors;

+      public readonly string ToolName;

+      [ContractInvariantMethod]

+      void ObjectInvariant() {

+        Contract.Invariant(args != null);

+        Contract.Invariant(0 <= i && i <= args.Length);

+        Contract.Invariant(0 <= nextIndex && nextIndex <= args.Length);

+      }

+

+

+      public CommandLineParseState(string[] args, string toolName) {

+        Contract.Requires(args != null);

+        Contract.Requires(Contract.ForAll(0, args.Length, i => args[i] != null));

+        Contract.Requires(toolName != null);

+        Contract.Ensures(this.args == args);

+        this.ToolName = toolName;

+        this.s = null;  // set later by client

+        this.hasColonArgument = false;  // set later by client

+        this.args = args;

+        this.i = 0;

+        this.nextIndex = 0;  // set later by client

+        this.EncounteredErrors = false;

+      }

+

+      public bool CheckBooleanFlag(string flagName, ref bool flag, bool valueWhenPresent) {

+        Contract.Requires(flagName != null);

+        //modifies nextIndex, encounteredErrors, Console.Error.*;

+        bool flagPresent = false;

+

+        if ((s == "/" + flagName || s == "-" + flagName) && ConfirmArgumentCount(0)) {

+          flag = valueWhenPresent;

+          flagPresent = true;

+        }

+        return flagPresent;

+      }

+

+      public bool CheckBooleanFlag(string flagName, ref bool flag) {

+        Contract.Requires(flagName != null);

+        //modifies nextIndex, encounteredErrors, Console.Error.*;

+        return CheckBooleanFlag(flagName, ref flag, true);

+      }

+

+      /// <summary>

+      /// If there is one argument and it is a non-negative integer, then set "arg" to that number and return "true".

+      /// Otherwise, emit error message, leave "arg" unchanged, and return "false".

+      /// </summary>

+      public bool GetNumericArgument(ref int arg) {

+        //modifies nextIndex, encounteredErrors, Console.Error.*;

+        if (this.ConfirmArgumentCount(1)) {

+          try {

+            Contract.Assume(args[i] != null);

+            Contract.Assert(args[i] is string);  // needed to prove args[i].IsPeerConsistent

+            int d = Convert.ToInt32(this.args[this.i]);

+            if (0 <= d) {

+              arg = d;

+              return true;

+            }

+          } catch (System.FormatException) {

+          } catch (System.OverflowException) {

+          }

+        } else {

+          return false;

         }

-        _version = _toolname + VersionSuffix;

+        Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);

+        return false;

       }

+

+      /// <summary>

+      /// If there is one argument and it is a non-negative integer less than "limit",

+      /// then set "arg" to that number and return "true".

+      /// Otherwise, emit error message, leave "arg" unchanged, and return "false".

+      /// </summary>

+      public bool GetNumericArgument(ref int arg, int limit) {

+        Contract.Requires(this.i < args.Length);

+        //modifies nextIndex, encounteredErrors, Console.Error.*;

+        int a = arg;

+        if (!GetNumericArgument(ref a)) {

+          return false;

+        } else if (a < limit) {

+          arg = a;

+          return true;

+        } else {

+          Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);

+          return false;

+        }

+      }

+

+      /// <summary>

+      /// If there is one argument and it is a non-negative real, then set "arg" to that number and return "true".

+      /// Otherwise, emit an error message, leave "arg" unchanged, and return "false".

+      /// </summary>

+      public bool GetNumericArgument(ref double arg) {

+        //modifies nextIndex, encounteredErrors, Console.Error.*;

+        if (this.ConfirmArgumentCount(1)) {

+          try {

+            Contract.Assume(args[i] != null);

+            Contract.Assert(args[i] is string);  // needed to prove args[i].IsPeerConsistent

+            double d = Convert.ToDouble(this.args[this.i]);

+            if (0 <= d) {

+              arg = d;

+              return true;

+            }

+          } catch (System.FormatException) {

+          } catch (System.OverflowException) {

+          }

+        } else {

+          return false;

+        }

+        Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);

+        return false;

+      }

+

+      public bool ConfirmArgumentCount(int argCount) {

+        Contract.Requires(0 <= argCount);

+        //modifies nextIndex, encounteredErrors, Console.Error.*;

+        Contract.Ensures(Contract.Result<bool>() == (!(hasColonArgument && argCount != 1) && !(args.Length < i + argCount)));

+        if (hasColonArgument && argCount != 1) {

+          Error("\"{0}\" cannot take a colon argument", s);

+          nextIndex = args.Length;

+          return false;

+        } else if (args.Length < i + argCount) {

+          Error("\"{0}\" expects {1} argument{2}", s, argCount.ToString(), (string)(argCount == 1 ? "" : "s"));

+          nextIndex = args.Length;

+          return false;

+        } else {

+          nextIndex = i + argCount;

+          return true;

+        }

+      }

+

+      public void Error(string message, params string[] args) {

+        Contract.Requires(args != null);

+        Contract.Requires(message != null);

+        //modifies encounteredErrors, Console.Error.*;

+        Console.Error.WriteLine("{0}: Error: {1}", ToolName, String.Format(message, args));

+        EncounteredErrors = true;

+      }

+    }

+

+    public virtual void Usage() {

+      Console.WriteLine("{0}: usage:  {0} [ option ... ] [ filename ... ]", ToolName);

+      Console.WriteLine(@"  where <option> is one of

+

+  ---- General options -------------------------------------------------------

+

+  /help         this message

+  /attrHelp     print a message about declaration attributes supported by

+                this implementation");

+    }

+

+    public virtual void AttributeUsage() {

     }

-    string/*!*/ _toolname = ToolNameBoogie;

-    string/*!*/ _version = ToolNameBoogie + VersionSuffix;

+

+    /// <summary>

+    /// This method is called after all parsing is done, if no parse errors were encountered.

+    /// </summary>

+    protected virtual void ApplyDefaultOptions() {

+    }

+      

+    /// <summary>

+    /// Parses the command-line arguments "args" into the global flag variables.  Returns true

+    /// if there were no errors.

+    /// </summary>

+    /// <param name="args">Consumed ("captured" and possibly modified) by the method.</param>

+    public bool Parse([Captured] string[]/*!*/ args) {

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

+      Contract.Ensures(-2 <= Contract.Result<int>() && Contract.Result<int>() <= 2 && Contract.Result<int>() != 0);

+

+      // save the command line options for the log files

+      Environment += "Command Line Options: " + args.Concat(" ");

+      args = cce.NonNull((string[])args.Clone());  // the operations performed may mutate the array, so make a copy

+      var ps = new CommandLineParseState(args, ToolName);

+

+      while (ps.i < args.Length) {

+        cce.LoopInvariant(ps.args == args);

+        ps.s = args[ps.i];

+        Contract.Assert(ps.s != null);

+        ps.s = ps.s.Trim();

+

+        bool isOption = ps.s.StartsWith("-") || ps.s.StartsWith("/");

+        int colonIndex = ps.s.IndexOf(':');

+        if (0 <= colonIndex && isOption) {

+          ps.hasColonArgument = true;

+          args[ps.i] = ps.s.Substring(colonIndex + 1);

+          ps.s = ps.s.Substring(0, colonIndex);

+        } else {

+          ps.i++;

+          ps.hasColonArgument = false;

+        }

+        ps.nextIndex = ps.i;

+

+        if (isOption) {

+          if (!ParseOption(ps.s.Substring(1), ps)) {

+            ps.Error("unknown switch: {0}", ps.s);

+          }

+        } else if (ps.ConfirmArgumentCount(0)) {

+          string filename = ps.s;

+          Files.Add(filename);

+        }

+        ps.i = ps.nextIndex;

+      }

+

+      if (HelpRequested) {

+        Usage();

+      } else if (AttrHelpRequested) {

+        AttributeUsage();

+      } else if (ps.EncounteredErrors) {

+        Console.WriteLine("Use /help for available options");

+      }

+

+      if (ps.EncounteredErrors) {

+        return false;

+      } else {

+        this.ApplyDefaultOptions();

+        return true;

+      }

+    }

+

+  }

+

+  /// <summary>

+  /// Boogie command-line options (other tools can subclass this class in order to support a

+  /// superset of Boogie's options.

+  /// </summary>

+  public class CommandLineOptions : CommandLineOptionEngine {

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(_toolname != null);

-      Contract.Invariant(_version != null);

-      Contract.Invariant(Environment != null);

-      Contract.Invariant(FileName != null);

-      Contract.Invariant(cce.NonNullElements(Files));

-      Contract.Invariant(cce.NonNullElements(ContractAssemblies));

       Contract.Invariant(FileTimestamp != null);

     }

 

-    public string/*!*/ ToolName {

-      get {

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

-        return _toolname;

-      }

+    public CommandLineOptions()

+      : base("Boogie", "Boogie program verifier") {

     }

-    public string/*!*/ Version {

-      get {

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

-        return _version;

-      }

+

+    protected CommandLineOptions(string toolName, string descriptiveName)

+      : base(toolName, descriptiveName) {

+      Contract.Requires(toolName != null);

+      Contract.Requires(descriptiveName != null);

     }

 

-    private static CommandLineOptions clo = new CommandLineOptions();

+    private static CommandLineOptions clo;

     public static CommandLineOptions/*!*/ Clo

     {

       get { return clo; }

     }

 

-    public string/*!*/ Environment = "";

-    public string/*!*/ FileName = "unknown";

+    public static void Install(CommandLineOptions options) {

+      Contract.Requires(options != null);

+      clo = options;

+    }

 

     public const long Megabyte = 1048576;

 

     // Flags and arguments

 

     public bool RunningBoogieFromCommandLine = false;  // "false" means running Boogie from the plug-in

-    public bool RunningBoogieOnSsc = true; // "true" means running Boogie on ssc input while false means running it on bpl input

-

-    public bool AttrHelpRequested = false;

-

-    [Peer]

-    public List<string/*!*/>/*!*/ Files = new List<string/*!*/>();

-    public List<string/*!*/>/*!*/ ContractAssemblies = new List<string/*!*/>();

-

-    public string/*!*/ FileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.');

-    public void ExpandFilename(ref string pattern) {

-      if (pattern != null) {

-        pattern = pattern.Replace("@PREFIX@", LogPrefix).Replace("@TIME@", FileTimestamp);

-        string fn = Files.Count == 0 ? "" : Files[Files.Count - 1];

-        fn = fn.Replace('/', '-').Replace('\\', '-');

-        pattern = pattern.Replace("@FILE@", fn);

-      }

-    }

 

     [ContractInvariantMethod]

     void ObjectInvariant2() {

       Contract.Invariant(LogPrefix != null);

       Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3);  // 0 = print only structured,  1 = both structured and unstructured,  2 = only unstructured

-

     }

 

     public string PrintFile = null;

@@ -136,9 +386,6 @@ namespace Microsoft.Boogie {
     public bool NoTypecheck = false;

     public bool OverlookBoogieTypeErrors = false;

     public bool Verify = true;

-    public bool DisallowSoundnessCheating = false;

-    public int DafnyInduction = 3;

-    public int DafnyInductionHeuristic = 6;

     public bool TraceVerify = false;

     public int /*(0:3)*/ ErrorTrace = 1;

     public bool IntraproceduralInfer = true;

@@ -149,23 +396,6 @@ namespace Microsoft.Boogie {
     public bool SoundnessSmokeTest = false;

     public string Z3ExecutablePath = null;

 

-    private bool noConsistencyChecks = false;

-    public bool NoConsistencyChecks {

-      get {

-        return !Verify ? true : noConsistencyChecks;

-      }

-      set

-        //modifies noConsistencyChecks;

-        {

-        noConsistencyChecks = value;

-      }

-    }

-

-    public string DafnyPrelude = null;

-    public string DafnyPrintFile = null;

-    public bool Compile = true;

-    public bool ForceCompile = false;

-

     public enum ProverWarnings {

       None,

       Stdout,

@@ -192,11 +422,6 @@ namespace Microsoft.Boogie {
     public bool DontShowLogo = false;

     [ContractInvariantMethod]

     void ObjectInvariant3() {

-      Contract.Invariant(0 <= CheckingLevel && CheckingLevel < 3);

-      Contract.Invariant(0 <= OrderStrength && OrderStrength < 2);

-      Contract.Invariant(0 <= SummationAxiomStrength && SummationAxiomStrength < 2);

-      Contract.Invariant(0 <= InductiveMinMax && InductiveMinMax < 6);

-      Contract.Invariant(0 <= FCOStrength && FCOStrength < 6);

       Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3);

       Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7);

       Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);

@@ -206,17 +431,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(cce.NonNullElements(ProverOptions));

     }

 

-    public int CheckingLevel = 2;

-    public enum Methodology {

-      Boogie,

-      VisibleState

-    }

-    public Methodology MethodologySelection = Methodology.Boogie;

-    public int OrderStrength = 0;

-    public bool UseArithDistributionAxioms = false;

-    public int SummationAxiomStrength = 1;

-    public int InductiveMinMax = 0;

-    public int FCOStrength = 5;

     public int LoopUnrollCount = -1;  // -1 means don't unroll loops

     public int LoopFrameConditions = -1;  // -1 means not specified -- this will be replaced by the "implications" section below

     public int ModifiesDefault = 5;

@@ -373,46 +587,17 @@ namespace Microsoft.Boogie {
         TraceListenerCollection/*!*/ dbl = Debug.Listeners;

         Contract.Assert(dbl != null);

         Contract.Assume(cce.IsPeerConsistent(dbl));  // hangs off static field

-#if WHIDBEY

-        dbl.Add(new ConsoleTraceListener());

-#else

         dbl.Add(new DefaultTraceListener());

-#endif

       }

     }

 

-    private string methodToLog = null;

-    private string methodToBreakOn = null;

+    public List<string/*!*/> ProcsToCheck = null;  // null means "no restriction"

     [ContractInvariantMethod]

     void ObjectInvariant5() {

       Contract.Invariant(cce.NonNullElements(ProcsToCheck, true));

-      Contract.Invariant(cce.NonNullElements(methodsToTranslateClass, true));

-      Contract.Invariant(cce.NonNullElements(methodsToTranslateClassQualified, true));

-      Contract.Invariant(cce.NonNullElements(methodsToTranslateExclude));

-      Contract.Invariant(cce.NonNullElements(methodsToTranslateFile, true));

-      Contract.Invariant(cce.NonNullElements(methodsToTranslateMethod, true));

-      Contract.Invariant(cce.NonNullElements(methodsToTranslateMethodQualified, true));

-      Contract.Invariant(cce.NonNullElements(methodsToTranslateSubstring, true));

       Contract.Invariant(Ai != null);

     }

 

-    [Rep]

-    public List<string/*!*/> ProcsToCheck = null;  // null means "no restriction"

-    [Rep]

-    private List<string/*!*/> methodsToTranslateSubstring = null;  // null means "no restriction"

-    [Rep]

-    private List<string/*!*/> methodsToTranslateMethod = null;  // null means "no restriction"

-    [Rep]

-    private List<string/*!*/> methodsToTranslateMethodQualified = null;  // null means "no restriction"

-    [Rep]

-    private List<string/*!*/> methodsToTranslateClass = null;  // null means "no restriction"

-    [Rep]

-    private List<string/*!*/> methodsToTranslateClassQualified = null;  // null means "no restriction"

-    [Rep]

-    private List<string/*!*/> methodsToTranslateFile = null;  // null means "no restriction"

-    [Rep]

-    private List<string/*!*/>/*!*/ methodsToTranslateExclude = new List<string/*!*/>();

-

     public class AiFlags {

       public bool Intervals = false;

       public bool Constant = false;

@@ -433,932 +618,572 @@ namespace Microsoft.Boogie {
     }

     public AiFlags/*!*/ Ai = new AiFlags();

 

-    [Verify(false)]

-    private CommandLineOptions() {

-      // this is just to suppress verification.

-    }

-

-    [Verify(false)]

-    public static void ResetClo()

-    {

-      clo = new CommandLineOptions();

-    }

-

-

-    /// <summary>

-    /// Parses the command-line arguments "args" into the global flag variables.  The possible result

-    /// values are:

-    /// -2: an error occurred and help was requested

-    /// -1: no error occurred and help was requested

-    ///  1: no error occurred and help was not requested

-    ///  2: an error occurred and help was not requested

-    /// </summary>

-    /// <param name="args">Consumed ("captured" and possibly modified) by the method.</param>

-    [Verify(false)]

-    public int Parse([Captured] string[]/*!*/ args) {

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

-      Contract.Ensures(TheProverFactory != null);

-      Contract.Ensures(vcVariety != VCVariety.Unspecified);

-      Contract.Ensures(-2 <= Contract.Result<int>() && Contract.Result<int>() <= 2 && Contract.Result<int>() != 0);

-      // save the command line options for the log files

-      Environment += "Command Line Options:";

-      foreach (string s in args)

-        Environment += " " + s;

-      args = cce.NonNull((string[])args.Clone());  // the operations performed may mutate the array, so make a copy

-      CommandLineParseState/*!*/ ps = new CommandLineParseState(args);

-      Contract.Assert(ps != null);

-      int res = 1;  // the result value

-

-      while (ps.i < args.Length) {

-        cce.LoopInvariant(cce.IsPeerConsistent(ps));

-        cce.LoopInvariant(ps.args == args);

-        ps.s = args[ps.i];

-        Contract.Assert(ps.s != null);

-        ps.s = ps.s.Trim();

-

-        int colonIndex = ps.s.IndexOf(':');

-        if (colonIndex >= 0 && (ps.s.StartsWith("-") || ps.s.StartsWith("/"))) {

-          ps.hasColonArgument = true;

-          args[ps.i] = ps.s.Substring(colonIndex + 1);

-          ps.s = ps.s.Substring(0, colonIndex);

-        } else {

-          cce.BeginExpose(ps);

-          {

-            ps.i++;

-          }

-          cce.EndExpose();

-          ps.hasColonArgument = false;

-        }

-        ps.nextIndex = ps.i;

-

-

-        switch (ps.s) {

-          case "-help":

-          case "/help":

-          case "-?":

-          case "/?":

-            if (ps.ConfirmArgumentCount(0)) {

-              res = -1;  // help requested

-            }

-            break;

-

-          case "-attrHelp":

-          case "/attrHelp":

-            if (ps.ConfirmArgumentCount(0)) {

-              AttrHelpRequested = true;

-            }

-            break;

-

-          case "-infer":

-          case "/infer":

-            if (ps.ConfirmArgumentCount(1)) {

-              foreach (char c in cce.NonNull(args[ps.i])) {

-                switch (c) {

-                  case 'i':

-                    Ai.Intervals = true;

-                    UseAbstractInterpretation = true;

-                    break;

-                  case 'c':

-                    Ai.Constant = true;

-                    UseAbstractInterpretation = true;

-                    break;

-                  case 'd':

-                    Ai.DynamicType = true;

-                    UseAbstractInterpretation = true;

-                    break;

-                  case 'n':

-                    Ai.Nullness = true;

-                    UseAbstractInterpretation = true;

-                    break;

-                  case 'p':

-                    Ai.Polyhedra = true;

-                    UseAbstractInterpretation = true;

-                    break;

-                  case 's':

-                    Ai.DebugStatistics = true;

-                    UseAbstractInterpretation = true;

-                    break;

-                  case '0':

-                  case '1':

-                  case '2':

-                  case '3':

-                  case '4':

-                  case '5':

-                  case '6':

-                  case '7':

-                  case '8':

-                  case '9':

-                    StepsBeforeWidening = (int)char.GetNumericValue(c);

-                    break;

-                  default:

-                    ps.Error("Invalid argument '{0}' to option {1}", c.ToString(), ps.s);

-                    break;

-                }

+    protected override bool ParseOption(string name, CommandLineOptionEngine.CommandLineParseState ps) {

+      var args = ps.args;  // convenient synonym

+      switch (name) {

+        case "infer":

+          if (ps.ConfirmArgumentCount(1)) {

+            foreach (char c in cce.NonNull(args[ps.i])) {

+              switch (c) {

+                case 'i':

+                  Ai.Intervals = true;

+                  UseAbstractInterpretation = true;

+                  break;

+                case 'c':

+                  Ai.Constant = true;

+                  UseAbstractInterpretation = true;

+                  break;

+                case 'd':

+                  Ai.DynamicType = true;

+                  UseAbstractInterpretation = true;

+                  break;

+                case 'n':

+                  Ai.Nullness = true;

+                  UseAbstractInterpretation = true;

+                  break;

+                case 'p':

+                  Ai.Polyhedra = true;

+                  UseAbstractInterpretation = true;

+                  break;

+                case 's':

+                  Ai.DebugStatistics = true;

+                  UseAbstractInterpretation = true;

+                  break;

+                case '0':

+                case '1':

+                case '2':

+                case '3':

+                case '4':

+                case '5':

+                case '6':

+                case '7':

+                case '8':

+                case '9':

+                  StepsBeforeWidening = (int)char.GetNumericValue(c);

+                  break;

+                default:

+                  ps.Error("Invalid argument '{0}' to option {1}", c.ToString(), ps.s);

+                  break;

               }

             }

-            break;

+          }

+          return true;

 

-          case "-noinfer":

-          case "/noinfer":

-            if (ps.ConfirmArgumentCount(0)) {

-              UseAbstractInterpretation = false;

-            }

-            break;

-

-          case "-log":

-          case "/log":

-            if (ps.hasColonArgument) {

-              methodToLog = args[ps.i];

-              ps.nextIndex = ps.i + 1;

-            } else {

-              methodToLog = "*";

-            }

-            break;

+        case "noinfer":

+          if (ps.ConfirmArgumentCount(0)) {

+            UseAbstractInterpretation = false;

+          }

+          return true;

 

-          case "-logInfer":

-          case "/logInfer":

+        case "logInfer":

+          if (ps.ConfirmArgumentCount(0)) {

             Microsoft.AbstractInterpretationFramework.Lattice.LogSwitch = true;

-            break;

-

-          case "-break":

-          case "/break":

-            if (ps.hasColonArgument) {

-              methodToBreakOn = args[ps.i];

-              ps.nextIndex = ps.i + 1;

-            } else {

-              System.Diagnostics.Debugger.Break();

-            }

-            break;

+          }

+          return true;

 

-          case "-launch":

-          case "/launch":

+        case "break":

+        case "launch":

+          if (ps.ConfirmArgumentCount(0)) {

             System.Diagnostics.Debugger.Launch();

-            break;

-

-          case "-proc":

-          case "/proc":

-            if (ProcsToCheck == null) {

-              ProcsToCheck = new List<string/*!*/>();

-            }

-            if (ps.ConfirmArgumentCount(1)) {

-              ProcsToCheck.Add(cce.NonNull(args[ps.i]));

-            }

-            break;

-

-          case "-translate":

-          case "/translate":

-            if (methodsToTranslateSubstring == null) {

-              methodsToTranslateSubstring = new List<string/*!*/>();

-            }

-            if (ps.ConfirmArgumentCount(1)) {

-              methodsToTranslateSubstring.Add(cce.NonNull(args[ps.i]));

-            }

-            break;

-

-          case "-trMethod":

-          case "/trMethod":

-            if (ps.ConfirmArgumentCount(1)) {

-              string m = cce.NonNull(args[ps.i]);

-              if (0 <= m.IndexOf('.')) {

-                if (methodsToTranslateMethodQualified == null) {

-                  methodsToTranslateMethodQualified = new List<string/*!*/>();

-                }

-                methodsToTranslateMethodQualified.Add(m);

-              } else {

-                if (methodsToTranslateMethod == null) {

-                  methodsToTranslateMethod = new List<string/*!*/>();

-                }

-                methodsToTranslateMethod.Add(m);

-              }

-            }

-            break;

-

-          case "-trClass":

-          case "/trClass":

-            if (ps.ConfirmArgumentCount(1)) {

-              string m = cce.NonNull(args[ps.i]);

-              if (0 <= m.IndexOf('.')) {

-                if (methodsToTranslateClassQualified == null) {

-                  methodsToTranslateClassQualified = new List<string/*!*/>();

-                }

-                methodsToTranslateClassQualified.Add(m);

-              } else {

-                if (methodsToTranslateClass == null) {

-                  methodsToTranslateClass = new List<string/*!*/>();

-                }

-                methodsToTranslateClass.Add(m);

-              }

-            }

-            break;

-

-          case "-trFile":

-          case "/trFile":

-            if (methodsToTranslateFile == null) {

-              methodsToTranslateFile = new List<string/*!*/>();

-            }

-            if (ps.ConfirmArgumentCount(1)) {

-              methodsToTranslateFile.Add(cce.NonNull(args[ps.i]));

-            }

-            break;

-

-          case "-trExclude":

-          case "/trExclude":

-            if (ps.ConfirmArgumentCount(1)) {

-              methodsToTranslateExclude.Add(cce.NonNull(args[ps.i]));

-            }

-            break;

+          }

+          return true;

 

-          case "-xml":

-          case "/xml":

-            if (ps.ConfirmArgumentCount(1)) {

-              XmlSinkFilename = args[ps.i];

-            }

-            break;

+        case "proc":

+          if (ProcsToCheck == null) {

+            ProcsToCheck = new List<string/*!*/>();

+          }

+          if (ps.ConfirmArgumentCount(1)) {

+            ProcsToCheck.Add(cce.NonNull(args[ps.i]));

+          }

+          return true;

 

-          case "-print":

-          case "/print":

-            if (ps.ConfirmArgumentCount(1)) {

-              PrintFile = args[ps.i];

-            }

-            break;

+        case "xml":

+          if (ps.ConfirmArgumentCount(1)) {

+            XmlSinkFilename = args[ps.i];

+          }

+          return true;

 

-          case "-dprelude":

-          case "/dprelude":

-            if (ps.ConfirmArgumentCount(1))

-            {

-                DafnyPrelude = args[ps.i];

-            }

-            break;

+        case "print":

+          if (ps.ConfirmArgumentCount(1)) {

+            PrintFile = args[ps.i];

+          }

+          return true;

 

-          case "-dprint":

-          case "/dprint":

-            if (ps.ConfirmArgumentCount(1)) {

-              DafnyPrintFile = args[ps.i];

-            }

-            break;

-

-          case "-compile":

-          case "/compile": {

-              int compile = 0;

-              if (ps.GetNumericArgument(ref compile, 3)) {

-                Compile = compile == 1 || compile == 2;

-                ForceCompile = compile == 2;

-              }

-              break;

-            }

+        case "proverLog":

+          if (ps.ConfirmArgumentCount(1)) {

+            SimplifyLogFilePath = args[ps.i];

+          }

+          return true;

 

-          case "-noCheating":

-          case "/noCheating": {

-              int cheat = 0; // 0 is default, allows cheating

-              if (ps.GetNumericArgument(ref cheat, 2)) {

-                DisallowSoundnessCheating = cheat == 1;

-              }

-              break;

-            }

+        case "logPrefix":

+          if (ps.ConfirmArgumentCount(1)) {

+            string s = cce.NonNull(args[ps.i]);

+            LogPrefix += s.Replace('/', '-').Replace('\\', '-');

+          }

+          return true;

 

-          case "-induction":

-          case "/induction":

-            ps.GetNumericArgument(ref DafnyInduction, 4);

-            break;

-

-          case "-inductionHeuristic":

-          case "/inductionHeuristic":

-            ps.GetNumericArgument(ref DafnyInductionHeuristic, 7);

-            break;

-

-          case "-contracts":

-          case "/contracts":

-          case "-c":

-          case "/c":

-            if (ps.ConfirmArgumentCount(1)) {

-              ContractAssemblies.Add(cce.NonNull(args[ps.i]));

-            }

-            break;

+        case "proverShutdownLimit":

+          ps.GetNumericArgument(ref ProverShutdownLimit);

+          return true;

 

-          case "-proverLog":

-          case "/proverLog":

-            if (ps.ConfirmArgumentCount(1)) {

-              SimplifyLogFilePath = args[ps.i];

-            }

-            break;

+        case "errorTrace":

+          ps.GetNumericArgument(ref ErrorTrace, 3);

+          return true;

 

-          case "-logPrefix":

-          case "/logPrefix":

-            if (ps.ConfirmArgumentCount(1)) {

-              string s = cce.NonNull(args[ps.i]);

-              LogPrefix += s.Replace('/', '-').Replace('\\', '-');

-            }

-            break;

-

-          case "-proverShutdownLimit":

-          case "/proverShutdownLimit":

-            ps.GetNumericArgument(ref ProverShutdownLimit);

-            break;

-

-          case "-errorTrace":

-          case "/errorTrace":

-            ps.GetNumericArgument(ref ErrorTrace, 3);

-            break;

-

-          case "-level":

-          case "/level":

-            ps.GetNumericArgument(ref CheckingLevel, 3);

-            break;

-

-          case "-methodology":

-          case "/methodology":

-            if (ps.ConfirmArgumentCount(1)) {

-              switch (args[ps.i]) {

-                case "b":

-                case "Boogie":

-                case "boogie":

-                  MethodologySelection = Methodology.Boogie;

+        case "proverWarnings": {

+            int pw = 0;

+            if (ps.GetNumericArgument(ref pw, 3)) {

+              switch (pw) {

+                case 0:

+                  PrintProverWarnings = ProverWarnings.None;

                   break;

-                case "vs":

-                case "visible-state":

-                  MethodologySelection = Methodology.VisibleState;

+                case 1:

+                  PrintProverWarnings = ProverWarnings.Stdout;

                   break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                case 2:

+                  PrintProverWarnings = ProverWarnings.Stderr;

                   break;

+                default: {

+                    Contract.Assert(false);

+                    throw new cce.UnreachableException();

+                  } // postcondition of GetNumericArgument guarantees that we don't get here

               }

             }

-            break;

-

-          case "-proverWarnings":

-          case "/proverWarnings": {

-              int pw = 0;

-              if (ps.GetNumericArgument(ref pw, 3)) {

-                switch (pw) {

-                  case 0:

-                    PrintProverWarnings = ProverWarnings.None;

-                    break;

-                  case 1:

-                    PrintProverWarnings = ProverWarnings.Stdout;

-                    break;

-                  case 2:

-                    PrintProverWarnings = ProverWarnings.Stderr;

-                    break;

-                  default: {

-                      Contract.Assert(false);

-                      throw new cce.UnreachableException();

-                    } // postcondition of GetNumericArgument guarantees that we don't get here

-                }

-              }

-              break;

-            }

-

-          case "-env":

-          case "/env": {

-              int e = 0;

-              if (ps.GetNumericArgument(ref e, 3)) {

-                switch (e) {

-                  case 0:

-                    ShowEnv = ShowEnvironment.Never;

-                    break;

-                  case 1:

-                    ShowEnv = ShowEnvironment.DuringPrint;

-                    break;

-                  case 2:

-                    ShowEnv = ShowEnvironment.Always;

-                    break;

-                  default: {

-                      Contract.Assert(false);

-                      throw new cce.UnreachableException();

-                    } // postcondition of GetNumericArgument guarantees that we don't get here

-                }

-              }

-              break;

-            }

+            return true;

+          }

 

-          case "-loopUnroll":

-          case "/loopUnroll":

-            ps.GetNumericArgument(ref LoopUnrollCount);

-            break;

-

-          case "-modifiesOnLoop":

-          case "/modifiesOnLoop":

-            ps.GetNumericArgument(ref LoopFrameConditions, 3);

-            break;

-

-          case "-modifiesDefault":

-          case "/modifiesDefault":

-            ps.GetNumericArgument(ref ModifiesDefault, 7);

-            break;

-

-          case "-localModifiesChecks":

-          case "/localModifiesChecks": {

-              int localChecks = 0;

-              ps.GetNumericArgument(ref localChecks, 2);

-              LocalModifiesChecks = (localChecks != 0);

-            }

-            break;

-

-          case "-orderStrength":

-          case "/orderStrength":

-            ps.GetNumericArgument(ref OrderStrength, 2);

-            break;

-

-          case "-summationStrength":

-          case "/summationStrength":

-            ps.GetNumericArgument(ref SummationAxiomStrength, 2);

-            break;

-

-          case "-inductiveMinMax":

-          case "/inductiveMinMax":

-            ps.GetNumericArgument(ref InductiveMinMax, 6);

-            break;

-

-          case "-fcoStrength":

-          case "/fcoStrength":

-            ps.GetNumericArgument(ref FCOStrength, 6);

-            break;

-

-          case "-ownerModelEncoding":

-          case "/ownerModelEncoding":

-            if (ps.ConfirmArgumentCount(1)) {

-              switch (args[ps.i]) {

-                case "s":

-                case "standard":

-                  OwnershipModelEncoding = OwnershipModelOption.Standard;

+        case "env": {

+            int e = 0;

+            if (ps.GetNumericArgument(ref e, 3)) {

+              switch (e) {

+                case 0:

+                  ShowEnv = ShowEnvironment.Never;

                   break;

-                case "e":

-                case "experimental":

-                  OwnershipModelEncoding = OwnershipModelOption.Experimental;

+                case 1:

+                  ShowEnv = ShowEnvironment.DuringPrint;

                   break;

-                case "t":

-                case "trivial":

-                  OwnershipModelEncoding = OwnershipModelOption.Trivial;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                case 2:

+                  ShowEnv = ShowEnvironment.Always;

                   break;

+                default: {

+                    Contract.Assert(false);

+                    throw new cce.UnreachableException();

+                  } // postcondition of GetNumericArgument guarantees that we don't get here

               }

             }

-            break;

-

-          case "-printModel":

-          case "/printModel":

-            if (ps.ConfirmArgumentCount(1)) {

-              switch (args[ps.i]) {

-                case "0":

-                  PrintErrorModel = 0;

-                  break;

-                case "1":

-                  PrintErrorModel = 1;

-                  break;

-                case "2":

-                  PrintErrorModel = 2;

-                  break;

-                case "4":

-                  PrintErrorModel = 4;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

-            }

-            break;

+            return true;

+          }

 

+        case "loopUnroll":

+          ps.GetNumericArgument(ref LoopUnrollCount);

+          return true;

 

-          case "-mv":

-          case "/mv":

-            if (ps.ConfirmArgumentCount(1)) {

-              ModelViewFile = args[ps.i];

+        case "printModel":

+          if (ps.ConfirmArgumentCount(1)) {

+            switch (args[ps.i]) {

+              case "0":

+                PrintErrorModel = 0;

+                break;

+              case "1":

+                PrintErrorModel = 1;

+                break;

+              case "2":

+                PrintErrorModel = 2;

+                break;

+              case "4":

+                PrintErrorModel = 4;

+                break;

+              default:

+                ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                break;

             }

-            break;

+          }

+          return true;

 

-          case "-printModelToFile":

-          case "/printModelToFile":

-            if (ps.ConfirmArgumentCount(1)) {

-              PrintErrorModelFile = args[ps.i];

-            }

-            break;

-

-

-          case "-enhancedErrorMessages":

-          case "/enhancedErrorMessages":

-            ps.GetNumericArgument(ref EnhancedErrorMessages, 2);

-            break;

-

-          case "-forceBplErrors":

-          case "/forceBplErrors":

-            ForceBplErrors = true;

-            break;

-

-          case "-contractInfer":

-          case "/contractInfer":

-            ContractInfer = true;

-            break;

-          case "-inlineDepth":

-          case "/inlineDepth":

-            ps.GetNumericArgument(ref InlineDepth);

-            break;

-          case "-subsumption":

-          case "/subsumption": {

-              int s = 0;

-              if (ps.GetNumericArgument(ref s, 3)) {

-                switch (s) {

-                  case 0:

-                    UseSubsumption = SubsumptionOption.Never;

-                    break;

-                  case 1:

-                    UseSubsumption = SubsumptionOption.NotForQuantifiers;

-                    break;

-                  case 2:

-                    UseSubsumption = SubsumptionOption.Always;

-                    break;

-                  default: {

-                      Contract.Assert(false);

-                      throw new cce.UnreachableException();

-                    } // postcondition of GetNumericArgument guarantees that we don't get here

-                }

-              }

-              break;

-            }

+        case "mv":

+          if (ps.ConfirmArgumentCount(1)) {

+            ModelViewFile = args[ps.i];

+          }

+          return true;

 

-          case "-liveVariableAnalysis":

-          case "/liveVariableAnalysis": {

-              int lva = 0;

-              if (ps.GetNumericArgument(ref lva, 3)) {

-                LiveVariableAnalysis = lva;

-              }

-              break;

-            }

+        case "printModelToFile":

+          if (ps.ConfirmArgumentCount(1)) {

+            PrintErrorModelFile = args[ps.i];

+          }

+          return true;

 

-          case "-removeEmptyBlocks":

-          case "/removeEmptyBlocks": {

-              int reb = 0;

-              if (ps.GetNumericArgument(ref reb, 2)) {

-                RemoveEmptyBlocks = reb == 1;

-              }

-              break;

-            }

+        case "enhancedErrorMessages":

+          ps.GetNumericArgument(ref EnhancedErrorMessages, 2);

+          return true;

 

-          case "-coalesceBlocks":

-          case "/coalesceBlocks": {

-              int cb = 0;

-              if (ps.GetNumericArgument(ref cb, 2)) {

-                CoalesceBlocks = cb == 1;

-              }

-              break;

-            }

+        case "contractInfer":

+          ContractInfer = true;

+          return true;

 

-          case "-vc":

-          case "/vc":

-            if (ps.ConfirmArgumentCount(1)) {

-              switch (args[ps.i]) {

-                case "s":

-                case "structured":

-                  vcVariety = VCVariety.Structured;

-                  break;

-                case "b":

-                case "block":

-                  vcVariety = VCVariety.Block;

-                  break;

-                case "l":

-                case "local":

-                  vcVariety = VCVariety.Local;

-                  break;

-                case "n":

-                case "nested":

-                  vcVariety = VCVariety.BlockNested;

-                  break;

-                case "m":

-                  vcVariety = VCVariety.BlockNestedReach;

-                  break;

-                case "r":

-                  vcVariety = VCVariety.BlockReach;

-                  break;

-                case "d":

-                case "dag":

-                  vcVariety = VCVariety.Dag;

-                  break;

-                case "i":

-                  vcVariety = VCVariety.DagIterative;

+        case "inlineDepth":

+          ps.GetNumericArgument(ref InlineDepth);

+          return true;

+

+        case "subsumption": {

+            int s = 0;

+            if (ps.GetNumericArgument(ref s, 3)) {

+              switch (s) {

+                case 0:

+                  UseSubsumption = SubsumptionOption.Never;

                   break;

-                case "doomed":

-                  vcVariety = VCVariety.Doomed;

+                case 1:

+                  UseSubsumption = SubsumptionOption.NotForQuantifiers;

                   break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                case 2:

+                  UseSubsumption = SubsumptionOption.Always;

                   break;

+                default: {

+                    Contract.Assert(false);

+                    throw new cce.UnreachableException();

+                  } // postcondition of GetNumericArgument guarantees that we don't get here

               }

             }

-            break;

+            return true;

+          }

 

-          case "-prover":

-          case "/prover":

-            if (ps.ConfirmArgumentCount(1)) {

-              TheProverFactory = ProverFactory.Load(cce.NonNull(args[ps.i]));

-              ProverName = cce.NonNull(args[ps.i]).ToUpper();

-            }

-            break;

-

-          case "-p":

-          case "/p":

-          case "-proverOpt":

-          case "/proverOpt":

-            if (ps.ConfirmArgumentCount(1)) {

-              ProverOptions.Add(cce.NonNull(args[ps.i]));

-            }

-            break;

-

-          case "-DoomStrategy":

-          case "/DoomStrategy":

-            ps.GetNumericArgument(ref DoomStrategy);

-            break;

-          case "-DoomRestartTP":

-          case "/DoomRestartTP":

-            if (ps.ConfirmArgumentCount(0))

-            {

-                DoomRestartTP = true;

+        case "liveVariableAnalysis": {

+            int lva = 0;

+            if (ps.GetNumericArgument(ref lva, 3)) {

+              LiveVariableAnalysis = lva;

             }

-            break;

+            return true;

+          }

 

-          case "-extractLoops":

-          case "/extractLoops":

-            if (ps.ConfirmArgumentCount(0)) {

-              ExtractLoops = true;

-            }

-            break;

-          case "-inline":

-          case "/inline":

-            if (ps.ConfirmArgumentCount(1)) {

-              switch (args[ps.i]) {

-                case "none":

-                  ProcedureInlining = Inlining.None;

-                  break;

-                case "assert":

-                  ProcedureInlining = Inlining.Assert;

-                  break;

-                case "assume":

-                  ProcedureInlining = Inlining.Assume;

-                  break;

-                case "spec":

-                  ProcedureInlining = Inlining.Spec;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

+        case "removeEmptyBlocks": {

+            int reb = 0;

+            if (ps.GetNumericArgument(ref reb, 2)) {

+              RemoveEmptyBlocks = reb == 1;

             }

-            break;

-          case "-lazyInline":

-          case "/lazyInline":

-            if (ps.ConfirmArgumentCount(1)) {

-                LazyInlining = Int32.Parse(args[ps.i]);

-                if (LazyInlining > 3) ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-            }

-            break;

-          case "-procCopyBound":

-          case "/procCopyBound":

-            if (ps.ConfirmArgumentCount(1))

-            {

-                ProcedureCopyBound = Int32.Parse(args[ps.i]);

-            }

-            break;

-          case "-stratifiedInline":

-          case "/stratifiedInline":

-            if (ps.ConfirmArgumentCount(1)) {

-              switch (args[ps.i]) {

-                case "0":

-                  StratifiedInlining = 0;

-                  break;

-                case "1":

-                  StratifiedInlining = 1;

-                  break;

-                default:

-                  StratifiedInlining = Int32.Parse(cce.NonNull(args[ps.i]));

-                  //ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

-            }

-            break;

-          case "-recursionBound":

-          case "/recursionBound":

-            if(ps.ConfirmArgumentCount(1)){

-              RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));

-            }

-            break;

-          case "-coverageReporter":

-          case "/coverageReporter":

-            if (ps.ConfirmArgumentCount(1)) {

-              CoverageReporterPath = args[ps.i];

+            return true;

+          }

+

+        case "coalesceBlocks": {

+            int cb = 0;

+            if (ps.GetNumericArgument(ref cb, 2)) {

+              CoalesceBlocks = cb == 1;

             }

-            break;

-          case "-stratifiedInlineOption":

-          case "/stratifiedInlineOption":

-            if (ps.ConfirmArgumentCount(1)) {

-              StratifiedInliningOption=Int32.Parse(cce.NonNull(args[ps.i]));

+            return true;

+          }

+

+        case "vc":

+          if (ps.ConfirmArgumentCount(1)) {

+            switch (args[ps.i]) {

+              case "s":

+              case "structured":

+                vcVariety = VCVariety.Structured;

+                break;

+              case "b":

+              case "block":

+                vcVariety = VCVariety.Block;

+                break;

+              case "l":

+              case "local":

+                vcVariety = VCVariety.Local;

+                break;

+              case "n":

+              case "nested":

+                vcVariety = VCVariety.BlockNested;

+                break;

+              case "m":

+                vcVariety = VCVariety.BlockNestedReach;

+                break;

+              case "r":

+                vcVariety = VCVariety.BlockReach;

+                break;

+              case "d":

+              case "dag":

+                vcVariety = VCVariety.Dag;

+                break;

+              case "i":

+                vcVariety = VCVariety.DagIterative;

+                break;

+              case "doomed":

+                vcVariety = VCVariety.Doomed;

+                break;

+              default:

+                ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                break;

             }

-            break;

-          case "-useUnsatCoreForInlining":

-          case "/useUnsatCoreForInlining":

-            UseUnsatCoreForInlining = true;

-            break;

-          case "-inferLeastForUnsat":

-          case "/inferLeastForUnsat":

-            if (ps.ConfirmArgumentCount(1))

-            {

-                inferLeastForUnsat = args[ps.i];

+          }

+          return true;

+

+        case "prover":

+          if (ps.ConfirmArgumentCount(1)) {

+            TheProverFactory = ProverFactory.Load(cce.NonNull(args[ps.i]));

+            ProverName = cce.NonNull(args[ps.i]).ToUpper();

+          }

+          return true;

+

+        case "p":

+        case "proverOpt":

+          if (ps.ConfirmArgumentCount(1)) {

+            ProverOptions.Add(cce.NonNull(args[ps.i]));

+          }

+          return true;

+

+        case "DoomStrategy":

+          ps.GetNumericArgument(ref DoomStrategy);

+          return true;

+

+        case "DoomRestartTP":

+          if (ps.ConfirmArgumentCount(0)) {

+            DoomRestartTP = true;

+          }

+          return true;

+

+        case "extractLoops":

+          if (ps.ConfirmArgumentCount(0)) {

+            ExtractLoops = true;

+          }

+          return true;

+

+        case "inline":

+          if (ps.ConfirmArgumentCount(1)) {

+            switch (args[ps.i]) {

+              case "none":

+                ProcedureInlining = Inlining.None;

+                break;

+              case "assert":

+                ProcedureInlining = Inlining.Assert;

+                break;

+              case "assume":

+                ProcedureInlining = Inlining.Assume;

+                break;

+              case "spec":

+                ProcedureInlining = Inlining.Spec;

+                break;

+              default:

+                ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                break;

             }

-            break;

-          case "-typeEncoding":

-          case "/typeEncoding":

-            if (ps.ConfirmArgumentCount(1)) {

-              switch (args[ps.i]) {

-                case "n":

-                case "none":

-                  TypeEncodingMethod = TypeEncoding.None;

-                  break;

-                case "p":

-                case "predicates":

-                  TypeEncodingMethod = TypeEncoding.Predicates;

-                  break;

-                case "a":

-                case "arguments":

-                  TypeEncodingMethod = TypeEncoding.Arguments;

-                  break;

-                case "m":

-                case "monomorphic":

-                  TypeEncodingMethod = TypeEncoding.Monomorphic;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

+          }

+          return true;

+

+        case "lazyInline":

+          if (ps.ConfirmArgumentCount(1)) {

+            LazyInlining = Int32.Parse(args[ps.i]);

+            if (LazyInlining > 3) ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+          }

+          return true;

+

+        case "procCopyBound":

+          if (ps.ConfirmArgumentCount(1)) {

+            ProcedureCopyBound = Int32.Parse(args[ps.i]);

+          }

+          return true;

+

+        case "stratifiedInline":

+          if (ps.ConfirmArgumentCount(1)) {

+            switch (args[ps.i]) {

+              case "0":

+                StratifiedInlining = 0;

+                break;

+              case "1":

+                StratifiedInlining = 1;

+                break;

+              default:

+                StratifiedInlining = Int32.Parse(cce.NonNull(args[ps.i]));

+                //ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                break;

             }

-            break;

-

-          case "-instrumentInfer":

-          case "/instrumentInfer":

-            if (ps.ConfirmArgumentCount(1)) {

-              switch (args[ps.i]) {

-                case "e":

-                  InstrumentInfer = InstrumentationPlaces.Everywhere;

-                  break;

-                case "h":

-                  InstrumentInfer = InstrumentationPlaces.LoopHeaders;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

+          }

+          return true;

+

+        case "recursionBound":

+          if (ps.ConfirmArgumentCount(1)) {

+            RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));

+          }

+          return true;

+

+        case "coverageReporter":

+          if (ps.ConfirmArgumentCount(1)) {

+            CoverageReporterPath = args[ps.i];

+          }

+          return true;

+

+        case "stratifiedInlineOption":

+          if (ps.ConfirmArgumentCount(1)) {

+            StratifiedInliningOption = Int32.Parse(cce.NonNull(args[ps.i]));

+          }

+          return true;

+

+        case "useUnsatCoreForInlining":

+          UseUnsatCoreForInlining = true;

+          return true;

+

+        case "inferLeastForUnsat":

+          if (ps.ConfirmArgumentCount(1)) {

+            inferLeastForUnsat = args[ps.i];

+          }

+          return true;

+

+        case "typeEncoding":

+          if (ps.ConfirmArgumentCount(1)) {

+            switch (args[ps.i]) {

+              case "n":

+              case "none":

+                TypeEncodingMethod = TypeEncoding.None;

+                break;

+              case "p":

+              case "predicates":

+                TypeEncodingMethod = TypeEncoding.Predicates;

+                break;

+              case "a":

+              case "arguments":

+                TypeEncodingMethod = TypeEncoding.Arguments;

+                break;

+              case "m":

+              case "monomorphic":

+                TypeEncodingMethod = TypeEncoding.Monomorphic;

+                break;

+              default:

+                ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                break;

             }

-            break;

-

-          case "-vcBrackets":

-          case "/vcBrackets":

-            ps.GetNumericArgument(ref BracketIdsInVC, 2);

-            break;

-

-          case "-proverMemoryLimit":

-          case "/proverMemoryLimit": {

-              int d = 0;

-              if (ps.GetNumericArgument(ref d)) {

-                MaxProverMemory = d * Megabyte;

-              }

-              break;

+          }

+          return true;

+

+        case "instrumentInfer":

+          if (ps.ConfirmArgumentCount(1)) {

+            switch (args[ps.i]) {

+              case "e":

+                InstrumentInfer = InstrumentationPlaces.Everywhere;

+                break;

+              case "h":

+                InstrumentInfer = InstrumentationPlaces.LoopHeaders;

+                break;

+              default:

+                ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                break;

             }

+          }

+          return true;

+

+        case "vcBrackets":

+          ps.GetNumericArgument(ref BracketIdsInVC, 2);

+          return true;

 

-          case "-vcsMaxCost":

-          case "/vcsMaxCost":

-            ps.GetNumericArgument(ref VcsMaxCost);

-            break;

-

-          case "-vcsPathJoinMult":

-          case "/vcsPathJoinMult":

-            ps.GetNumericArgument(ref VcsPathJoinMult);

-            break;

-

-          case "-vcsPathCostMult":

-          case "/vcsPathCostMult":

-            ps.GetNumericArgument(ref VcsPathCostMult);

-            break;

-

-          case "-vcsAssumeMult":

-          case "/vcsAssumeMult":

-            ps.GetNumericArgument(ref VcsAssumeMult);

-            break;

-

-          case "-vcsPathSplitMult":

-          case "/vcsPathSplitMult":

-            ps.GetNumericArgument(ref VcsPathSplitMult);

-            break;

-

-          case "-vcsMaxSplits":

-          case "/vcsMaxSplits":

-            ps.GetNumericArgument(ref VcsMaxSplits);

-            break;

-

-          case "-vcsMaxKeepGoingSplits":

-          case "/vcsMaxKeepGoingSplits":

-            ps.GetNumericArgument(ref VcsMaxKeepGoingSplits);

-            break;

-

-          case "-vcsFinalAssertTimeout":

-          case "/vcsFinalAssertTimeout":

-            ps.GetNumericArgument(ref VcsFinalAssertTimeout);

-            break;

-

-          case "-vcsKeepGoingTimeout":

-          case "/vcsKeepGoingTimeout":

-            ps.GetNumericArgument(ref VcsKeepGoingTimeout);

-            break;

-

-          case "-vcsCores":

-          case "/vcsCores":

-            ps.GetNumericArgument(ref VcsCores);

-            break;

-

-          case "-simplifyMatchDepth":

-          case "/simplifyMatchDepth":

-            ps.GetNumericArgument(ref SimplifyProverMatchDepth);

-            break;

-

-          case "-timeLimit":

-          case "/timeLimit":

-            ps.GetNumericArgument(ref ProverKillTime);

-            break;

-

-          case "-smokeTimeout":

-          case "/smokeTimeout":

-            ps.GetNumericArgument(ref SmokeTimeout);

-            break;

-

-          case "-errorLimit":

-          case "/errorLimit":

-            ps.GetNumericArgument(ref ProverCCLimit);

-            break;

-

-          case "-z3opt":

-          case "/z3opt":

-            if (ps.ConfirmArgumentCount(1)) {

-              Z3Options.Add(cce.NonNull(args[ps.i]));

+        case "proverMemoryLimit": {

+            int d = 0;

+            if (ps.GetNumericArgument(ref d)) {

+              MaxProverMemory = d * Megabyte;

             }

-            break;

-

-          case "-z3lets":

-          case "/z3lets":

-            ps.GetNumericArgument(ref Z3lets, 4);

-            break;

-

-          case "-platform":

-          case "/platform":

-            if (ps.ConfirmArgumentCount(1)) {

-              StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]);

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

-                try {

-                  this.TargetPlatform = (PlatformType)cce.NonNull(Enum.Parse(typeof(PlatformType), cce.NonNull(platformOptions[0])));

-                } catch {

-                  ps.Error("Bad /platform type '{0}'", platformOptions[0]);

+            return true;

+          }

+

+        case "vcsMaxCost":

+          ps.GetNumericArgument(ref VcsMaxCost);

+          return true;

+

+        case "vcsPathJoinMult":

+          ps.GetNumericArgument(ref VcsPathJoinMult);

+          return true;

+

+        case "vcsPathCostMult":

+          ps.GetNumericArgument(ref VcsPathCostMult);

+          return true;

+

+        case "vcsAssumeMult":

+          ps.GetNumericArgument(ref VcsAssumeMult);

+          return true;

+

+        case "vcsPathSplitMult":

+          ps.GetNumericArgument(ref VcsPathSplitMult);

+          return true;

+

+        case "vcsMaxSplits":

+          ps.GetNumericArgument(ref VcsMaxSplits);

+          return true;

+

+        case "vcsMaxKeepGoingSplits":

+          ps.GetNumericArgument(ref VcsMaxKeepGoingSplits);

+          return true;

+

+        case "vcsFinalAssertTimeout":

+          ps.GetNumericArgument(ref VcsFinalAssertTimeout);

+          return true;

+

+        case "vcsKeepGoingTimeout":

+          ps.GetNumericArgument(ref VcsKeepGoingTimeout);

+          return true;

+

+        case "vcsCores":

+          ps.GetNumericArgument(ref VcsCores);

+          return true;

+

+        case "simplifyMatchDepth":

+          ps.GetNumericArgument(ref SimplifyProverMatchDepth);

+          return true;

+

+        case "timeLimit":

+          ps.GetNumericArgument(ref ProverKillTime);

+          return true;

+

+        case "smokeTimeout":

+          ps.GetNumericArgument(ref SmokeTimeout);

+          return true;

+

+        case "errorLimit":

+          ps.GetNumericArgument(ref ProverCCLimit);

+          return true;

+

+        case "z3opt":

+          if (ps.ConfirmArgumentCount(1)) {

+            Z3Options.Add(cce.NonNull(args[ps.i]));

+          }

+          return true;

+

+        case "z3lets":

+          ps.GetNumericArgument(ref Z3lets, 4);

+          return true;

+

+        case "platform":

+          if (ps.ConfirmArgumentCount(1)) {

+            StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]);

+            if (platformOptions != null && platformOptions.Count > 0) {

+              try {

+                this.TargetPlatform = (PlatformType)cce.NonNull(Enum.Parse(typeof(PlatformType), cce.NonNull(platformOptions[0])));

+              } catch {

+                ps.Error("Bad /platform type '{0}'", platformOptions[0]);

+                break;

+              }

+              if (platformOptions.Count > 1) {

+                this.TargetPlatformLocation = platformOptions[1];

+                if (!Directory.Exists(platformOptions[1])) {

+                  ps.Error("/platform directory '{0}' does not exist", platformOptions[1]);

                   break;

                 }

-                if (platformOptions.Count > 1) {

-                  this.TargetPlatformLocation = platformOptions[1];

-                  if (!Directory.Exists(platformOptions[1])) {

-                    ps.Error("/platform directory '{0}' does not exist", platformOptions[1]);

-                    break;

-                  }

-                }

               }

             }

-            break;

+          }

+          return true;

 

-          case "-stdlib":

-          case "/stdlib":

-            if (ps.ConfirmArgumentCount(1)) {

-              this.StandardLibraryLocation = args[ps.i];

-            }

-            break;

+        case "z3exe":

+          if (ps.ConfirmArgumentCount(1)) {

+            Z3ExecutablePath = args[ps.i];

+          }

+          return true;

 

-          case "-z3exe":

-          case "/z3exe":

-            if (ps.ConfirmArgumentCount(1)) {

-              Z3ExecutablePath = args[ps.i];

-            }

-            break;

+        case "doBitVectorAnalysis":

+          DoBitVectorAnalysis = true;

+          if (ps.ConfirmArgumentCount(1)) {

+            BitVectorAnalysisOutputBplFile = args[ps.i];

+          }

+          return true;

 

-          case "-doBitVectorAnalysis":

-          case "/doBitVectorAnalysis":

-            DoBitVectorAnalysis = true;

-            if (ps.ConfirmArgumentCount(1)) {

-              BitVectorAnalysisOutputBplFile = args[ps.i];

-            }

-            break;

-

-          default:

-            Contract.Assume(true);

-            bool option = false;

-            if (ps.CheckBooleanFlag("printUnstructured", ref option)) {

-              cce.BeginExpose(this);

-              {

-                PrintUnstructured = option ? 1 : 0;

-              }

-              cce.EndExpose();

-            } else if (

-              ps.CheckBooleanFlag("printDesugared", ref PrintDesugarings) ||

+        default:

+          bool optionValue = false;

+          if (ps.CheckBooleanFlag("printUnstructured", ref optionValue)) {

+            PrintUnstructured = optionValue ? 1 : 0;

+            return true;

+          }

+

+          if (ps.CheckBooleanFlag("printDesugared", ref PrintDesugarings) ||

               ps.CheckBooleanFlag("printInstrumented", ref PrintInstrumented) ||

               ps.CheckBooleanFlag("printWithUniqueIds", ref PrintWithUniqueASTIds) ||

               ps.CheckBooleanFlag("wait", ref Wait) ||

@@ -1369,17 +1194,13 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("overlookTypeErrors", ref OverlookBoogieTypeErrors) ||

               ps.CheckBooleanFlag("noVerify", ref Verify, false) ||

               ps.CheckBooleanFlag("traceverify", ref TraceVerify) ||

-              ps.CheckBooleanFlag("noConsistencyChecks", ref noConsistencyChecks, true) ||

               ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||

               ps.CheckBooleanFlag("nologo", ref DontShowLogo) ||

-              ps.CheckBooleanFlag("noVerifyByDefault", ref NoVerifyByDefault) ||

-              ps.CheckBooleanFlag("useUncheckedContracts", ref UseUncheckedContracts) ||

               ps.CheckBooleanFlag("proverLogAppend", ref SimplifyLogFileAppend) ||

               ps.CheckBooleanFlag("checkInfer", ref InstrumentWithAsserts) ||

               ps.CheckBooleanFlag("interprocInfer", ref IntraproceduralInfer, false) ||

               ps.CheckBooleanFlag("restartProver", ref RestartProverPerVC) ||

               ps.CheckBooleanFlag("printInlined", ref PrintInlined) ||

-              ps.CheckBooleanFlag("arithDistributionAxioms", ref UseArithDistributionAxioms) ||

               ps.CheckBooleanFlag("smoke", ref SoundnessSmokeTest) ||

               ps.CheckBooleanFlag("vcsDumpSplits", ref VcsDumpSplits) ||

               ps.CheckBooleanFlag("dbgRefuted", ref DebugRefuted) ||

@@ -1391,55 +1212,26 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||

               ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis)

               ) {

-              // one of the boolean flags matched

-            } else if (ps.s.StartsWith("-") || ps.s.StartsWith("/")) {

-              ps.Error("unknown switch: {0}", ps.s);

-            } else if (ps.ConfirmArgumentCount(0)) {

-              string filename = ps.s;

-              string extension = Path.GetExtension(filename);

-              if (extension != null) {

-                InputFileExtension = extension.ToLower();

-              }

-              Files.Add(filename);

-              FileName = filename;

-            }

-            break;

-        }

-        cce.BeginExpose(ps);

-        ps.i = ps.nextIndex;

-        cce.EndExpose();

-      }

-

-      Contract.Assume(true);

-      if (ps.encounteredErrors)

-        res *= 2;

-      if (res < 0) {  // help requested

-        Usage();

-      } else if (AttrHelpRequested) {

-        AttributeUsage();

-      } else if (ps.encounteredErrors) {

-        Console.WriteLine("Use /help for available options");

+            // one of the boolean flags matched

+            return true;

+          }

+          break;

       }

 

-      SetProverOptions();

-

-      if (Trace) {

-        BoogieDebug.DoPrinting = true;

-      } // reuse the -trace option for debug printing

-      return res;

+      return base.ParseOption(name, ps);  // defer to superclass

     }

 

-    private void SetProverOptions() {

-      //modifies this.*;

+    protected override void ApplyDefaultOptions() {

       Contract.Ensures(TheProverFactory != null);

       Contract.Ensures(vcVariety != VCVariety.Unspecified);

+

+      base.ApplyDefaultOptions();

+

       // expand macros in filenames, now that LogPrefix is fully determined

-      ExpandFilename(ref XmlSinkFilename);

-      ExpandFilename(ref PrintFile);

-      ExpandFilename(ref DafnyPrelude);

-      ExpandFilename(ref DafnyPrintFile);

-      ExpandFilename(ref SimplifyLogFilePath);

-      ExpandFilename(ref PrintErrorModelFile);

+      ExpandFilename(ref XmlSinkFilename, LogPrefix, FileTimestamp);

+      ExpandFilename(ref PrintFile, LogPrefix, FileTimestamp);

+      ExpandFilename(ref SimplifyLogFilePath, LogPrefix, FileTimestamp);

+      ExpandFilename(ref PrintErrorModelFile, LogPrefix, FileTimestamp);

 

       Contract.Assume(XmlSink == null);  // XmlSink is to be set here

       if (XmlSinkFilename != null) {

@@ -1447,42 +1239,14 @@ namespace Microsoft.Boogie {
       }

 

       if (TheProverFactory == null) {

-        cce.BeginExpose(this);

-        {

-          TheProverFactory = ProverFactory.Load("SMTLIB");

-          ProverName = "SMTLIB".ToUpper();

-        }

-        cce.EndExpose();

+        TheProverFactory = ProverFactory.Load("SMTLIB");

+        ProverName = "SMTLIB".ToUpper();

       }

 

       if (vcVariety == VCVariety.Unspecified) {

         vcVariety = TheProverFactory.DefaultVCVariety;

       }

 

-      if (LoopFrameConditions == -1) {

-        // /modifiesOnLoop not specified.  Set its default depending on /localModifiesChecks

-        if (LocalModifiesChecks) {

-          LoopFrameConditions = 1;

-        } else {

-          LoopFrameConditions = 2;

-        }

-      }

-

-      switch (InductiveMinMax) {

-        case 1:

-        case 2:

-        case 4:

-        case 5:

-          ReflectAdd = true;  // these InductiveMinMax modes imply ReflectAdd

-          break;

-        default:

-          break;

-      }

-

-      if (MethodologySelection == Methodology.VisibleState) {

-        OwnershipModelEncoding = OwnershipModelOption.Trivial;

-      }

-

       if (UseArrayTheory) {

         Monomorphize = true;

       }

@@ -1493,9 +1257,8 @@ namespace Microsoft.Boogie {
         UseAbstractInterpretation = false;

       }

 

-      if (inferLeastForUnsat != null)

-      {

-          StratifiedInlining = 1;

+      if (inferLeastForUnsat != null) {

+        StratifiedInlining = 1;

       }

 

       if (StratifiedInlining > 0) {

@@ -1503,30 +1266,17 @@ namespace Microsoft.Boogie {
         UseArrayTheory = true;

         UseAbstractInterpretation = false;

         MaxProverMemory = 0; // no max: avoids restarts

-        if (ProverName == "Z3API" || ProverName == "SMTLIB")

-        {

-            ProverCCLimit = 1;

+        if (ProverName == "Z3API" || ProverName == "SMTLIB") {

+          ProverCCLimit = 1;

         }

       }

-    }

-

-

 

-    public bool UserWantsMethodLogging(string methodFullName) {

-      Contract.Requires(methodFullName != null);

-      if (methodToLog == null) {

-        return false;

+      if (Trace) {

+        BoogieDebug.DoPrinting = true;  // reuse the -trace option for debug printing

       }

-      return methodToLog == "*" || methodFullName.IndexOf(methodToLog) >= 0;

     }

 

-    public bool UserWantsToBreak(string methodFullName) {

-      Contract.Requires(methodFullName != null);

-      if (methodToBreakOn == null) {

-        return false;

-      }

-      return methodFullName.IndexOf(methodToBreakOn) >= 0;

-    }

+

 

     public bool UserWantsToCheckRoutine(string methodFullname) {

       Contract.Requires(methodFullname != null);

@@ -1537,284 +1287,6 @@ namespace Microsoft.Boogie {
       return Contract.Exists(ProcsToCheck, s => 0 <= methodFullname.IndexOf(s));

     }

 

-#if CCI

-    public bool UserWantsToTranslateRoutine(Cci.Method method, string methodFullname) {

-      Contract.Requires(methodFullname != null);

-      Contract.Requires(method != null);

-      return UserWantsToTranslateRoutineInclude(method, methodFullname) &&

-        !Contract.Exists(methodsToTranslateExclude, s => 0 <= methodFullname.IndexOf(s));

-    }

-

-    public bool UserWantsToTranslateRoutineInclude(Cci.Method method, string methodFullname) {

-      Contract.Requires(methodFullname != null);

-      Contract.Requires(method != null);

-      if (methodsToTranslateSubstring == null &&

-          methodsToTranslateClass == null &&

-          methodsToTranslateClassQualified == null &&

-          methodsToTranslateFile == null &&

-          methodsToTranslateMethod == null &&

-          methodsToTranslateMethodQualified == null) {

-        // no preference

-        return true;

-      }

-      if (methodsToTranslateSubstring != null) {

-        if (Contract.Exists(methodsToTranslateSubstring, s => 0 <= methodFullname.IndexOf(s))) {

-          return true;

-        }

-      }

-      if (methodsToTranslateMethod != null) {

-        string methodName = method.Name.Name;

-        Contract.Assert(methodsToTranslateMethod != null);

-        if (methodsToTranslateMethod.Contains(methodName)) {

-          return true;

-        }

-      }

-      if (methodsToTranslateMethodQualified != null && method.DeclaringType != null) {

-        string methodName = method.DeclaringType.Name.Name + "." + method.Name.Name;

-        Contract.Assert(methodsToTranslateMethodQualified != null);

-        if (methodsToTranslateMethodQualified.Contains(methodName)) {

-          return true;

-        }

-      }

-      if (method.DeclaringType != null) {

-        if (methodsToTranslateClass != null) {

-          string className = method.DeclaringType.Name.Name;

-          if (methodsToTranslateClass.Contains(className)) {

-            return true;

-          }

-        }

-        if (methodsToTranslateClassQualified != null) {

-          string className = method.DeclaringType.FullName;

-          if (className != null) {

-            className = className.Replace('+', '.');

-            if (methodsToTranslateClassQualified.Contains(className)) {

-              return true;

-            }

-          }

-        }

-      }

-      if (methodsToTranslateFile != null) {

-        string methodFilename = GetSourceDocument(method);

-        if (methodFilename != null) {

-          string path = methodFilename;

-          if (path != null) {

-            string filename = Path.GetFileName(path);

-            if (methodsToTranslateFile.Contains(filename)) {

-              return true;

-            }

-          }

-        }

-      }

-      // the method is not among the desired routines

-      return false;

-    }

-

-    /// <summary>

-    /// Returns the file containing "method".  Returns null f that information is not available.

-    /// </summary>

-    static string GetSourceDocument(Cci.Method method) {

-      Contract.Requires(method != null);

-      // Start by looking for a source context in the method itself.  However, if the program

-      // was read from a binary, then there is no source location for the method.  If so, there

-      // some other ways we might find a source location.

-      if (method.SourceContext.Document != null) {

-        return method.SourceContext.Document.Name;

-      }

-      // Try to find a source location in the method's contract

-      if (method.Contract != null) {

-        if (method.Contract.Requires != null) {

-          foreach (Cci.Requires c in method.Contract.Requires) {

-            if (c != null && c.SourceContext.Document != null) {

-              return c.SourceContext.Document.Name;

-            }

-          }

-        }

-        if (method.Contract.Modifies != null) {

-          foreach (Cci.Expression c in method.Contract.Modifies) {

-            if (c != null && c.SourceContext.Document != null) {

-              return c.SourceContext.Document.Name;

-            }

-          }

-        }

-        if (method.Contract.Ensures != null) {

-          foreach (Cci.Ensures c in method.Contract.Ensures) {

-            if (c != null && c.SourceContext.Document != null) {

-              return c.SourceContext.Document.Name;

-            }

-          }

-        }

-      }

-      // As a last attempt, look for a source location among the statements

-      if (method.Body != null) {

-        return GetSourceDocumentFromStatements(method.Body.Statements);

-      }

-      return null;  // no source location found

-    }

-

-    [Pure]

-    static string GetSourceDocumentFromStatements(Cci.StatementList list) {

-      if (list != null) {

-        foreach (Cci.Statement c in list) {

-          if (c != null && c.SourceContext.Document != null) {

-            return c.SourceContext.Document.Name;

-          }

-          if (c is Cci.Block) {

-            Cci.Block b = (Cci.Block)c;

-            string n = GetSourceDocumentFromStatements(b.Statements);

-            if (n != null) {

-              return n;

-            }

-          }

-        }

-      }

-      return null;

-    }

-#endif

-

-    class CommandLineParseState {

-      public string s;

-      public bool hasColonArgument;

-      public readonly string[]/*!*/ args;

-      public int i;

-      public int nextIndex;

-      public bool encounteredErrors;

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(args != null);

-        Contract.Invariant(0 <= i && i <= args.Length);

-        Contract.Invariant(0 <= nextIndex && nextIndex <= args.Length);

-

-      }

-

-

-

-      public CommandLineParseState(string[] args) {

-        Contract.Requires(args != null);

-        Contract.Requires(Contract.ForAll(0, args.Length, i => args[i] != null));

-        Contract.Ensures(this.args == args);

-        this.s = null;  // set later by client

-        this.hasColonArgument = false;  // set later by client

-        this.args = args;

-        this.i = 0;

-        this.nextIndex = 0;  // set later by client

-        this.encounteredErrors = false;

-      }

-

-      public bool CheckBooleanFlag(string flagName, ref bool flag, bool valueWhenPresent) {

-        Contract.Requires(flagName != null);

-        //modifies nextIndex, encounteredErrors, Console.Error.*;

-        bool flagPresent = false;

-

-        if ((s == "/" + flagName || s == "-" + flagName) && ConfirmArgumentCount(0)) {

-          flag = valueWhenPresent;

-          flagPresent = true;

-        }

-        return flagPresent;

-      }

-

-      public bool CheckBooleanFlag(string flagName, ref bool flag) {

-        Contract.Requires(flagName != null);

-        //modifies nextIndex, encounteredErrors, Console.Error.*;

-        return CheckBooleanFlag(flagName, ref flag, true);

-      }

-

-      /// <summary>

-      /// If there is one argument and it is a non-negative integer, then set "arg" to that number and return "true".

-      /// Otherwise, emit error message, leave "arg" unchanged, and return "false".

-      /// </summary>

-      public bool GetNumericArgument(ref int arg) {

-        //modifies nextIndex, encounteredErrors, Console.Error.*;

-        if (this.ConfirmArgumentCount(1)) {

-          try {

-            Contract.Assume(args[i] != null);

-            Contract.Assert(args[i] is string);  // needed to prove args[i].IsPeerConsistent

-            int d = Convert.ToInt32(this.args[this.i]);

-            if (0 <= d) {

-              arg = d;

-              return true;

-            }

-          } catch (System.FormatException) {

-          } catch (System.OverflowException) {

-          }

-        } else {

-          return false;

-        }

-        Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);

-        return false;

-      }

-

-      /// <summary>

-      /// If there is one argument and it is a non-negative integer less than "limit",

-      /// then set "arg" to that number and return "true".

-      /// Otherwise, emit error message, leave "arg" unchanged, and return "false".

-      /// </summary>

-      public bool GetNumericArgument(ref int arg, int limit) {

-        Contract.Requires(this.i < args.Length);

-        //modifies nextIndex, encounteredErrors, Console.Error.*;

-        int a = arg;

-        if (!GetNumericArgument(ref a)) {

-          return false;

-        } else if (a < limit) {

-          arg = a;

-          return true;

-        } else {

-          Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);

-          return false;

-        }

-      }

-

-      /// <summary>

-      /// If there is one argument and it is a non-negative real, then set "arg" to that number and return "true".

-      /// Otherwise, emit an error message, leave "arg" unchanged, and return "false".

-      /// </summary>

-      public bool GetNumericArgument(ref double arg) {

-        //modifies nextIndex, encounteredErrors, Console.Error.*;

-        if (this.ConfirmArgumentCount(1)) {

-          try {

-            Contract.Assume(args[i] != null);

-            Contract.Assert(args[i] is string);  // needed to prove args[i].IsPeerConsistent

-            double d = Convert.ToDouble(this.args[this.i]);

-            if (0 <= d) {

-              arg = d;

-              return true;

-            }

-          } catch (System.FormatException) {

-          } catch (System.OverflowException) {

-          }

-        } else {

-          return false;

-        }

-        Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s);

-        return false;

-      }

-

-      public bool ConfirmArgumentCount(int argCount) {

-        Contract.Requires(0 <= argCount);

-        //modifies nextIndex, encounteredErrors, Console.Error.*;

-        Contract.Ensures(Contract.Result<bool>() == (!(hasColonArgument && argCount != 1) && !(args.Length < i + argCount)));

-        if (hasColonArgument && argCount != 1) {

-          Error("\"{0}\" cannot take a colon argument", s);

-          nextIndex = args.Length;

-          return false;

-        } else if (args.Length < i + argCount) {

-          Error("\"{0}\" expects {1} argument{2}", s, argCount.ToString(), (string)(argCount == 1 ? "" : "s"));

-          nextIndex = args.Length;

-          return false;

-        } else {

-          nextIndex = i + argCount;

-          return true;

-        }

-      }

-

-      public void Error(string message, params string[] args) {

-        Contract.Requires(args != null);

-        Contract.Requires(message != null);

-        //modifies encounteredErrors, Console.Error.*;

-        Console.Error.WriteLine("Boogie: Error: " + String.Format(message, args));

-        encounteredErrors = true;

-      }

-    }

-

     public virtual StringCollection ParseNamedArgumentList(string argList) {

       if (argList == null || argList.Length == 0)

         return null;

@@ -1848,7 +1320,7 @@ namespace Microsoft.Boogie {
       return semicolonIndex;

     }

 

-    public static void AttributeUsage() {

+    public override void AttributeUsage() {

       Console.WriteLine(

 @"Boogie: The following attributes are supported by this implementation.

 

@@ -1928,138 +1400,14 @@ namespace Microsoft.Boogie {
 ");

     }

 

-    private static bool printedHelp = false;

-

-    public static void Usage() {

-      // Ensure that we only print the help message once,

-      // no matter how many enabling conditions for printing

-      // help were triggered.

-      if (printedHelp) {

-        return;

-      }

-      printedHelp = true;

-

-      Console.WriteLine(@"Boogie: usage:  Boogie [ option ... ] [ filename ... ]

-  where <option> is one of

-

-  ---- General options -------------------------------------------------------

-

-  /help          : this message

-  /attrHelp      : print a message about declaration attributes supported by

-                   this implementation

-  /nologo        : suppress printing of version number, copyright message

-  /env:<n>       : print command line arguments

-                   0 - never, 1 (default) - during BPL print and prover log,

-                   2 - like 1 and also to standard output

-  /wait          : await Enter from keyboard before terminating program

-  /xml:<file>    : also produce output in XML format to <file>

-

-  ---- Spec# options ---------------------------------------------------------

-

-  If any of the following switches is included, only those methods specified

-  by some switch are translated into Boogie.  Furthermore, a method is

-  not translated if a [Verify(false)] attribute applies to it or if the

-  flag /trExclude applies (see below).

-  /translate:<str> : include method if its full name contains substring <str>

-  /trMethod:<method> : include method if its name is <method>

-                       Format:  Name or Class.Name

-  /trClass:<class>   : include method if the enclosing class is <class>

-                       Format:  Name or Qualification.Name

-  /trFile:<filename> : include method if it is contained in file <filename>

-                       Format:  Filename.ssc

-

-  /trExclude:<str> : exclude method it its full name contains substring <str>

-

-  /c[ontracts]:<file>

-                 : apply the contracts from <file> to

-                   the referenced assemblies of the input assembly.

-                   Note: the contracts for Xyz must be in Xyz.Contracts

-  /methodology:<m> : selects the specification and verification methodology

-                   b = boogie (default)

-                   vs = visible-state

-  /level:<n>     : 0 - reduced checks,

-                   1 - no modifies checking, 2 - full (default)

-  /useUncheckedContracts : generate purity axioms even when the postconditions

-                   could not be checked to be sound (this option only for

-                   experts and dare devils)

-  /modifiesDefault:<n> :

-                   0 - just what is declared

-                   1 - what is declared plus E.snapshot for every top-level

-                       E.f, E.*, E.**, E[i], or E[*] in the modifies clause

-                   2 - (1) but also for nested E's

-                   3 - (1) plus this.snapshot

-                   4 - (2) plus this.snapshot

-                   5 - (default) (1) plus p.* for receiver parameter p not

-                       occurring at the top-level of modifies clause as

-                       p.f, p.*, p.**, p[i], p[*], or p.0

-                   6 - (5) but for every parameter p

-  /modifiesOnLoop:<n> : 0 - never, 1 - assume only (default),

-                        2 - assume and check (default with

-                            /localModifiesChecks:0)

-  /localModifiesChecks: 0 - check modifies-clause as post-condition of a

-                            procedure

-                        1 - check violations of modifies-clause at each

-                            assignment and method call (default)

-  /loopUnroll:<n>  : unroll loops, following up to n back edges (and then some)

-  /noVerifyByDefault : change the default to [Verify(false)]

-  /orderStrength:<n> : 0 (default) - only few properties of subtyping

-                                     axiomatized,

-                       1 - full strength

-  /summationStrength:<n> : 0 - less applicable triggers in the axioms

-                           1 - (default) default set of axioms for summation-

-                           like quantifiers;

-  /arithDistributionAxioms : emit +/* distribution axioms

-  /inductiveMinMax:<n> : 0 (default) - extreme axioms for min/max;

-                         1 - inductive axioms for min/max;

-                         2 - both extreme and inductive axioms for min/max

-                         3,4,5 - like 0,1,2 but adding the plus-over-min/max

-                             distribution axiom

-                         Modes 1,2,4,5 imply /reflectAdd.

-  /fcoStrength:<n> : adjusts the amount of information encoded about 'first

-                     consistent owners'

-                     0 - no FCO axiom, 1 - cheaper but weaker FCO axiom,

-                     2 - pure-method FCO axiom,

-                     3, 4, 5 (default) - like 0,1,2 plus more specific

-                       FCO information on pure-method return

-  /ownerModelEncoding:<enc> : s = standard (default)

-                              e = experimental

-                              t = trivial (implied by /methodology:vs)

-  /printModel:<n> : 0 (default) - do not print Z3's error model

-                    1 - print Z3's error model

-                    2 - print Z3's error model plus reverse mappings

-                    4 - print Z3's error model in a more human readable way

-  /printModelToFile:<file> : print model to <file> instead of console

-  /mv:<file>        Specify file where to save the model in BVD format

-  /enhancedErrorMessages:<n> : 0 (default) - no enhanced error messages

-                               1 - Z3 error model enhanced error messages

-

-  ---- Dafny options ---------------------------------------------------------

-

-  Multiple .dfy files supplied on the command line are concatenated into one

-  Dafny program.

-

-  /dprelude:<file> : choose Dafny prelude file

-  /dprint:<file> : print Dafny program after parsing it

-                   (use - as <file> to print to console)

-  /compile:<n>   : 0 - do not compile Dafny program

-                   1 (default) - upon successful verification of the Dafny

-                       program, compile Dafny program to C# program out.cs

-                   2 - always attempt to compile Dafny program to C# program

-                       out.cs, regardless of verification outcome

-  /noCheating:<n> : 0 (default) - allow assume statements and free invariants

-                    1 - treat all assumptions as asserts, and drop free.

-  /induction:<n> : 0 - never do induction, not even when attributes request it

-                   1 - only apply induction when attributes request it

-                   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

-  /inductionHeuristic: 0 - least discriminating induction heuristic (that is,

-                           lean toward applying induction more often)

-                       1,2,3,4,5 - levels in between, ordered as follows as

-                           far as how discriminating they are:

-                           0 < 1 < 2 < (3,4) < 5 < 6

-                       6 (default) - most discriminating

+    public override void Usage() {

+      Console.WriteLine(@"

+  /nologo       suppress printing of version number, copyright message

+  /env:<n>      print command line arguments

+                  0 - never, 1 (default) - during BPL print and prover log,

+                  2 - like 1 and also to standard output

+  /wait         await Enter from keyboard before terminating program

+  /xml:<file>   also produce output in XML format to <file>

 

   ---- Boogie options --------------------------------------------------------

 

@@ -2080,10 +1428,25 @@ namespace Microsoft.Boogie {
   /overlookTypeErrors : skip any implementation with resolution or type

                         checking errors

 

+  /loopUnroll:<n>

+                unroll loops, following up to n back edges (and then some)

+  /printModel:<n>

+                0 (default) - do not print Z3's error model

+                1 - print Z3's error model

+                2 - print Z3's error model plus reverse mappings

+                4 - print Z3's error model in a more human readable way

+  /printModelToFile:<file>

+                print model to <file> instead of console

+  /mv:<file>    Specify file where to save the model in BVD format

+  /enhancedErrorMessages:<n>

+                0 (default) - no enhanced error messages

+                1 - Z3 error model enhanced error messages

+

   ---- Inference options -----------------------------------------------------

 

-  /infer:<flags> : use abstract interpretation to infer invariants

-                   The default is /infer:i"

+  /infer:<flags>

+                use abstract interpretation to infer invariants

+                The default is /infer:i"

         // This is not 100% true, as the /infer ALWAYS creates

         // a multilattice, whereas if nothing is specified then

         // intervals are isntantiated WITHOUT being embedded in

@@ -2097,185 +1460,228 @@ namespace Microsoft.Boogie {
                    p = polyhedra for linear inequalities

                    s = debug statistics

                 0..9 = number of iterations before applying a widen (default=0)

-  /noinfer       : turn off the default inference, and overrides the /infer

-                   switch on its left

-  /checkInfer    : instrument inferred invariants as asserts to be checked by

-                   theorem prover

-  /interprocInfer : perform interprocedural inference (deprecated, not

-                    supported)

-  /contractInfer : perform procedure contract inference

-  /logInfer      : print debug output during inference

-  /instrumentInfer : h - instrument inferred invariants only at beginning of

-                         loop headers (default)

-                     e - instrument inferred invariants at beginning and end

-                         of every block

-  /printInstrumented : print Boogie program after it has been

-                   instrumented with invariants

+  /noinfer      turn off the default inference, and overrides the /infer

+                switch on its left

+  /checkInfer   instrument inferred invariants as asserts to be checked by

+                theorem prover

+  /interprocInfer

+                perform interprocedural inference (deprecated, not supported)

+  /contractInfer

+                perform procedure contract inference

+  /logInfer     print debug output during inference

+  /instrumentInfer

+                h - instrument inferred invariants only at beginning of

+                    loop headers (default)

+                e - instrument inferred invariants at beginning and end

+                    of every block

+  /printInstrumented

+                print Boogie program after it has been instrumented with

+                invariants

 

   ---- Debugging and general tracing options ---------------------------------

 

-  /trace         : blurt out various debug trace information

-  /traceTimes    : output timing information at certain points in the pipeline

-  /log[:method]  : Print debug output during translation

+  /trace        blurt out various debug trace information

+  /traceTimes   output timing information at certain points in the pipeline

+  /log[:method] Print debug output during translation

 

-  /break[:method] : break into debugger

+  /break        launch and break into debugger

 

   ---- Verification-condition generation options -----------------------------

 

-  /liveVariableAnalysis:<c> : 0 = do not perform live variable analysis

-                              1 = perform live variable analysis (default)

-                              2 = perform interprocedural live variable analysis

-  /noVerify      : skip VC generation and invocation of the theorem prover

-  /removeEmptyBlocks:<c> : 0 - do not remove empty blocks during VC generation

-                           1 - remove empty blocks (default)

-  /coalesceBlocks:<c> : 0 = do not coalesce blocks

-                        1 = coalesce blocks (default)

-  /vc:<variety>  : n = nested block (default for /prover:Simplify),

-                   m = nested block reach,

-                   b = flat block, r = flat block reach,

-                   s = structured, l = local,

-                   d = dag (default, except with /prover:Simplify)

-                   doomed = doomed

-  /traceverify   : print debug output during verification condition generation

-  /subsumption:<c> : apply subsumption to asserted conditions:

-                    0 - never, 1 - not for quantifiers, 2 (default) - always

-  /alwaysAssumeFreeLoopInvariants : usually, a free loop invariant (or assume

-                   statement in that position) is ignored in checking contexts

-                   (like other free things); this option includes these free

-                   loop invariants as assumes in both contexts

-  /inline:<i>    : use inlining strategy <i> for procedures with the :inline

-                   attribute, see /attrHelp for details:

-                   none

-                   assume (default)

-                   assert

-                   spec

-  /printInlined  : print the implementation after inlining calls to

-                   procedures with the :inline attribute (works with /inline)

-  /lazyInline:1  : Use the lazy inlining algorithm

-  /stratifiedInline:1 : Use the stratified inlining algorithm

-  /recursionBound:<n> : Set the recursion bound for stratified inlining to

-                        be n (default 500)

-  /inferLeastForUnsat:<str> : Infer the least number of constants (whose names

-                              are prefixed by <str>) that need to be set to

-                              true for the program to be correct. This turns

-                              on stratified inlining.

-  /smoke         : Soundness Smoke Test: try to stick assert false; in some

-                   places in the BPL and see if we can still prove it

-  /smokeTimeout:<n> : Timeout, in seconds, for a single theorem prover

-                   invocation during smoke test, defaults to 10.

-  /causalImplies : Translate Boogie's A ==> B into prover's A ==> A && B.

-  /typeEncoding:<m> : how to encode types when sending VC to theorem prover

+  /liveVariableAnalysis:<c>

+                0 = do not perform live variable analysis

+                1 = perform live variable analysis (default)

+                2 = perform interprocedural live variable analysis

+  /noVerify     skip VC generation and invocation of the theorem prover

+  /removeEmptyBlocks:<c>

+                0 - do not remove empty blocks during VC generation

+                1 - remove empty blocks (default)

+  /coalesceBlocks:<c>

+                0 = do not coalesce blocks

+                1 = coalesce blocks (default)

+  /vc:<variety> n = nested block (default for /prover:Simplify),

+                m = nested block reach,

+                b = flat block, r = flat block reach,

+                s = structured, l = local,

+                d = dag (default, except with /prover:Simplify)

+                doomed = doomed

+  /traceverify  print debug output during verification condition generation

+  /subsumption:<c>

+                apply subsumption to asserted conditions:

+                0 - never, 1 - not for quantifiers, 2 (default) - always

+  /alwaysAssumeFreeLoopInvariants

+                usually, a free loop invariant (or assume

+                statement in that position) is ignored in checking contexts

+                (like other free things); this option includes these free

+                loop invariants as assumes in both contexts

+  /inline:<i>   use inlining strategy <i> for procedures with the :inline

+                attribute, see /attrHelp for details:

+                  none

+                  assume (default)

+                  assert

+                  spec

+  /printInlined

+                print the implementation after inlining calls to

+                procedures with the :inline attribute (works with /inline)

+  /lazyInline:1

+                Use the lazy inlining algorithm

+  /stratifiedInline:1

+                Use the stratified inlining algorithm

+  /recursionBound:<n>

+                Set the recursion bound for stratified inlining to

+                be n (default 500)

+  /inferLeastForUnsat:<str>

+                Infer the least number of constants (whose names

+                are prefixed by <str>) that need to be set to

+                true for the program to be correct. This turns

+                on stratified inlining.

+  /smoke        Soundness Smoke Test: try to stick assert false; in some

+                places in the BPL and see if we can still prove it

+  /smokeTimeout:<n>

+                Timeout, in seconds, for a single theorem prover

+                invocation during smoke test, defaults to 10.

+  /causalImplies

+                Translate Boogie's A ==> B into prover's A ==> A && B.

+  /typeEncoding:<m>

+                how to encode types when sending VC to theorem prover

                    n = none (unsound)

                    p = predicates (default)

                    a = arguments

-  /monomorphize    Do not abstract map types in the encoding (this is an

-                   experimental feature that will not do the right thing if

-                   the program uses polymorphism)

-  /reflectAdd      In the VC, generate an auxiliary symbol, elsewhere defined

-                   to be +, instead of +.

+  /monomorphize   

+                Do not abstract map types in the encoding (this is an

+                experimental feature that will not do the right thing if

+                the program uses polymorphism)

+  /reflectAdd   In the VC, generate an auxiliary symbol, elsewhere defined

+                to be +, instead of +.

 

   ---- Verification-condition splitting --------------------------------------

 

-  /vcsMaxCost:<f>   : VC will not be split unless the cost of a VC exceeds this

-                      number, defaults to 2000.0. This does NOT apply in the

-                      keep-going mode after first round of splitting.

-  /vcsMaxSplits:<n> : Maximal number of VC generated per method. In keep

-                      going mode only applies to the first round.

-                      Defaults to 1.

-  /vcsMaxKeepGoingSplits:<n> : If set to more than 1, activates the keep

-                      going mode, where after the first round of splitting,

-                      VCs that timed out are split into <n> pieces and retried

-                      until we succeed proving them, or there is only one

-                      assertion on a single path and it timeouts (in which

-                      case error is reported for that assertion).

-                      Defaults to 1.

-  /vcsKeepGoingTimeout:<n> : Timeout in seconds for a single theorem prover

-                      invocation in keep going mode, except for the final

-                      single-assertion case. Defaults to 1s.

-  /vcsFinalAssertTimeout:<n> : Timeout in seconds for the single last

-                      assertion in the keep going mode. Defaults to 30s.

-  /vcsPathJoinMult:<f> : If more than one path join at a block, by how much

-                      multiply the number of paths in that block, to accomodate

-                      for the fact that the prover will learn something on one

-                      paths, before proceeding to another. Defaults to 0.8.

+  /vcsMaxCost:<f>

+                VC will not be split unless the cost of a VC exceeds this

+                number, defaults to 2000.0. This does NOT apply in the

+                keep-going mode after first round of splitting.

+  /vcsMaxSplits:<n>

+                Maximal number of VC generated per method. In keep

+                going mode only applies to the first round.

+                Defaults to 1.

+  /vcsMaxKeepGoingSplits:<n>

+                If set to more than 1, activates the keep

+                going mode, where after the first round of splitting,

+                VCs that timed out are split into <n> pieces and retried

+                until we succeed proving them, or there is only one

+                assertion on a single path and it timeouts (in which

+                case error is reported for that assertion).

+                Defaults to 1.

+  /vcsKeepGoingTimeout:<n>

+                Timeout in seconds for a single theorem prover

+                invocation in keep going mode, except for the final

+                single-assertion case. Defaults to 1s.

+  /vcsFinalAssertTimeout:<n>

+                Timeout in seconds for the single last

+                assertion in the keep going mode. Defaults to 30s.

+  /vcsPathJoinMult:<f>

+                If more than one path join at a block, by how much

+                multiply the number of paths in that block, to accomodate

+                for the fact that the prover will learn something on one

+                paths, before proceeding to another. Defaults to 0.8.

   /vcsPathCostMult:<f1>

-  /vcsAssumeMult:<f2> : The cost of a block is

-         (<assert-cost> + <f2>*<assume-cost>)*(1.0 + <f1>*<entering-paths>)

-                      <f1> defaults to 1.0, <f2> defaults to 0.01.

-                      The cost of a single assertion or assumption is

-                      currently always 1.0.

-  /vcsPathSplitMult:<f> : If the best path split of a VC of cost A is into

-                      VCs of cost B and C, then the split is applied if

-                      A >= <f>*(B+C), otherwise assertion splitting will be

-                      applied. Defaults to 0.5 (always do path splitting if

-                      possible), set to more to do less path splitting

-                      and more assertion splitting.

-  /vcsDumpSplits      For split #n dump split.n.dot and split.n.bpl.

-                      Warning: Affects error reporting.

-  /vcsCores:<n>     : Try to verify <n> VCs at once. Defaults to 1.

+  /vcsAssumeMult:<f2>

+                The cost of a block is

+                    (<assert-cost> + <f2>*<assume-cost>) * 

+                    (1.0 + <f1>*<entering-paths>)

+                <f1> defaults to 1.0, <f2> defaults to 0.01.

+                The cost of a single assertion or assumption is

+                currently always 1.0.

+  /vcsPathSplitMult:<f>

+                If the best path split of a VC of cost A is into

+                VCs of cost B and C, then the split is applied if

+                A >= <f>*(B+C), otherwise assertion splitting will be

+                applied. Defaults to 0.5 (always do path splitting if

+                possible), set to more to do less path splitting

+                and more assertion splitting.

+  /vcsDumpSplits

+                For split #n dump split.n.dot and split.n.bpl.

+                Warning: Affects error reporting.

+  /vcsCores:<n>

+                Try to verify <n> VCs at once. Defaults to 1.

 

   ---- Prover options --------------------------------------------------------

 

-  /errorLimit:<num> : Limit the number of errors produced for each procedure

-                      (default is 5, some provers may support only 1)

-  /timeLimit:<num>  : Limit the number of seconds spent trying to verify

-                      each procedure

-  /errorTrace:<n> : 0 - no Trace labels in the error output,

-                    1 (default) - include useful Trace labels in error output,

-                    2 - include all Trace labels in the error output

-  /vcBrackets:<b> : bracket odd-charactered identifier names with |'s.  <b> is:

+  /errorLimit:<num>

+                Limit the number of errors produced for each procedure

+                (default is 5, some provers may support only 1)

+  /timeLimit:<num>

+                Limit the number of seconds spent trying to verify

+                each procedure

+  /errorTrace:<n>

+                0 - no Trace labels in the error output,

+                1 (default) - include useful Trace labels in error output,

+                2 - include all Trace labels in the error output

+  /vcBrackets:<b>

+                bracket odd-charactered identifier names with |'s.  <b> is:

                    0 - no (default with non-/prover:Simplify),

                    1 - yes (default with /prover:Simplify)

-  /prover:<tp>   : use theorem prover <tp>, where <tp> is either the name of

-                   a DLL containing the prover interface located in the

-                   Boogie directory, or a full path to a DLL containing such

-                   an interface. The standard interfaces shipped include:

-                     SMTLib (default, uses the SMTLib2 format and calls Z3)

-                     Z3 (uses Z3 with the Simplify format)

-                     Simplify

-                     ContractInference (uses Z3)

-                     Z3api (Z3 using Managed .NET API)

-  /proverOpt:KEY[=VALUE] : Provide a prover-specific option (short form /p).

-  /proverLog:<file> : Log input for the theorem prover.  Like filenames

-                   supplied as arguments to other options, <file> can use the

-                   following macros:

-                     @TIME@    expands to the current time

-                     @PREFIX@  expands to the concatenation of strings given

-                               by /logPrefix options

-                     @FILE@    expands to the last filename specified on the

-                               command line

-                   In addition, /proverLog can also use the macro '@PROC@',

-                   which causes there to be one prover log file per

-                   verification condition, and the macro then expands to the

-                   name of the procedure that the verification condition is

-                   for.

-  /logPrefix:<str> : Defines the expansion of the macro '@PREFIX@', which can

-                   be used in various filenames specified by other options.

-  /proverLogAppend : Append (not overwrite) the specified prover log file

-  /proverWarnings : 0 (default) - don't print, 1 - print to stdout,

-                    2 - print to stderr

-  /proverMemoryLimit:<num>  : Limit on the virtual memory for prover before

-                             restart in MB (default:100MB)

-  /restartProver            : Restart the prover after each query

-  /proverShutdownLimit<num> : Time between closing the stream to the prover and

-                              killing the prover process (default: 0s)

+  /prover:<tp>  use theorem prover <tp>, where <tp> is either the name of

+                a DLL containing the prover interface located in the

+                Boogie directory, or a full path to a DLL containing such

+                an interface. The standard interfaces shipped include:

+                    SMTLib (default, uses the SMTLib2 format and calls Z3)

+                    Z3 (uses Z3 with the Simplify format)

+                    Simplify

+                    ContractInference (uses Z3)

+                    Z3api (Z3 using Managed .NET API)

+  /proverOpt:KEY[=VALUE]

+                Provide a prover-specific option (short form /p).

+  /proverLog:<file>

+                Log input for the theorem prover.  Like filenames

+                supplied as arguments to other options, <file> can use the

+                following macros:

+                    @TIME@    expands to the current time

+                    @PREFIX@  expands to the concatenation of strings given

+                              by /logPrefix options

+                    @FILE@    expands to the last filename specified on the

+                              command line

+                In addition, /proverLog can also use the macro '@PROC@',

+                which causes there to be one prover log file per

+                verification condition, and the macro then expands to the

+                name of the procedure that the verification condition is for.

+  /logPrefix:<str>

+                Defines the expansion of the macro '@PREFIX@', which can

+                be used in various filenames specified by other options.

+  /proverLogAppend

+                Append (not overwrite) the specified prover log file

+  /proverWarnings

+                0 (default) - don't print, 1 - print to stdout,

+                2 - print to stderr

+  /proverMemoryLimit:<num>

+                Limit on the virtual memory for prover before

+                restart in MB (default:100MB)

+  /restartProver

+                Restart the prover after each query

+  /proverShutdownLimit<num>

+                Time between closing the stream to the prover and

+                killing the prover process (default: 0s)

   /platform:<ptype>,<location>

-                 : ptype = v11,v2,cli1

-                 : location = platform libraries directory

+                ptype = v11,v2,cli1

+                location = platform libraries directory

 

   Simplify specific options:

-  /simplifyMatchDepth:<num> : Set Simplify prover's matching depth limit

+  /simplifyMatchDepth:<num>

+                Set Simplify prover's matching depth limit

 

   Z3 specific options:

-  /z3opt:<arg>   : specify additional Z3 options

-  /z3multipleErrors : report multiple counterexamples for each error

-  /useArrayTheory : use Z3's native theory (as opposed to axioms).  Currently

-                    implies /monomorphize.

-

-  /z3types       : generate multi-sorted VC that make use of Z3 types

-  /z3lets:<n>    : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,

-                   3 - (default) any

-  /z3exe:<path>  : path to Z3 executable

+  /z3opt:<arg>  specify additional Z3 options

+  /z3multipleErrors

+                report multiple counterexamples for each error

+  /useArrayTheory

+                use Z3's native theory (as opposed to axioms).  Currently

+                implies /monomorphize.

+

+  /z3types      generate multi-sorted VC that make use of Z3 types

+  /z3lets:<n>   0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,

+                3 - (default) any

+  /z3exe:<path>

+                path to Z3 executable

 ");

     }

   }

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index de863e39..d0e0cb0e 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1667,6 +1667,17 @@ namespace Microsoft.Dafny {
           wr.Write(")");

         }

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        // Since there are no OldExpr's in an expression to be compiled, we can just do a regular substitution

+        // without having to worry about old-capture.

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

+        Contract.Assert(e.Vars.Count == e.RHSs.Count);  // checked by resolution

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

+          substMap.Add(e.Vars[i], e.RHSs[i]);

+        }

+        TrExpr(Translator.Substitute(e.Body, null, substMap));

+

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

         Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 8a9108f0..2eaaca7f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -716,7 +716,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
 VarDeclStatement<.out Statement/*!*/ s.>

 = (. IToken x = null, assignTok = null;  bool isGhost = false;

      VarDecl/*!*/ d;

-     AssignmentRhs r;  Expression lhs0;

+     AssignmentRhs r;  IdentifierExpr lhs0;

      List<VarDecl> lhss = new List<VarDecl>();

      List<AssignmentRhs> rhss = new List<AssignmentRhs>();

   .)

@@ -727,7 +727,10 @@ VarDeclStatement<.out Statement/*!*/ s.>
   { ","

     LocalIdentTypeOptional<out d, isGhost>  (. lhss.Add(d); .)

   }

-  [ ":="                           (. assignTok = t;  lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); .)

+  [ ":="                           (. assignTok = t;

+                                      lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

+                                      lhs0.Var = lhss[0];  lhs0.Type = lhss[0].OptionalType;  // resolve here

+                                   .)

     Rhs<out r, lhs0>               (. rhss.Add(r); .)

     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

     }

@@ -1204,20 +1207,34 @@ EndlessExpression<out Expression e>
 = (. IToken/*!*/ x;

      Expression e0, e1;

      e = dummyExpr;

+     BoundVar d;

+     List<BoundVar> letVars;  List<Expression> letRHSs;

   .)

-  ( "if"                                 (. x = t; .)

+  ( "if"                            (. x = t; .)

     Expression<out e>

     "then" Expression<out e0>

-    "else" Expression<out e1>            (. e = new ITEExpr(x, e, e0, e1); .)

+    "else" Expression<out e1>       (. e = new ITEExpr(x, e, e0, e1); .)

   | MatchExpression<out e>

   | QuantifierGuts<out e>

   | ComprehensionExpr<out e>

-  | "assert"                             (. x = t; .)

+  | "assert"                        (. x = t; .)

     Expression<out e0> ";"

-    Expression<out e1>                   (. e = new AssertExpr(x, e0, e1); .)

-  | "assume"                             (. x = t; .)

+    Expression<out e1>              (. e = new AssertExpr(x, e0, e1); .)

+  | "assume"                        (. x = t; .)

     Expression<out e0> ";"

-    Expression<out e1>                   (. e = new AssumeExpr(x, e0, e1); .)

+    Expression<out e1>              (. e = new AssumeExpr(x, e0, e1); .)

+  | "var"                           (. x = t;

+                                       letVars = new List<BoundVar>();

+                                       letRHSs = new List<Expression>(); .)

+    IdentTypeOptional<out d>        (. letVars.Add(d); .)

+    { "," IdentTypeOptional<out d>  (. letVars.Add(d); .)

+    }

+    ":="

+    Expression<out e>               (. letRHSs.Add(e); .)

+    { "," Expression<out e>         (. letRHSs.Add(e); .)

+    }

+    ";"

+    Expression<out e>               (. e = new LetExpr(x, letVars, letRHSs, e); .)

   )

   .

 MatchExpression<out Expression/*!*/ e>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 04b6b00e..8272736c 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -867,6 +867,17 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class DatatypeDestructor : SpecialField

+  {

+    public readonly DatatypeCtor EnclosingCtor;

+

+    public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes)

+      : base(tok, name, compiledName, preString, postString, isGhost, false, type, attributes)

+    {

+      EnclosingCtor = enclosingCtor;

+    }

+  }

+

   public class CouplingInvariant : MemberDecl {

     public readonly Expression Expr;

     public readonly List<IToken/*!*/>/*!*/ Toks;

@@ -2582,6 +2593,27 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class LetExpr : Expression

+  {

+    public readonly List<BoundVar> Vars;

+    public readonly List<Expression> RHSs;

+    public readonly Expression Body;

+    public LetExpr(IToken tok, List<BoundVar> vars, List<Expression> rhss, Expression body)

+      : base(tok) {

+      Vars = vars;

+      RHSs = rhss;

+      Body = body;

+    }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var rhs in RHSs) {

+          yield return rhs;

+        }

+        yield return Body;

+      }

+    }

+  }

+

   /// <summary>

   /// A ComprehensionExpr has the form:

   ///   BINDER x Attributes | Range(x) :: Term(x)

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index 3f0b6e97..1d075415 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -49,8 +49,8 @@ namespace Microsoft.Dafny {
 

       program = new Program(programName, modules, builtIns);

 

-      if (Bpl.CommandLineOptions.Clo.DafnyPrintFile != null) {

-        string filename = Bpl.CommandLineOptions.Clo.DafnyPrintFile;

+      if (DafnyOptions.O.DafnyPrintFile != null) {

+        string filename = DafnyOptions.O.DafnyPrintFile;

         if (filename == "-") {

           Printer pr = new Printer(System.Console.Out);

           pr.PrintProgram(program);

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
new file mode 100644
index 00000000..8c604b8a
--- /dev/null
+++ b/Source/Dafny/DafnyOptions.cs
@@ -0,0 +1,132 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics.Contracts;

+using Bpl = Microsoft.Boogie;

+

+namespace Microsoft.Dafny

+{

+  public class DafnyOptions : Bpl.CommandLineOptions

+  {

+    public DafnyOptions()

+      : base("Dafny", "Dafny program verifier") {

+    }

+

+    private static DafnyOptions clo;

+    public static DafnyOptions O {

+      get { return clo; }

+    }

+

+    public static void Install(DafnyOptions options) {

+      Contract.Requires(options != null);

+      clo = options;

+      Bpl.CommandLineOptions.Install(options);

+    }

+

+    public bool DisallowSoundnessCheating = false;

+    public int Induction = 3;

+    public int InductionHeuristic = 6;

+    public string DafnyPrelude = null;

+    public string DafnyPrintFile = null;

+    public bool Compile = true;

+    public bool ForceCompile = false;

+

+    protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

+      Contract.Requires(name != null);

+      Contract.Requires(ps != null);

+      var args = ps.args;  // convenient synonym

+

+      switch (name) {

+        case "dprelude":

+          if (ps.ConfirmArgumentCount(1)) {

+            DafnyPrelude = args[ps.i];

+          }

+          return true;

+

+        case "dprint":

+          if (ps.ConfirmArgumentCount(1)) {

+            DafnyPrintFile = args[ps.i];

+          }

+          return true;

+

+        case "compile": {

+            int compile = 0;

+            if (ps.GetNumericArgument(ref compile, 3)) {

+              Compile = compile == 1 || compile == 2;

+              ForceCompile = compile == 2;

+            }

+            return true;

+          }

+

+        case "noCheating": {

+            int cheat = 0; // 0 is default, allows cheating

+            if (ps.GetNumericArgument(ref cheat, 2)) {

+              DisallowSoundnessCheating = cheat == 1;

+            }

+            return true;

+          }

+

+        case "induction":

+          ps.GetNumericArgument(ref Induction, 4);

+          return true;

+

+        case "inductionHeuristic":

+          ps.GetNumericArgument(ref InductionHeuristic, 7);

+          return true;

+

+        default:

+          break;

+      }

+      // not a Dafny-specific option, so defer to superclass

+      return base.ParseOption(name, ps);

+    }

+

+    protected override void ApplyDefaultOptions() {

+      base.ApplyDefaultOptions();

+

+      // expand macros in filenames, now that LogPrefix is fully determined

+      ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp);

+      ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp);

+    }

+

+    public override void AttributeUsage() {

+      // TODO: provide attribute help here

+    }

+

+    public override void Usage() {

+      Console.WriteLine(@"  ---- Dafny options ---------------------------------------------------------

+

+  Multiple .dfy files supplied on the command line are concatenated into one

+  Dafny program.

+

+  /dprelude:<file>

+                choose Dafny prelude file

+  /dprint:<file>

+                print Dafny program after parsing it

+                (use - as <file> to print to console)

+  /compile:<n>  0 - do not compile Dafny program

+                1 (default) - upon successful verification of the Dafny

+                    program, compile Dafny program to C# program out.cs

+                2 - always attempt to compile Dafny program to C# program

+                    out.cs, regardless of verification outcome

+  /noCheating:<n>

+                0 (default) - allow assume statements and free invariants

+                1 - treat all assumptions as asserts, and drop free.

+  /induction:<n>

+                0 - never do induction, not even when attributes request it

+                1 - only apply induction when attributes request it

+                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

+  /inductionHeuristic:<n>

+                0 - least discriminating induction heuristic (that is, lean

+                    toward applying induction more often)

+                1,2,3,4,5 - levels in between, ordered as follows as far as

+                    how discriminating they are:  0 < 1 < 2 < (3,4) < 5 < 6

+                6 (default) - most discriminating

+");

+    }

+  }

+}

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 40a8cacc..dfa9e503 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -154,6 +154,7 @@
     <Compile Include="Compiler.cs" />

     <Compile Include="DafnyAst.cs" />

     <Compile Include="DafnyMain.cs" />

+    <Compile Include="DafnyOptions.cs" />

     <Compile Include="Printer.cs" />

     <Compile Include="Resolver.cs" />

     <Compile Include="SccGraph.cs" />

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 0dc30e8a..583fcc61 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -23,7 +23,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-

+	

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

-

-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

-	  Contract.Requires(tok != null);

-	  Contract.Requires(msg != null);

+	

+    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+      Contract.Requires(tok != null);

+      Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

 	}

 

@@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;

 		}

 	}

-

+	

 	void Expect (int n) {

 		if (la.kind==n) Get(); else { SynErr(n); }

 	}

-

+	

 	bool StartOf (int s) {

 		return set[s, la.kind];

 	}

-

+	

 	void ExpectWeak (int n, int follow) {

 		if (la.kind == n) Get();

 		else {

@@ -182,7 +182,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 	}

 

-

+	

 	void Dafny() {

 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

@@ -1100,7 +1100,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void VarDeclStatement(out Statement/*!*/ s) {

 		IToken x = null, assignTok = null;  bool isGhost = false;

 		VarDecl/*!*/ d;

-		AssignmentRhs r;  Expression lhs0;

+		AssignmentRhs r;  IdentifierExpr lhs0;

 		List<VarDecl> lhss = new List<VarDecl>();

 		List<AssignmentRhs> rhss = new List<AssignmentRhs>();

 		

@@ -1119,7 +1119,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		}

 		if (la.kind == 49) {

 			Get();

-			assignTok = t;  lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); 

+			assignTok = t;

+			lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

+			lhs0.Var = lhss[0];  lhs0.Type = lhss[0].OptionalType;  // resolve here

+			

 			Rhs(out r, lhs0);

 			rhss.Add(r); 

 			while (la.kind == 19) {

@@ -1789,7 +1792,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: {

+		case 18: case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: {

 			EndlessExpression(out e);

 			break;

 		}

@@ -1845,6 +1848,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 		IToken/*!*/ x;

 		Expression e0, e1;

 		e = dummyExpr;

+		BoundVar d;

+		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

 		case 55: {

@@ -1888,6 +1893,31 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new AssumeExpr(x, e0, e1); 

 			break;

 		}

+		case 18: {

+			Get();

+			x = t;

+			letVars = new List<BoundVar>();

+			letRHSs = new List<Expression>(); 

+			IdentTypeOptional(out d);

+			letVars.Add(d); 

+			while (la.kind == 19) {

+				Get();

+				IdentTypeOptional(out d);

+				letVars.Add(d); 

+			}

+			Expect(49);

+			Expression(out e);

+			letRHSs.Add(e); 

+			while (la.kind == 19) {

+				Get();

+				Expression(out e);

+				letRHSs.Add(e); 

+			}

+			Expect(17);

+			Expression(out e);

+			e = new LetExpr(x, letVars, letRHSs, e); 

+			break;

+		}

 		default: SynErr(133); break;

 		}

 	}

@@ -2277,13 +2307,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";

+		la.val = "";		

 		Get();

 		Dafny();

 

-		Expect(0);

+    Expect(0);

 	}

-

+	

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

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

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

@@ -2291,17 +2321,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

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

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

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

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

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

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

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

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

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

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

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

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

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

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

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

-		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}

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

 

 	};

 } // end Parser

@@ -2310,20 +2340,18 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {

 	public int count = 0;                                    // number of errors detected

 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

-

+  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

+  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

+  

 	public void SynErr(string filename, int line, int col, int n) {

-		SynErr(filename, line, col, GetSyntaxErrorString(n));

-	}

-

-	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

-		Contract.Requires(msg != null);

+    SynErr(filename, line, col, GetSyntaxErrorString(n));

+  }

+	public virtual void SynErr(string filename, int line, int col, string msg) {

+	  Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

-	}

-

-	string GetSyntaxErrorString(int n) {

+  }

+  string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

 			case 0: s = "EOF expected"; break;

@@ -2473,7 +2501,7 @@ public class Errors {
 

 			default: s = "error " + n; break;

 		}

-		return s;

+    return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2481,9 +2509,8 @@ public class Errors {
 		Contract.Requires(msg != null);

 		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

-

 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

-		Contract.Requires(msg != null);

+	  Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

 	}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 10099bf4..5b9ba1d6 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1014,6 +1014,23 @@ namespace Microsoft.Dafny {
         }

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

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        bool parensNeeded = !isRightmost;

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

+        string sep = "";

+        foreach (var v in e.Vars) {

+          wr.Write("{0}{1}", sep, v.Name);

+          PrintType(": ", v.Type);

+          sep = ", ";

+        }

+        wr.Write(" := ");

+        PrintExpressionList(e.RHSs);

+        wr.Write("; ");

+        PrintExpression(e.Body);

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

+

+

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         bool parensNeeded = !isRightmost;

@@ -1106,8 +1123,8 @@ namespace Microsoft.Dafny {
       string sep = "";

       foreach (BoundVar bv in boundVars) {

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

-        sep = ", ";

         PrintType(": ", bv.Type);

+        sep = ", ";

       }

       PrintAttributes(attrs);

       if (range != null) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index df2d2b0b..55c2f48b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -12,7 +12,12 @@ using Microsoft.Boogie;
 namespace Microsoft.Dafny {

   public class Resolver {

     public int ErrorCount = 0;

-    void Error(IToken tok, string msg, params object[] args) {

+    public virtual void HereIsASillyTest() {

+    }

+    /// <summary>

+    /// This method is virtual, because it is overridden in the VSX plug-in for Dafny.

+    /// </summary>

+    protected virtual void Error(IToken tok, string msg, params object[] args) {

       Contract.Requires(tok != null);

       Contract.Requires(msg != null);

       ConsoleColor col = Console.ForegroundColor;

@@ -254,7 +259,7 @@ namespace Microsoft.Dafny {
                 if (members.ContainsKey(formal.Name)) {

                   Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);

                 } else {

-                  dtor = new SpecialField(formal.tok, formal.Name, "dtor_" + formal.Name, "", "", false, false, formal.Type, null);

+                  dtor = new DatatypeDestructor(formal.tok, ctor, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);

                   dtor.EnclosingClass = dt;  // resolve here

                   members.Add(formal.Name, dtor);

                 }

@@ -2751,6 +2756,30 @@ namespace Microsoft.Dafny {
         }

         e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        foreach (var rhs in e.RHSs) {

+          ResolveExpression(rhs, twoState);

+        }

+        scope.PushMarker();

+        if (e.Vars.Count != e.RHSs.Count) {

+          Error(expr, "let expression must have same number of bound variables (found {0}) as RHSs (found {1})", e.Vars.Count, e.RHSs.Count);

+        }

+        int i = 0;

+        foreach (var v in e.Vars) {

+          if (!scope.Push(v.Name, v)) {

+            Error(v, "Duplicate let-variable name: {0}", v.Name);

+          }

+          ResolveType(v.tok, v.Type);

+          if (i < e.RHSs.Count && !UnifyTypes(v.Type, e.RHSs[i].Type)) {

+            Error(e.RHSs[i].tok, "type of RHS ({0}) does not match type of bound variable ({1})", e.RHSs[i].Type, v.Type);

+          }

+          i++;

+        }

+        ResolveExpression(e.Body, twoState);

+        scope.PopMarker();

+        expr.Type = e.Body.Type;

+

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         int prevErrorCount = ErrorCount;

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 634abf45..1ab06974 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer

 	//    b) part of stream in buffer

 	// 2) non seekable stream (network, console)

-

+  

 	public const int EOF = 65535 + 1; // char.MaxValue + 1;

 	const int MIN_BUFFER_LENGTH = 1024; // 1KB

 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

@@ -31,17 +31,15 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)

 	bool isUserStream;  // was the stream opened by the user?

 

-	[ContractInvariantMethod]

-	void ObjectInvariant(){

-		Contract.Invariant(buf != null);

-		Contract.Invariant(stream != null);

-	}

-

-//  [NotDelayed]

-	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {

+[ContractInvariantMethod]

+void ObjectInvariant(){

+  Contract.Invariant(buf != null);

+  Contract.Invariant(stream != null);}

+    [NotDelayed]

+	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {

 	  Contract.Requires(s != null);

 		stream = s; this.isUserStream = isUserStream;

-

+		

 		int fl, bl;

 		if (s.CanSeek) {

 			fl = (int) s.Length;

@@ -53,12 +51,12 @@ public class Buffer {
 

 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

 		fileLen = fl;  bufLen = bl;

-

+		

 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

 		if (bufLen == fileLen && s.CanSeek) Close();

 	}

-

+	

 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor

 	  Contract.Requires(b != null);

 		buf = b.buf;

@@ -75,14 +73,14 @@ public class Buffer {
 	}

 

 	~Buffer() { Close(); }

-

+	

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-

+	

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -102,7 +100,7 @@ public class Buffer {
 		Pos = curPos;

 		return ch;

 	}

-

+	

 	public string/*!*/ GetString (int beg, int end) {

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

 		int len = 0;

@@ -141,7 +139,7 @@ public class Buffer {
 			}

 		}

 	}

-

+	

 	// Read the next chunk of bytes from the stream, increases the buffer

 	// if needed and updates the fields fileLen and bufLen.

 	// Returns the number of bytes read.

@@ -215,20 +213,19 @@ public class Scanner {
 	const int noSym = 104;

 

 

-	[ContractInvariantMethod]

-	void objectInvariant(){

-		Contract.Invariant(buffer!=null);

-		Contract.Invariant(t != null);

-		Contract.Invariant(start != null);

-		Contract.Invariant(tokens != null);

-		Contract.Invariant(pt != null);

-		Contract.Invariant(tval != null);

-		Contract.Invariant(Filename != null);

-		Contract.Invariant(errorHandler != null);

-	}

-

+[ContractInvariantMethod]

+void objectInvariant(){

+  Contract.Invariant(buffer!=null);

+  Contract.Invariant(t != null);

+  Contract.Invariant(start != null);

+  Contract.Invariant(tokens != null);

+  Contract.Invariant(pt != null);

+  Contract.Invariant(tval != null);

+  Contract.Invariant(Filename != null);

+  Contract.Invariant(errorHandler != null);

+}

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

-

+	

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

 	int ch;           // current input character

 	int pos;          // byte position of current character

@@ -239,13 +236,13 @@ public class Scanner {
 

 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)

 	Token/*!*/ pt;         // current peek token

-

+	

 	char[]/*!*/ tval = new char[128]; // text of current token

 	int tlen;         // length of current token

-

+	

 	private string/*!*/ Filename;

 	private Errors/*!*/ errorHandler;

-

+	

 	static Scanner() {

 		start = new Hashtable(128);

 		for (int i = 39; i <= 39; ++i) start[i] = 1;

@@ -293,9 +290,9 @@ public class Scanner {
 		start[Buffer.EOF] = -1;

 

 	}

-

-//	[NotDelayed]

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

+	

+	[NotDelayed]

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

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -305,14 +302,15 @@ public class Scanner {
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

 			Filename = fileName;

+			

 			Init();

 		} catch (IOException) {

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

 		}

 	}

-

-//	[NotDelayed]

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

+	

+	[NotDelayed]

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

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -321,9 +319,10 @@ public class Scanner {
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

+		

 		Init();

 	}

-

+	

 	void Init() {

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

 		oldEols = 0;

@@ -344,11 +343,11 @@ public class Scanner {
 	Contract.Ensures(Contract.Result<string>() != null);

 	  int p = buffer.Pos;

 	  int ch = buffer.Read();

-	  // replace isolated '\r' by '\n' in order to make

+      // replace isolated '\r' by '\n' in order to make

 	  // eol handling uniform across Windows, Unix and Mac

 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 	  while (ch != EOL && ch != Buffer.EOF){

-		ch = buffer.Read();

+	    ch = buffer.Read();

 		// replace isolated '\r' by '\n' in order to make

 		// eol handling uniform across Windows, Unix and Mac

 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

@@ -359,7 +358,7 @@ public class Scanner {
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; }

+		if (oldEols > 0) { ch = EOL; oldEols--; } 

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -367,9 +366,9 @@ public class Scanner {
 //			// eol handling uniform across Windows, Unix and Mac

 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 //			if (ch == EOL) { line++; col = 0; }

-

+			

 			while (true) {

-				pos = buffer.Pos;

+			    pos = buffer.Pos;

 				ch = buffer.Read(); col++;

 				// replace isolated '\r' by '\n' in order to make

 				// eol handling uniform across Windows, Unix and Mac

@@ -419,7 +418,7 @@ public class Scanner {
 				return;

 			  }

 

-

+			

 		}

 

 	}

@@ -557,13 +556,10 @@ public class Scanner {
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) {

-			Contract.Assert(start[ch] != null);

-			state = (int) start[ch];

-		}

+		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

 		else { state = 0; }

 		tlen = 0; AddCh();

-

+		

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -763,14 +759,14 @@ public class Scanner {
 		t.val = new String(tval, 0, tlen);

 		return t;

 	}

-

+	

 	private void SetScannerBehindT() {

 		buffer.Pos = t.pos;

 		NextCh();

 		line = t.line; col = t.col;

 		for (int i = 0; i < tlen; i++) NextCh();

 	}

-

+	

 	// get the next token (possibly a token already seen during peeking)

 	public Token/*!*/ Scan () {

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

@@ -791,7 +787,7 @@ public class Scanner {
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-

+	

 		return pt;

 	}

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 37f80bf1..88f95f30 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -259,7 +259,7 @@ namespace Microsoft.Dafny {
     }

 

     static Bpl.Program ReadPrelude() {

-      string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude;

+      string preludePath = DafnyOptions.O.DafnyPrelude;

       if (preludePath == null)

       {

           //using (System.IO.Stream stream = cce.NonNull( System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource

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

       Bpl.StmtList stmts;

       if (!wellformednessProc) {

-        if (3 <= CommandLineOptions.Clo.DafnyInduction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) {

+        if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) {

           var posts = new List<Expression>();

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

           var allIns = new List<Formal>();

@@ -1650,6 +1650,9 @@ namespace Microsoft.Dafny {
           var t = IsTotal(e.Obj, etran);

           if (e.Obj.Type.IsRefType) {

             t = BplAnd(t, Bpl.Expr.Neq(etran.TrExpr(e.Obj), predef.Null));

+          } else if (e.Field is DatatypeDestructor) {

+            var dtor = (DatatypeDestructor)e.Field;

+            t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));

           }

           return t;

         }

@@ -1735,7 +1738,7 @@ namespace Microsoft.Dafny {
         return r;

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

-        return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran));

+        return IsTotal(e.E, etran.Old);

       } else if (expr is MultiSetFormingExpr) {

         MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

         return IsTotal(e.E, etran);

@@ -1777,6 +1780,14 @@ namespace Microsoft.Dafny {
         }

         Bpl.Expr r = BplAnd(t0, t1);

         return z == null ? r : BplAnd(r, z);

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        Bpl.Expr total = Bpl.Expr.True;

+        foreach (var rhs in e.RHSs) {

+          total = BplAnd(total, IsTotal(rhs, etran));

+        }

+        return BplAnd(total, IsTotal(etran.GetSubstitutedBody(e), etran));

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var total = IsTotal(e.Term, etran);

@@ -1794,7 +1805,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr gTotal = IsTotal(e.Guard, etran);

         Bpl.Expr g = etran.TrExpr(e.Guard);

         Bpl.Expr bTotal = IsTotal(e.Body, etran);

-        if (e is AssertExpr) {

+        if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {

           return BplAnd(gTotal, BplAnd(g, bTotal));

         } else {

           return BplAnd(gTotal, Bpl.Expr.Imp(g, bTotal));

@@ -1893,7 +1904,7 @@ namespace Microsoft.Dafny {
         return CanCallAssumption(dtv.Arguments, etran);

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

-        return new Bpl.OldExpr(expr.tok, CanCallAssumption(e.E, etran));

+        return CanCallAssumption(e.E, etran.Old);

       } else if (expr is MultiSetFormingExpr) {

         MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

         return CanCallAssumption(e.E, etran);

@@ -1923,6 +1934,14 @@ namespace Microsoft.Dafny {
             break;

         }

         return BplAnd(t0, t1);

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        Bpl.Expr canCall = Bpl.Expr.True;

+        foreach (var rhs in e.RHSs) {

+          canCall = BplAnd(canCall, CanCallAssumption(rhs, etran));

+        }

+        return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran));

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var total = CanCallAssumption(e.Term, etran);

@@ -1938,11 +1957,11 @@ namespace Microsoft.Dafny {
       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         Bpl.Expr gCanCall = CanCallAssumption(e.Guard, etran);

-        Bpl.Expr g = etran.TrExpr(e.Guard);

         Bpl.Expr bCanCall = CanCallAssumption(e.Body, etran);

-        if (e is AssertExpr) {

-          return BplAnd(gCanCall, BplAnd(g, bCanCall));

+        if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {

+          return BplAnd(gCanCall, bCanCall);

         } else {

+          Bpl.Expr g = etran.TrExpr(e.Guard);

           return BplAnd(gCanCall, Bpl.Expr.Imp(g, bCanCall));

         }

       } else if (expr is ITEExpr) {

@@ -2110,6 +2129,10 @@ namespace Microsoft.Dafny {
         CheckWellformed(e.Obj, options, locals, builder, etran);

         if (e.Obj.Type.IsRefType) {

           CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);

+        } else if (e.Field is DatatypeDestructor) {

+          var dtor = (DatatypeDestructor)e.Field;

+          builder.Add(Assert(expr.tok, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)),

+            string.Format("destructor '{0}' can only be applied to datatype values constructed by '{1}'", dtor.Name, dtor.EnclosingCtor.Name)));

         }

         if (options.DoReadsChecks && e.Field.IsMutable) {

           builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv));

@@ -2321,6 +2344,13 @@ namespace Microsoft.Dafny {
             break;

         }

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        foreach (var rhs in e.RHSs) {

+          CheckWellformed(rhs, options, locals, builder, etran);

+        }

+        CheckWellformedWithResult(etran.GetSubstitutedBody(e), options, result, resultType, locals, builder, etran);

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran);

@@ -2339,7 +2369,7 @@ namespace Microsoft.Dafny {
       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         CheckWellformed(e.Guard, options, locals, builder, etran);

-        if (e is AssertExpr) {

+        if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {

           bool splitHappened;

           var ss = TrSplitExpr(e.Guard, etran, out splitHappened);

           if (!splitHappened) {

@@ -2813,7 +2843,7 @@ namespace Microsoft.Dafny {
       if (!wellformednessProc) {

         string comment = "user-defined preconditions";

         foreach (MaybeFreeExpression p in m.Req) {

-          if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {

+          if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));

           } else {

             bool splitHappened;  // we actually don't care

@@ -2826,7 +2856,7 @@ namespace Microsoft.Dafny {
         }

         comment = "user-defined postconditions";

         if (!skipEnsures) foreach (MaybeFreeExpression p in m.Ens) {

-          if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {

+          if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));

           } else {

             bool splitHappened;  // we actually don't care

@@ -3300,7 +3330,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

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

       if (stmt is PredicateStmt) {

-        if (stmt is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {

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

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

           PredicateStmt s = (PredicateStmt)stmt;

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

@@ -3928,7 +3958,7 @@ namespace Microsoft.Dafny {
         invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));

 

         invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));

-        if (loopInv.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {

+        if (loopInv.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

           invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));

         } else {

           bool splitHappened;

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

       Contract.Requires(etran != null);

 

-      Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver);

+      Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type);

       Bpl.ExprSeq ins = new Bpl.ExprSeq();

       if (!method.IsStatic) {

         if (bReceiver == null) {

@@ -4995,11 +5025,13 @@ namespace Microsoft.Dafny {
     internal class BoogieWrapper : Expression

     {

       public readonly Bpl.Expr Expr;

-      public BoogieWrapper(Bpl.Expr expr)

+      public BoogieWrapper(Bpl.Expr expr, Type dafnyType)

         : base(expr.tok)

       {

         Contract.Requires(expr != null);

+        Contract.Requires(dafnyType != null);

         Expr = expr;

+        Type = dafnyType;  // resolve immediately

       }

     }

 

@@ -5009,7 +5041,7 @@ namespace Microsoft.Dafny {
       public readonly PredefinedDecls predef;

       public readonly Translator translator;

       public readonly string This;

-      public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.

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

       readonly Function applyLimited_CurrentFunction;

       public readonly int layerOffset = 0;

       public int Statistics_CustomLayerFunctionCount = 0;

@@ -5020,66 +5052,60 @@ namespace Microsoft.Dafny {
         Contract.Invariant(predef != null);

         Contract.Invariant(translator != null);

         Contract.Invariant(This != null);

+        Contract.Invariant(modifiesFrame != null);

         Contract.Invariant(layerOffset == 0 || layerOffset == 1);

         Contract.Invariant(0 <= Statistics_CustomLayerFunctionCount);

       }

 

-      public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken) {

+      /// <summary>

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

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

+      /// </summary>

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

+        Function applyLimited_CurrentFunction, int layerOffset, string modifiesFrame) {

+

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

-        Contract.Requires(heapToken != null);

+        Contract.Requires(heap != null);

+        Contract.Requires(thisVar != null);

+        Contract.Invariant(layerOffset == 0 || layerOffset == 1);

+        Contract.Invariant(modifiesFrame != null);

+

         this.translator = translator;

         this.predef = predef;

-        this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);

-        this.This = "this";

+        this.HeapExpr = heap;

+        this.This = thisVar;

+        this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

+        this.layerOffset = layerOffset;

+        this.modifiesFrame = modifiesFrame;

       }

 

-      public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) {

+      public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken)

+        : this(translator, predef, new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType)) {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

-        Contract.Requires(heap != null);

-        this.translator = translator;

-        this.predef = predef;

-        this.HeapExpr = heap;

-        this.This = "this";

+        Contract.Requires(heapToken != null);

       }

 

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

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

+        : this(translator, predef, heap, "this") {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

         Contract.Requires(heap != null);

-        Contract.Requires(thisVar != null);

-        this.translator = translator;

-        this.predef = predef;

-        this.HeapExpr = heap;

-        this.This = thisVar;

       }

 

-      ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset)

-      {

-          Contract.Requires(translator != null);

-          Contract.Requires(predef != null);

-          Contract.Requires(heap != null);

-          this.translator = translator;

-          this.predef = predef;

-          this.HeapExpr = heap;

-          this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

-          this.This = "this";

-          this.layerOffset = layerOffset;

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

+        : this(translator, predef, heap, thisVar, null, 0, "$_Frame") {

+        Contract.Requires(translator != null);

+        Contract.Requires(predef != null);

+        Contract.Requires(heap != null);

+        Contract.Requires(thisVar != null);

       }

 

       public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)

-      {

-          Contract.Requires(etran != null);

-          Contract.Requires(modifiesFrame != null);

-          this.translator = etran.translator;

-          this.HeapExpr = etran.HeapExpr;

-          this.predef = etran.predef;

-          this.This = etran.This;

-          this.applyLimited_CurrentFunction = etran.applyLimited_CurrentFunction;

-          this.layerOffset = etran.layerOffset;

-          this.oldEtran = etran.oldEtran;

-          this.modifiesFrame = modifiesFrame;

+        : this(etran.translator, etran.predef, etran.HeapExpr, etran.This, etran.applyLimited_CurrentFunction, etran.layerOffset, modifiesFrame) {

+        Contract.Requires(etran != null);

+        Contract.Requires(modifiesFrame != null);

       }

 

       ExpressionTranslator oldEtran;

@@ -5088,7 +5114,7 @@ namespace Microsoft.Dafny {
           Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);

 

           if (oldEtran == null) {

-            oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyLimited_CurrentFunction, layerOffset);

+            oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);

           }

           return oldEtran;

         }

@@ -5104,7 +5130,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(applyLimited_CurrentFunction != null);

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

 

-        return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset);

+        return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);

       }

 

       public ExpressionTranslator LayerOffset(int offset) {

@@ -5112,7 +5138,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(layerOffset + offset <= 1);

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

 

-        return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset + offset);

+        return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame);

       }

 

       public Bpl.IdentifierExpr TheFrame(IToken tok)

@@ -5124,7 +5150,7 @@ namespace Microsoft.Dafny {
         Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");

         Bpl.Type fieldAlpha = predef.FieldName(tok, alpha);

         Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);

-        return new Bpl.IdentifierExpr(tok, this.modifiesFrame ?? "$_Frame", ty);

+        return new Bpl.IdentifierExpr(tok, this.modifiesFrame, ty);

       }

 

       public Bpl.IdentifierExpr Tick() {

@@ -5134,24 +5160,33 @@ namespace Microsoft.Dafny {
         return new Bpl.IdentifierExpr(Token.NoToken, "$Tick", predef.TickType);

       }

 

-      public Bpl.IdentifierExpr ModuleContextHeight()

-        {

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

+      public Bpl.IdentifierExpr ModuleContextHeight() {

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

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

       }

 

-      public Bpl.IdentifierExpr FunctionContextHeight()

-        {

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

+      public Bpl.IdentifierExpr FunctionContextHeight() {

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

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

       }

 

-      public Bpl.IdentifierExpr InMethodContext()

-        {

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

+      public Bpl.IdentifierExpr InMethodContext() {

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

         return new Bpl.IdentifierExpr(Token.NoToken, "$InMethodContext", Bpl.Type.Bool);

       }

 

+      public Expression GetSubstitutedBody(LetExpr e) {

+        Contract.Requires(e != null);

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

+        Contract.Assert(e.Vars.Count == e.RHSs.Count);  // checked by resolution

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

+          Expression rhs = e.RHSs[i];

+          substMap.Add(e.Vars[i], new BoogieWrapper(TrExpr(rhs), rhs.Type));

+        }

+        return Translator.Substitute(e.Body, null, substMap);

+      }

+

+

       /// <summary>

       /// Translates Dafny expression "expr" into a Boogie expression.  If the type of "expr" can be a boolean, then the

       /// token (source location) of the resulting expression is filled in (it wouldn't hurt if the token were always

@@ -5322,7 +5357,7 @@ namespace Microsoft.Dafny {
 

         } else if (expr is OldExpr) {

           OldExpr e = (OldExpr)expr;

-          return new Bpl.OldExpr(expr.tok, TrExpr(e.E));

+          return Old.TrExpr(e.E);

 

         } else if (expr is MultiSetFormingExpr) {

           MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

@@ -5337,7 +5372,6 @@ namespace Microsoft.Dafny {
 

         } else if (expr is FreshExpr) {

           FreshExpr e = (FreshExpr)expr;

-          Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr);

           if (e.E.Type is SetType) {

             // generate:  (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])

             // TODO: trigger?

@@ -5345,7 +5379,7 @@ namespace Microsoft.Dafny {
             Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);

             Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);

             Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg);

-            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, o, oldHeap));

+            Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, o));

             Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);

             return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), body);

           } else if (e.E.Type is SeqType) {

@@ -5355,14 +5389,14 @@ namespace Microsoft.Dafny {
             Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);

             Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);

             Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);

-            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, XsubI, oldHeap));

+            Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, XsubI));

             Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null);

             Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);

             return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body);

           } else {

             // generate:  x == null || !old($Heap)[x]

             Bpl.Expr oNull = Bpl.Expr.Eq(TrExpr(e.E), predef.Null);

-            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, TrExpr(e.E), oldHeap));

+            Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));

             return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Or, oNull, oIsFresh);

           }

 

@@ -5539,6 +5573,10 @@ namespace Microsoft.Dafny {
           }

           return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);

 

+        } else if (expr is LetExpr) {

+          var e = (LetExpr)expr;

+          return TrExpr(GetSubstitutedBody(e));

+

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

           Bpl.VariableSeq bvars = new Bpl.VariableSeq();

@@ -5923,16 +5961,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(e != null);

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

 

-        return IsAlloced(tok, e, HeapExpr);

-      }

-

-      Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e, Bpl.Expr heap) {

-        Contract.Requires(tok != null);

-        Contract.Requires(e != null);

-        Contract.Requires(heap != null);

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

-

-        return ReadHeap(tok, heap, e, predef.Alloc(tok));

+        return ReadHeap(tok, HeapExpr, e, predef.Alloc(tok));

       }

 

       public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) {

@@ -6394,9 +6423,9 @@ namespace Microsoft.Dafny {
         var e = (ConcreteSyntaxExpression)expr;

         return TrSplitExpr(e.ResolvedExpression, splits, position, expandFunctions, etran);

 

-      } else if (expr is PredicateExpr) {

-        var e = (PredicateExpr)expr;

-        return TrSplitExpr(e.Body, splits, position, expandFunctions, etran);

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, expandFunctions, etran);

 

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

@@ -6467,15 +6496,33 @@ namespace Microsoft.Dafny {
           return true;

         }

 

-      } else if (expr is OldExpr) {

-        var e = (OldExpr)expr;

-        var ss = new List<SplitExprInfo>();

-        if (TrSplitExpr(e.E, ss, position, expandFunctions, etran)) {

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        // For a predicate expression in split position, the predicate can be used as an assumption.  Unfortunately,

+        // this assumption is not generated in non-split positions (because I don't know how.)

+        // So, treat "assert/assume P; E" like "P ==> E".

+        if (position) {

+          var guard = etran.TrExpr(e.Guard);

+          var ss = new List<SplitExprInfo>();

+          TrSplitExpr(e.Body, ss, position, expandFunctions, etran);

+          foreach (var s in ss) {

+            // as the source location in the following implication, use that of the translated "s"

+            splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, guard, s.E)));

+          }

+        } else {

+          var ss = new List<SplitExprInfo>();

+          TrSplitExpr(e.Guard, ss, !position, expandFunctions, etran);

+          var rhs = etran.TrExpr(e.Body);

           foreach (var s in ss) {

-            splits.Add(new SplitExprInfo(s.IsFree, new Bpl.OldExpr(s.E.tok, s.E)));

+            // as the source location in the following implication, use that of the translated "s"

+            splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs)));

           }

-          return true;

         }

+        return true;

+

+      } else if (expr is OldExpr) {

+        var e = (OldExpr)expr;

+        return TrSplitExpr(e.E, splits, position, expandFunctions, etran.Old);

 

       } else if (expandFunctions && position && expr is FunctionCallExpr) {

         var fexp = (FunctionCallExpr)expr;

@@ -6531,7 +6578,7 @@ namespace Microsoft.Dafny {
       } else if ((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) {

         var e = (QuantifierExpr)expr;

         var inductionVariables = ApplyInduction(e);

-        if (2 <= CommandLineOptions.Clo.DafnyInduction && inductionVariables.Count != 0) {

+        if (2 <= DafnyOptions.O.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

@@ -6642,7 +6689,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tracePrinter != null);

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

 

-      if (CommandLineOptions.Clo.DafnyInduction == 0) {

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

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

       }

 

@@ -6727,7 +6774,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      if (CommandLineOptions.Clo.DafnyInduction < 2) {

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

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

       }

 

@@ -6762,7 +6809,7 @@ namespace Microsoft.Dafny {
     /// Parameter 'n' is allowed to be a ThisSurrogate.

     /// </summary>

     bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {

-      switch (CommandLineOptions.Clo.DafnyInductionHeuristic) {

+      switch (DafnyOptions.O.InductionHeuristic) {

         case 0: return true;

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

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

@@ -6780,7 +6827,7 @@ namespace Microsoft.Dafny {
       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 = CommandLineOptions.Clo.DafnyInductionHeuristic == 2 || CommandLineOptions.Clo.DafnyInductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;

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

@@ -6789,13 +6836,13 @@ namespace Microsoft.Dafny {
         return exprIsProminent && e.Var == n;

       } else if (expr is SeqSelectExpr) {

         var e = (SeqSelectExpr)expr;

-        var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent;

+        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 = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent;

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

@@ -6806,7 +6853,7 @@ namespace Microsoft.Dafny {
         bool inferredDecreases;  // we don't actually care

         var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases);

         bool variantArgument;

-        if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) {

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

           variantArgument = rec;

         } else {

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

@@ -6821,7 +6868,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < e.Function.Formals.Count; i++) {

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

           var exp = e.Args[i];

-          if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) {

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

             variantArgument = rec;

           } else {

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

@@ -6838,9 +6885,6 @@ namespace Microsoft.Dafny {
         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 OldExpr) {

-        var e = (OldExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);  // prominent status continues

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

         // both Not and SeqLength preserve prominence

@@ -6958,7 +7002,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {

+    public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(expr != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

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

@@ -7044,7 +7088,11 @@ namespace Microsoft.Dafny {
 

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

-        Expression se = Substitute(e.E, receiverReplacement, substMap);  // TODO: whoa, won't this do improper variable capture?

+        // Note, it is up to the caller to avoid variable capture.  In most cases, this is not a

+        // problem, since variables have unique declarations.  However, it is an issue if the substitution

+        // takes place inside an OldExpr.  In those cases (see LetExpr), the caller can use a

+        // BoogieWrapper before calling Substitute.

+        Expression se = Substitute(e.E, receiverReplacement, substMap);

         if (se != e.E) {

           newExpr = new OldExpr(expr.tok, se);

         }

@@ -7076,6 +7124,22 @@ namespace Microsoft.Dafny {
           newExpr = newBin;

         }

 

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

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

+        bool anythingChanged = false;

+        foreach (var rhs in e.RHSs) {

+          var r = Substitute(rhs, receiverReplacement, substMap);

+          if (r != rhs) {

+            anythingChanged = true;

+          }

+          rhss.Add(r);

+        }

+        var body = Substitute(e.Body, receiverReplacement, substMap);

+        if (anythingChanged || body != e.Body) {

+          newExpr = new LetExpr(e.tok, e.Vars, rhss, body);

+        }

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);

@@ -7102,10 +7166,12 @@ namespace Microsoft.Dafny {
         var e = (PredicateExpr)expr;

         Expression g = Substitute(e.Guard, receiverReplacement, substMap);

         Expression b = Substitute(e.Body, receiverReplacement, substMap);

-        if (expr is AssertExpr) {

-          newExpr = new AssertExpr(e.tok, g, b);

-        } else {

-          newExpr = new AssumeExpr(e.tok, g, b);

+        if (g != e.Guard || b != e.Body) {

+          if (expr is AssertExpr) {

+            newExpr = new AssertExpr(e.tok, g, b);

+          } else {

+            newExpr = new AssumeExpr(e.tok, g, b);

+          }

         }

 

       } else if (expr is ITEExpr) {

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 1c6c1e77..eed5cf59 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -4,11 +4,11 @@
 //

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

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

-// OnlyDafny OnlyDafny.ssc

+// DafnyDriver

 //       - main program for taking a Dafny program and verifying it

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

 

-namespace Microsoft.Boogie

+namespace Microsoft.Dafny

 {

   using System;

   using System.IO;

@@ -17,30 +17,27 @@ namespace Microsoft.Boogie
   using System.Diagnostics.Contracts;

   using PureCollections;

   using Microsoft.Boogie;

+  using Bpl = Microsoft.Boogie;

   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics;

   using VC;

   using AI = Microsoft.AbstractInterpretationFramework;

 

-/*

-  The following assemblies are referenced because they are needed at runtime, not at compile time:

-    BaseTypes

-    Provers.Z3

-    System.Compiler.Framework

-*/

-

-  public class OnlyDafny

+  public class DafnyDriver

   {

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

     // Main

 

-    public static int Main (string[] args)

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

+    public static int Main(string[] args)

+    {

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

+

+      DafnyOptions.Install(new DafnyOptions());

+

       //assert forall{int i in (0:args.Length); args[i] != null};

       ExitValue exitValue = ExitValue.VERIFIED;

       CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;

-      if (CommandLineOptions.Clo.Parse(args) != 1)

-      {

+      if (!CommandLineOptions.Clo.Parse(args)) {

         exitValue = ExitValue.PREPROCESSING_ERROR;

         goto END;

       }

@@ -84,7 +81,6 @@ namespace Microsoft.Boogie
             goto END;

         }

       }

-      CommandLineOptions.Clo.RunningBoogieOnSsc = false;

       exitValue = ProcessFiles(CommandLineOptions.Clo.Files);

 

       END:

@@ -155,7 +151,7 @@ namespace Microsoft.Boogie
           ErrorWriteLine(err);

         } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {

           Dafny.Translator translator = new Dafny.Translator();

-          Program boogieProgram = translator.Translate(dafnyProgram);

+          Bpl.Program boogieProgram = translator.Translate(dafnyProgram);

           if (CommandLineOptions.Clo.PrintFile != null)

           {

             PrintBplFile(CommandLineOptions.Clo.PrintFile, boogieProgram, false);

@@ -176,12 +172,12 @@ namespace Microsoft.Boogie
           switch (oc) {

             case PipelineOutcome.VerificationCompleted:

               WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

-              if ((CommandLineOptions.Clo.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || CommandLineOptions.Clo.ForceCompile)

+              if ((DafnyOptions.O.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || DafnyOptions.O.ForceCompile)

                 CompileDafnyProgram(dafnyProgram);

               break;

             case PipelineOutcome.Done:

               WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

-              if (CommandLineOptions.Clo.ForceCompile)

+              if (DafnyOptions.O.ForceCompile)

                 CompileDafnyProgram(dafnyProgram);

               break;

             default:

@@ -209,7 +205,7 @@ namespace Microsoft.Boogie
       }

     }

 

-    static void PrintBplFile (string filename, Program program, bool allowPrintDesugaring)

+    static void PrintBplFile (string filename, Bpl.Program program, bool allowPrintDesugaring)

     {

       Contract.Requires(filename != null);

       Contract.Requires(program != null);

@@ -230,7 +226,7 @@ namespace Microsoft.Boogie
     }

 

 

-    static bool ProgramHasDebugInfo (Program program)

+    static bool ProgramHasDebugInfo (Bpl.Program program)

     {

       Contract.Requires(program != null);

         // We inspect the last declaration because the first comes from the prelude and therefore always has source context.

@@ -251,7 +247,7 @@ namespace Microsoft.Boogie
     static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories){

       Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);

       Console.WriteLine();

-      Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");

+      Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

       if (inconclusives != 0) {

         Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");

       }

@@ -291,11 +287,11 @@ namespace Microsoft.Boogie
     /// Parse the given files into one Boogie program.  If an I/O or parse error occurs, an error will be printed

     /// and null will be returned.  On success, a non-null program is returned.

     /// </summary>

-    static Program ParseBoogieProgram(List<string/*!*/>/*!*/ fileNames, bool suppressTraceOutput)

+    static Bpl.Program ParseBoogieProgram(List<string/*!*/>/*!*/ fileNames, bool suppressTraceOutput)

     {

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

       //BoogiePL.Errors.count = 0;

-      Program program = null;

+      Bpl.Program program = null;

       bool okay = true;

       foreach (string bplFileName in fileNames) {

         if (!suppressTraceOutput) {

@@ -307,7 +303,7 @@ namespace Microsoft.Boogie
           }

         }

 

-        Program programSnippet;

+        Bpl.Program programSnippet;

         int errorCount;

         try {

           errorCount = Microsoft.Boogie.Parser.Parse(bplFileName, null, out programSnippet);

@@ -330,7 +326,7 @@ namespace Microsoft.Boogie
       if (!okay) {

         return null;

       } else if (program == null) {

-        return new Program();

+        return new Bpl.Program();

       } else {

         return program;

       }

@@ -344,7 +340,7 @@ namespace Microsoft.Boogie
     /// The method prints errors for resolution and type checking errors, but still returns

     /// their error code.

     /// </summary>

-    static PipelineOutcome BoogiePipelineWithRerun (Program/*!*/ program, string/*!*/ bplFileName,

+    static PipelineOutcome BoogiePipelineWithRerun (Bpl.Program/*!*/ program, string/*!*/ bplFileName,

         out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

     Contract.Requires(bplFileName != null);

@@ -367,7 +363,7 @@ namespace Microsoft.Boogie
 

             List<string/*!*/>/*!*/ fileNames = new List<string/*!*/>();

             fileNames.Add(bplFileName);

-            Program reparsedProgram = ParseBoogieProgram(fileNames, true);

+            Bpl.Program reparsedProgram = ParseBoogieProgram(fileNames, true);

             if (reparsedProgram != null) {

               ResolveAndTypecheck(reparsedProgram, bplFileName);

             }

@@ -394,7 +390,7 @@ namespace Microsoft.Boogie
     ///  - TypeCheckingError if a type checking error occurred

     ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded

     /// </summary>

-    static PipelineOutcome ResolveAndTypecheck (Program program, string bplFileName)

+    static PipelineOutcome ResolveAndTypecheck (Bpl.Program program, string bplFileName)

     {

       Contract.Requires(program != null);

       Contract.Requires(bplFileName != null);

@@ -435,7 +431,7 @@ namespace Microsoft.Boogie
     ///  - VerificationCompleted if inference and verification completed, in which the out

     ///    parameters contain meaningful values

     /// </summary>

-    static PipelineOutcome InferAndVerify (Program program,

+    static PipelineOutcome InferAndVerify (Bpl.Program program,

                                            out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

@@ -491,7 +487,7 @@ namespace Microsoft.Boogie
       }

 

       var decls = program.TopLevelDeclarations.ToArray();

-      foreach ( Declaration decl in decls )

+      foreach (var decl in decls )

       {Contract.Assert(decl != null);

         Implementation impl = decl as Implementation;

         if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 2f08477b..bef0505e 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -20,6 +20,7 @@ namespace GPUVerify
         public static bool Inference;

         public static string invariantsFile = null;

         public static bool DividedArray = false;

+        public static string ArrayToCheck = null;

         public static bool DividedAccesses = false;

         public static bool Eager = false;

 

@@ -77,6 +78,10 @@ namespace GPUVerify
 

                     case "-dividedArray":

                     case "/dividedArray":

+                    if (hasColonArgument)

+                    {

+                        ArrayToCheck = afterColon;

+                    }

                     DividedArray = true;

 

                     break;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 36881f88..c15327ca 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -414,7 +414,6 @@ namespace GPUVerify
 

         private void ComputeInvariant()

         {

-            List<Expr> UserSuppliedInvariants = GetUserSuppliedInvariants();

 

             invariantGenerationCounter = 0;

 

@@ -430,6 +429,8 @@ namespace GPUVerify
                         continue;

                     }

 

+                    List<Expr> UserSuppliedInvariants = GetUserSuppliedInvariants(Impl.Name);

+

                     HashSet<string> LocalNames = new HashSet<string>();

                     foreach (Variable v in Impl.LocVars)

                     {

@@ -613,7 +614,7 @@ namespace GPUVerify
             Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);

         }

 

-        private List<Expr> GetUserSuppliedInvariants()

+        private List<Expr> GetUserSuppliedInvariants(string ProcedureName)

         {

             List<Expr> result = new List<Expr>();

 

@@ -627,6 +628,24 @@ namespace GPUVerify
             int lineNumber = 1;

             while ((line = sr.ReadLine()) != null)

             {

+                string[] components = line.Split(':');

+

+                if (components.Length != 1 && components.Length != 2)

+                {

+                    Console.WriteLine("Ignoring badly formed candidate invariant '" + line + "' at '" + CommandLineOptions.invariantsFile + "' line " + lineNumber);

+                    continue;

+                }

+

+                if (components.Length == 2)

+                {

+                    if (!components[0].Trim().Equals(ProcedureName))

+                    {

+                        continue;

+                    }

+

+                    line = components[1];

+                }

+

                 string temp_program_text = "axiom (" + line + ");";

                 TokenTextWriter writer = new TokenTextWriter("temp_out.bpl");

                 writer.WriteLine(temp_program_text);

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index 9791d6cf..e38aabea 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -134,6 +134,8 @@ namespace GPUVerify
 

             if (CommandLineOptions.DividedArray)

             {

+                bool FoundArray = CommandLineOptions.ArrayToCheck == null;

+

                 foreach (Variable v in g.NonLocalState.getAllNonLocalVariables())

                 {

                     if (CommandLineOptions.DividedAccesses)

@@ -163,9 +165,20 @@ namespace GPUVerify
                     }

                     else

                     {

-                        doit("temp_" + v.Name + ".bpl", v, -1, -1);

+                        if (CommandLineOptions.ArrayToCheck == null || CommandLineOptions.ArrayToCheck.Equals(v.Name))

+                        {

+                            FoundArray = true;

+                            doit("temp_" + v.Name, v, -1, -1);

+                        }

                     }

                 }

+

+                if (!FoundArray)

+                {

+                    Console.WriteLine("Did not find a non-local array named " + CommandLineOptions.ArrayToCheck);

+                    Environment.Exit(1);

+                }

+

             }

             else

             {

@@ -191,6 +204,8 @@ namespace GPUVerify
 

         public static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)

         {

+            Microsoft.Boogie.CommandLineOptions.Install(new Microsoft.Boogie.CommandLineOptions());

+

             Program program = null;

             bool okay = true;

             for (int fileId = 0; fileId < fileNames.Count; fileId++)

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 64793c9e..947d4eae 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -7,7 +7,6 @@ using System.Diagnostics;
 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie;

 using Microsoft.Boogie.Z3;

-using Microsoft.Z3;

 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Boogie.Simplify;

 

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 2f7f120d..0bcbad35 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -25,6 +25,7 @@ namespace VC
         private Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

         public bool PersistCallTree;

         public static Dictionary<string, int> callTree = null;

+        public int numInlined = 0;

         public readonly static string recordProcName = "boogie_si_record";

 

         [ContractInvariantMethod]

@@ -1576,6 +1577,8 @@ namespace VC
             #endregion

             coverageManager.stop();

 

+            numInlined = (calls.candidateParent.Keys.Count + 1) - (calls.currCandidates.Count);

+

             // Store current call tree

             if (PersistCallTree && (ret == Outcome.Correct || ret == Outcome.Errors || ret == Outcome.ReachedBound))

             {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 001b3f2d..0a59555e 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2964,10 +2964,11 @@ namespace VC {
             if (!(kvp.Key is LiteralExpr) && kvp.Key.ToString() != o.ToString()) {

               string boogieExpr;

               // check whether we are handling BPL or SSC input

-              if (CommandLineOptions.Clo.RunningBoogieOnSsc) {

-                boogieExpr = Helpers.PrettyPrintBplExpr(kvp.Key);

-              } else {

+              bool runningOnBpl = CommandLineOptions.Clo.Files.Exists(fn => Path.GetExtension(fn).ToLower() == "bpl");

+              if (runningOnBpl) {

                 boogieExpr = kvp.Key.ToString();

+              } else {

+                boogieExpr = Helpers.PrettyPrintBplExpr(kvp.Key);

               }

               relatedInformation.Add("(internal state dump): " + string.Format("{0} == {1}", boogieExpr, o));

             }

diff --git a/Test/alltests.txt b/Test/alltests.txt
index e50d0a61..baffc2a1 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -27,6 +27,7 @@ dafny2           Use    More Dafny examples
 havoc0           Use    HAVOC-generated bpl files

 VSI-Benchmarks   Use    Solutions to Verified Software Initiative verification challenges

 vacid0           Use    Dafny attempts to VACID Edition 0 benchmarks

+vstte2012        Use    Dafny solutions for the VSTTE 2012 program verification competition

 livevars         Use    STORM benchmarks for testing correctness of live variable analysis

 lazyinline       Postponed    Lazy inlining benchmarks

 stratifiedinline Use    Stratified inlining benchmarks

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3198df33..15cec24f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -484,7 +484,8 @@ ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called w
 ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)

 ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)

 ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)

-44 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts

+45 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -1154,8 +1155,15 @@ Execution trace:
     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon5_Then

+Datatypes.dfy(198,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'

+Execution trace:

+    (0,0): anon0

+Datatypes.dfy(201,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

 

-Dafny program verifier finished with 29 verified, 3 errors

+Dafny program verifier finished with 29 verified, 5 errors

 

 -------------------- TypeAntecedents.dfy --------------------

 TypeAntecedents.dfy(32,13): Error: assertion violation

@@ -1313,12 +1321,33 @@ CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost
 Dafny program verifier finished with 22 verified, 0 errors

 

 -------------------- PredExpr.dfy --------------------

-PredExpr.dfy(23,15): Error: value assigned to a nat must be non-negative

+PredExpr.dfy(4,12): Error: condition in assert expression might not hold

+Execution trace:

+    (0,0): anon3_Else

+PredExpr.dfy(36,15): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

-PredExpr.dfy(36,17): Error: condition in assert expression might not hold

+PredExpr.dfy(49,17): Error: condition in assert expression might not hold

 Execution trace:

     (0,0): anon0

+PredExpr.dfy(74,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Else

+    (0,0): anon3

+    PredExpr.dfy(73,20): anon10_Else

+    (0,0): anon6

+

+Dafny program verifier finished with 11 verified, 4 errors

+

+-------------------- LetExpr.dfy --------------------

+LetExpr.dfy(5,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+LetExpr.dfy(104,21): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

 

-Dafny program verifier finished with 9 verified, 2 errors

+Dafny program verifier finished with 13 verified, 2 errors

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index eb527e0d..aff12fda 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -194,6 +194,17 @@ method InjectivityTests(d: XList)
   }

 }

 

+method MatchingDestructor(d: XList) returns (r: XList)

+  ensures r.Car == 5;  // error: specification is not well-formed (since r might not be an XCons)

+{

+  if (*) {

+    var x0 := d.Car;  // error: d might not be an XCons

+  } else if (d.XCons?) {

+    var x1 := d.Car;

+  }

+  r := XCons(5, XNil);

+}

+

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

 

 method FwdBug(f: Fwd, initialized: bool)

diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
new file mode 100644
index 00000000..703813d2
--- /dev/null
+++ b/Test/dafny0/LetExpr.dfy
@@ -0,0 +1,109 @@
+method M0(n: int)

+  requires var f := 100; n < f;

+{

+  assert n < 200;

+  assert 0 <= n;  // error

+}

+

+method M1()

+{

+  assert var f := 54; var g := f + 1; g == 55;

+}

+

+method M2()

+{

+  assert var f := 54; var f := f + 1; f == 55;

+}

+

+function method Fib(n: nat): nat

+{

+  if n < 2 then n else Fib(n-1) + Fib(n-2)

+}

+

+method M3(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6;

+  ensures (r + var t := r; t*2) == 3*r;

+{

+  assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3);

+

+  {

+    var x,y := Fib(8), Fib(11);

+    assume x == 21;

+    assert Fib(7) == 3 ==> Fib(9) == 24;

+    assume Fib(1000) == 1000;

+    assume Fib(9) - Fib(8) == 13;

+    assert Fib(9) <= Fib(10);

+    assert y == 89;

+  }

+

+  assert Fib(1000) == 1000;  // does it still know this?

+

+  parallel (i | 0 <= i < a.Length) ensures true; {

+    var j := i+1;

+    assert j < a.Length ==> a[i] == a[j];

+  }

+}

+

+// M4 is pretty much the same as M3, except with things rolled into expressions.

+method M4(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6;

+  ensures (r + var t := r; t*2) == 3*r;

+{

+  assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3);

+  assert

+    var x,y := Fib(8), Fib(11);

+    assume x == 21;

+    assert Fib(7) == 3 ==> Fib(9) == 24;

+    assume Fib(1000) == 1000;

+    assume Fib(9) - Fib(8) == 13;

+    assert Fib(9) <= Fib(10);

+    y == 89;

+  assert Fib(1000) == 1000;  // still known, because the assume was on the path here

+  assert forall i :: 0 <= i < a.Length ==> var j := i+1; j < a.Length ==> a[i] == a[j];

+}

+

+var index: int;

+method P(a: array<int>) returns (b: bool, ii: int)

+  requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;

+  modifies this, a;

+  ensures ii == index;

+  // The following uses a variable with a non-old definition inside an old expression:

+  ensures 0 <= index < a.Length && old(a[ii]) == 19;

+  ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19;

+  // The following places both the variable and the body inside an old:

+  ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17);

+  // Here, the definition of the variable is old, and it's used both inside and

+  // inside an old expression:

+  ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19;

+{

+  b := 0 <= index < a.Length && a[index] == 17;

+  var i, j := 0, -1;

+  while (i < a.Length)

+    invariant 0 <= i <= a.Length;

+    invariant forall k :: 0 <= k < i ==> a[k] == 21;

+    invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]);

+    invariant (0 <= j < i && old(a[j]) == 19) ||

+              (j == -1 && exists k :: i <= k < a.Length && a[k] == 19);

+  {

+    if (a[i] == 19) { j := i; }

+    i, a[i] := i + 1, 21;

+  }

+  index := j;

+  ii := index;

+}

+

+method PMain(a: array<int>)

+  requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;

+  modifies this, a;

+{

+  var s := a[..];

+  var b17, ii := P(a);

+  assert s == old(a[..]);

+  assert s[index] == 19;

+  if (*) {

+    assert a[index] == 19;  // error (a can have changed in P)

+  } else {

+    assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17;

+    assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;

+  }

+}

diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy
index 740c2308..96561ebd 100644
--- a/Test/dafny0/PredExpr.dfy
+++ b/Test/dafny0/PredExpr.dfy
@@ -1,3 +1,16 @@
+function SimpleAssert(n: int): int

+  ensures n < 100;

+{

+  assert n == 58;  // error: assert violation

+  n  // but postcondition is fine

+}

+

+function SimpleAssume(n: int): int

+  ensures n < 100;

+{

+  assume n == 58; n  // all is fine

+}

+

 function Subonacci(n: nat): nat

 {

   if 2 <= n then

@@ -18,7 +31,7 @@ function F(n: int): nat
 function G(n: int, b: bool): nat

 {

   if b then

-    Subonacci(assume 0 <= n; n)

+    Subonacci(assume 0 <= n; n) + n  // the last n is also affected by the assume

   else

     Subonacci(n)  // error: n may not be a nat

 }

@@ -49,3 +62,18 @@ function method FuncMeth(): int {
                       // PredicateExpr is not included in compilation

   15

 }

+

+method M5(a: int, b: int)

+{

+  var k := if a < 0 then

+             assume b < 0; 5

+           else

+             5;

+  if (*) {

+    assert a == -7 ==> b < 0;

+    assert b < 0;  // error: this condition does not hold on every path here

+  } else {

+    assert assume a == -7; b < 0;  // note, this is different than the ==> above

+    assert b < 0;  // this condition does hold on all paths to here

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 1b68ad91..e5e56d03 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -292,7 +292,7 @@ method ConstructorTests()
 

 // ------------------- datatype destructors ---------------------------------------

 

-datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List);

+datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int);

 

 method DatatypeDestructors(d: DTD_List) {

   if {

@@ -304,6 +304,8 @@ method DatatypeDestructors(d: DTD_List) {
       assert hd == d.Cdr;  // type error

       assert tl == d.Car;  // type error

       assert d.DTD_Cons? == d.Car;  // type error

-      assert d == DTD_Cons(hd, tl);

+      assert d == DTD_Cons(hd, tl, 5);

+      ghost var g0 := d.g;  // fine

+      var g1 := d.g;  // error: cannot use ghost member in non-ghost code

   }

 }

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 32a60340..18c23e55 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -20,7 +20,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

-            CallStmtTests.dfy MultiSets.dfy PredExpr.dfy) do (

+            CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer
new file mode 100644
index 00000000..15a95de1
--- /dev/null
+++ b/Test/vstte2012/Answer
@@ -0,0 +1,20 @@
+

+-------------------- Two-Way-Sort.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

+-------------------- Combinators.dfy --------------------

+

+Dafny program verifier finished with 25 verified, 0 errors

+

+-------------------- RingBuffer.dfy --------------------

+

+Dafny program verifier finished with 13 verified, 0 errors

+

+-------------------- Tree.dfy --------------------

+

+Dafny program verifier finished with 15 verified, 0 errors

+

+-------------------- BreadthFirstSearch.dfy --------------------

+

+Dafny program verifier finished with 24 verified, 0 errors

diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
new file mode 100644
index 00000000..5153b053
--- /dev/null
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -0,0 +1,276 @@
+class BreadthFirstSearch<Vertex>

+{

+  // The following function is left uninterpreted (for the purpose of the 

+  // verification problem, it can be thought of as a parameter to the class)

+  function method Succ(x: Vertex): set<Vertex>

+

+  // This is the definition of what it means to be a path "p" from vertex 

+  // "source" to vertex "dest"

+  function IsPath(source: Vertex, dest: Vertex, p: seq<Vertex>): bool

+  {

+    if source == dest then

+      p == []

+    else

+      p != [] && dest in Succ(p[|p|-1]) && IsPath(source, p[|p|-1], p[..|p|-1])

+  }

+

+  function IsClosed(S: set<Vertex>): bool  // says that S is closed under Succ

+  {

+    forall v :: v in S ==> Succ(v) <= S

+  }

+

+  // This is the main method to be verified.  Note, instead of using a 

+  // postcondition that talks about that there exists a path (such that ...), 

+  // this method returns, as a ghost out-parameter, that existential 

+  // witness.  The method could equally well have been written using an 

+  // existential quantifier and no ghost out-parameter.

+  method BFS(source: Vertex, dest: Vertex, ghost AllVertices: set<Vertex>) 

+         returns (d: int, ghost path: seq<Vertex>)

+    // source and dest are among AllVertices

+    requires source in AllVertices && dest in AllVertices;  

+    // AllVertices is closed under Succ

+    requires IsClosed(AllVertices);                         

+    // This method has two basic outcomes, as indicated by the sign of "d".  

+    // More precisely, "d" is non-negative iff "source" can reach "dest".

+    // The following postcondition says that under the "0 <= d" outcome, 

+    // "path" denotes a path of length "d" from "source" to "dest":

+    ensures 0 <= d ==> IsPath(source, dest, path) && |path| == d;

+    // Moreover, that path is as short as any path from "source" to "dest":

+    ensures 0 <= d ==> forall p :: IsPath(source, dest, p) ==> |path| <= |p|;

+    // Finally, under the outcome "d < 0", there is no path from "source" to "dest":

+    ensures d < 0 ==> !exists p :: IsPath(source, dest, p);

+  {

+    var V, C, N := {source}, {source}, {};

+    ghost var Processed, paths := {}, Maplet({source}, source, [], Empty);

+    // V - all encountered vertices

+    // Processed - vertices reachable from "source" is at most "d" steps

+    // C - unprocessed vertices reachable from "source" in "d" steps 

+    //     (but no less)

+    // N - vertices encountered and reachable from "source" in "d+1" steps 

+    //     (but no less)

+    d := 0;

+    var dd := Zero;

+    while (C != {})

+      // V, Processed, C, N are all subsets of AllVertices:

+      invariant V <= AllVertices && Processed <= AllVertices && C <= AllVertices && N <= AllVertices;

+      // source is encountered:

+      invariant source in V;

+      // V is the disjoint union of Processed, C, and N:

+      invariant V == Processed + C + N;

+      invariant Processed !! C !! N;  // Processed, C, and N are mutually disjoint

+      // "paths" records a path for every encountered vertex

+      invariant ValidMap(source, paths);

+      invariant V == Domain(paths);

+      // shortest paths for vertices in C have length d, and for vertices in N

+      // have length d+1

+      invariant forall x :: x in C ==> |Find(source, x, paths)| == d;

+      invariant forall x :: x in N ==> |Find(source, x, paths)| == d + 1;

+      // "dd" is just an inductive-looking way of writing "d":

+      invariant Value(dd) == d;

+      // "dest" is not reachable for any smaller value of "d":

+      invariant dest in R(source, dd, AllVertices) ==> dest in C;

+      invariant d != 0 ==> dest !in R(source, dd.predecessor, AllVertices);

+      // together, Processed and C are all the vertices reachable in at most d steps:

+      invariant Processed + C == R(source, dd, AllVertices);

+      // N are the successors of Processed that are not reachable within d steps:

+      invariant N == Successors(Processed, AllVertices) - R(source, dd, AllVertices);

+      // if we have exhausted C, then we have also exhausted N:

+      invariant C == {} ==> N == {};

+      // variant:

+      decreases AllVertices - Processed;

+    {

+      // remove a vertex "v" from "C"

+      var v := choose C;

+      C, Processed := C - {v}, Processed + {v};

+      ghost var pathToV := Find(source, v, paths);

+    

+      if (v == dest) {

+        parallel (p | IsPath(source, dest, p))

+          ensures |pathToV| <= |p|;

+        {

+          Lemma_IsPath_R(source, dest, p, AllVertices);

+          if (|p| < |pathToV|) {

+            // show that this branch is impossible

+            ToNat_Value_Bijection(|p|);

+            RMonotonicity(source, ToNat(|p|), dd.predecessor, AllVertices);

+          }

+        }

+        return d, pathToV;

+      }

+

+      // process newly encountered successors

+      var newlyEncountered := set w | w in Succ(v) && w !in V;

+      V, N := V + newlyEncountered, N + newlyEncountered;

+      paths := UpdatePaths(newlyEncountered, source, paths, v, pathToV);

+

+      if (C == {}) {

+        C, N, d, dd := N, {}, d+1, Suc(dd);

+      }

+    }

+

+    // show that "dest" in not in any reachability set, no matter 

+    // how many successors one follows

+    parallel (nn)

+      ensures dest !in R(source, nn, AllVertices);

+    {

+      if (Value(nn) < Value(dd)) {

+        RMonotonicity(source, nn, dd, AllVertices);

+      } else {

+        IsReachFixpoint(source, dd, nn, AllVertices);

+      }

+    }

+

+    // Now, show what what the above means in terms of IsPath.  More 

+    // precisely, show that there is no path "p" from "source" to "dest".

+    parallel (p | IsPath(source, dest, p))

+      // this and the previous two lines will establish the 

+      // absurdity of a "p" satisfying IsPath(source, dest, p)

+      ensures false;  

+    {

+      Lemma_IsPath_R(source, dest, p, AllVertices);

+      // a consequence of Lemma_IsPath_R is:  

+      // dest in R(source, ToNat(|p|), AllVertices)

+      // but that contradicts the conclusion of the preceding parallel statement

+    }

+

+    d := -1;  // indicate "no path"

+  }

+

+  // property of IsPath

+

+  ghost method Lemma_IsPath_Closure(source: Vertex, dest: Vertex, 

+                                p: seq<Vertex>, AllVertices: set<Vertex>)

+    requires IsPath(source, dest, p) && source in AllVertices && IsClosed(AllVertices);

+    ensures dest in AllVertices && forall v :: v in p ==> v in AllVertices;

+  {

+    if (p != []) {

+      var last := |p| - 1;

+      Lemma_IsPath_Closure(source, p[last], p[..last], AllVertices);

+    }

+  }

+

+  // operations on Nat

+

+  function Value(nn: Nat): nat

+    ensures ToNat(Value(nn)) == nn;

+  {

+    match nn

+    case Zero => 0

+    case Suc(mm) => Value(mm) + 1

+  }

+

+  function ToNat(n: nat): Nat

+  {

+    if n == 0 then Zero else Suc(ToNat(n - 1))

+  }

+

+  ghost method ToNat_Value_Bijection(n: nat)

+    ensures Value(ToNat(n)) == n;

+  {

+    // Dafny automatically figures out the inductive proof of the postcondition

+  }

+

+  // Reachability

+

+  function R(source: Vertex, nn: Nat, AllVertices: set<Vertex>): set<Vertex>

+  {

+    match nn

+    case Zero => {source}

+    case Suc(mm) =>  R(source, mm, AllVertices) + 

+                     Successors(R(source, mm, AllVertices), AllVertices)

+  }

+

+  function Successors(S: set<Vertex>, AllVertices: set<Vertex>): set<Vertex>

+  {

+    set w | w in AllVertices && exists x :: x in S && w in Succ(x)

+  }

+

+  ghost method RMonotonicity(source: Vertex, mm: Nat, nn: Nat, AllVertices: set<Vertex>)

+    requires Value(mm) <= Value(nn);

+    ensures R(source, mm, AllVertices) <= R(source, nn, AllVertices);

+    decreases Value(nn) - Value(mm);

+  {

+    if (Value(mm) < Value(nn)) {

+      RMonotonicity(source, Suc(mm), nn, AllVertices);

+    }

+  }

+

+  ghost method IsReachFixpoint(source: Vertex, mm: Nat, nn: Nat, AllVertices: set<Vertex>)

+    requires R(source, mm, AllVertices) == R(source, Suc(mm), AllVertices);

+    requires Value(mm) <= Value(nn);

+    ensures R(source, mm, AllVertices) == R(source, nn, AllVertices);

+    decreases Value(nn) - Value(mm);

+  {

+    if (Value(mm) < Value(nn)) {

+      IsReachFixpoint(source, Suc(mm), nn, AllVertices);

+    }

+  }

+

+  ghost method Lemma_IsPath_R(source: Vertex, x: Vertex, 

+                              p: seq<Vertex>, AllVertices: set<Vertex>)

+    requires IsPath(source, x, p) && source in AllVertices && IsClosed(AllVertices);

+    ensures x in R(source, ToNat(|p|), AllVertices);

+  {

+    if (p != []) {

+      Lemma_IsPath_Closure(source, x, p, AllVertices);

+      var last := |p| - 1;

+      Lemma_IsPath_R(source, p[last], p[..last], AllVertices);

+    }

+  }

+

+  // operations on Map's

+

+  function Domain(m: Map<Vertex>): set<Vertex>

+  {

+//    if m.Maplet? then m.dom else {}

+//    if m == Empty then {} else assert m.Maplet?; m.dom

+    match m

+    case Empty => {}

+    case Maplet(dom, t, s, nxt) => dom

+  }

+

+  // ValidMap encodes the consistency of maps (think, invariant).

+  // An explanation of this idiom is explained in the README file.

+  function ValidMap(source: Vertex, m: Map<Vertex>): bool

+  {

+    match m

+    case Empty =>  true

+    case Maplet(dom, v, path, next) =>

+      v in dom && dom == Domain(next) + {v} &&

+      IsPath(source, v, path) &&

+      ValidMap(source, next)

+  }

+

+  function Find(source: Vertex, x: Vertex, m: Map<Vertex>): seq<Vertex>

+    requires ValidMap(source, m) && x in Domain(m);

+    ensures IsPath(source, x, Find(source, x, m));

+  {

+    match m

+    case Maplet(dom, v, path, next) =>

+      if x == v then path else Find(source, x, next)

+  }

+

+  ghost method UpdatePaths(vSuccs: set<Vertex>, source: Vertex, 

+                    paths: Map<Vertex>, v: Vertex, pathToV: seq<Vertex>) 

+               returns (newPaths: Map<Vertex>)

+    requires ValidMap(source, paths);

+    requires vSuccs !! Domain(paths);

+    requires forall succ :: succ in vSuccs ==> IsPath(source, succ, pathToV + [v]);

+    ensures ValidMap(source, newPaths) && Domain(newPaths) == Domain(paths) + vSuccs;

+    ensures forall x :: x in Domain(paths) ==> 

+                        Find(source, x, paths) == Find(source, x, newPaths);

+    ensures forall x :: x in vSuccs ==> Find(source, x, newPaths) == pathToV + [v];

+  {

+    if (vSuccs == {}) {

+      newPaths := paths;

+    } else {

+      var succ := choose vSuccs;

+      newPaths := Maplet(Domain(paths) + {succ}, succ, pathToV + [v], paths);

+      newPaths := UpdatePaths(vSuccs - {succ}, source, newPaths, v, pathToV);

+    }

+  }

+}

+

+datatype Map<T> = Empty | Maplet(dom: set<T>, T, seq<T>, next: Map<T>);

+

+datatype Nat = Zero | Suc(predecessor: Nat);

diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy
new file mode 100644
index 00000000..46daf48d
--- /dev/null
+++ b/Test/vstte2012/Combinators.dfy
@@ -0,0 +1,459 @@
+// Problem 2 concerns an interpreter for the language of S and K combinators.

+

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

+// Definitions

+

+// First, we define the language of combinator terms.  "Apply(x, y)" is what

+// the problem description writes as "(x y)".  In the following Dafny

+// definition, "car" and "cdr" are declared to be destructors for terms

+// constructed by Apply.

+

+datatype Term = S | K | Apply(car: Term, cdr: Term);

+

+// The problem defines values to be a subset of the terms.  More precisely,

+// a Value is a Term that fits the following grammar:

+//     Value = K | S | (K Value) | (S Value) | ((S Value) Value)

+// The following predicate says whether or not a given term is a value.

+

+function method IsValue(t: Term): bool

+  ensures IsValue(t) && t.Apply? ==> IsValue(t.car) && IsValue(t.cdr);

+{

+  match t

+  case K => true

+  case S => true

+  case Apply(a, b) =>

+    match a

+    case K =>

+      assert IsValue(a);

+      IsValue(b)

+    case S =>

+      assert IsValue(a);

+      IsValue(b)

+    case Apply(x, y) =>

+      assert x==S && IsValue(y) && IsValue(b) ==> IsValue(a);

+      x==S && IsValue(y) && IsValue(b)

+}

+

+// A context is essentially a term with one missing subterm, a "hole".  It

+// is defined as follows:

+

+datatype Context = Hole | C_term(Context, Term) | value_C(Term/*Value*/, Context);

+

+// The problem seems to suggest that the value_C form requires a value and

+// a context.  To formalize that notion, we define a predicate that checks this

+// condition.

+

+function IsContext(C: Context): bool

+{

+  match C

+  case Hole => true                                   // []

+  case C_term(D, t) => IsContext(D)                   // (D t)

+  case value_C(v, D) => IsValue(v) && IsContext(D)    // (v D)

+}

+

+// The EvalExpr function replace the hole in a context with a given term.

+

+function EvalExpr(C: Context, t: Term): Term

+  requires IsContext(C);

+{

+  match C

+  case Hole => t

+  case C_term(D, u) => Apply(EvalExpr(D, t), u)

+  case value_C(v, D) => Apply(v, EvalExpr(D, t))

+}

+

+// A term can be reduced.  This reduction operation is defined via

+// a single-step reduction operation.  In the problem, the single-step

+// reduction has the form:

+//   C[t] --> C[r]

+// We formalize the single-step reduction by a function Step, which

+// performs the reduction if it applies or just returns the given term

+// if it does.  We will say that "Step applies" to refer to the first

+// case, which is a slight abuse of language, since the function "Step"

+// is total.

+//

+// Since the context C is the same on both sides in the single-step

+// reduction above, we don't pass it to function Step.  Rather, Step

+// just takes a term "t" and returns the following:

+//     match t

+//     case ((K v1) v2) => v1

+//     case (((S v1) v2) v3) => ((v1 v3) (v2 v3))

+//     else t

+// As you can see below, it takes more lines than shown here to express

+// this matching in Dafny, but this is all that Step does.

+//

+// Again, note that Step returns the given term if neither or the two

+// vs in the problem statement applies.

+//

+// One more thing:  Step has a postcondition (and the body of Step

+// contains three asserts that act as lemmas in proving the postcondition).

+// The postcondition has been included for the benefit of Verification

+// Task 2, and we describe the functions used in the Step postcondition

+// only much later in this file.  For now, the postcondition can be

+// ignored, since it is, after all, just a consequence of the body

+// of Step.

+

+function method Step(t: Term): Term

+  ensures !ContainsS(t) ==>

+             !ContainsS(Step(t)) &&

+             (Step(t) == t || TermSize(Step(t)) < TermSize(t));

+{

+  match t

+  case S => t

+  case K => t

+  case Apply(x, y) =>

+    match x

+    case S => t

+    case K => t

+    case Apply(m, n) =>

+      if m == K && IsValue(n) && IsValue(y) then

+        // this is the case t == Apply(Apply(K, n), y)

+        assert !ContainsS(t) ==> !ContainsS(x);

+        assert TermSize(n) < TermSize(Apply(m, n));

+        n

+      else if m.Apply? && m.car == S && IsValue(m.cdr) && IsValue(n) && IsValue(y) then

+        // t == Apply(Apply(Apply(S, m.cdr), n), y)

+        assert ContainsS(m) && ContainsS(t);

+        Apply(Apply(m.cdr, y), Apply(n, y))

+      else

+        t

+}

+

+// The single-step reduction operation may be applied to any subexpression

+// of a term that could be considered a hole.  Function FindAndStep

+// searches for a (context, term) pair C[u] that denotes a given term "t"

+// such that Step applies to "u".  If found, the function returns

+// C[Step(u)], which will necessarily be different from "t".  If no such

+// C[u] pair exists, this function returns the given "t".

+//

+// Note, FindAndStep only applies one Step.  We will get to repeated

+// applications of steps in the "reduction" method below.

+//

+// For all definitions above, it was necessary to check (manually) that

+// they correspond to the definitions intended in the problem statement.

+// That is, the definitions above are all part of the specification.

+// For function FindAndStep, the definition given does not require

+// such scrutiny.  Rather, we will soon state a theorem that states

+// the properties of what FindAndStep returns.

+//

+// Like Step, FindAndStep has a postcondition, and it is also included to

+// support Verification Task 2.

+

+function method FindAndStep(t: Term): Term

+  ensures !ContainsS(t) ==>

+             !ContainsS(FindAndStep(t)) &&

+             (FindAndStep(t) == t || TermSize(FindAndStep(t)) < TermSize(t));

+{

+  if Step(t) != t then

+    Step(t)

+  else if !t.Apply? then

+    t

+  else if FindAndStep(t.car) != t.car then

+    Apply(FindAndStep(t.car), t.cdr)

+  else if IsValue(t.car) && FindAndStep(t.cdr) != t.cdr then

+    Apply(t.car, FindAndStep(t.cdr))

+  else

+    t

+}

+

+// One part of the correctness of FindAndStep (and, indeed, of method

+// "reduction" below) is that a term can be terminal, meaning that there is

+// no way to apply Step to any part of it.

+

+function IsTerminal(t: Term): bool

+{

+  !(exists C,u :: IsContext(C) && t == EvalExpr(C,u) && Step(u) != u)

+}

+

+// The following theorem states the correctness of the FindAndStep function:

+

+ghost method Theorem_FindAndStep(t: Term)

+  // If FindAndStep returns the term it started from, then there is no

+  // way to take a step.  More precisely, there is no C[u] == t for which the

+  // Step applies to "u".

+  ensures FindAndStep(t) == t ==> IsTerminal(t);

+  // If FindAndStep returns a term that's different from what it started with,

+  // then it chose some C[u] == t for which the Step applies to "u", and then

+  // it returned C[Step(u)].

+  ensures FindAndStep(t) != t ==>

+          exists C,u :: IsContext(C) && t == EvalExpr(C,u) && Step(u) != u &&

+                        FindAndStep(t) == EvalExpr(C, Step(u));

+{

+  // The theorem follows from the following lemma, which itself is proved by

+  // induction.

+  var r, C, u := Lemma_FindAndStep(t);

+}

+

+// This is the lemma that proves the theorem above.  Whereas the theorem talks

+// existentially about C and u, the lemma constructs C and u and returns them,

+// which is useful in the proof by induction.  The computation inside the

+// lemma mimicks that done by function FindAndStep; indeed, the lemma

+// computes the value of FindAndStep(t) as it goes along and it returns

+// that value.

+

+ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)

+  ensures r == FindAndStep(t);

+  ensures r == t ==> IsTerminal(t);

+  ensures r != t ==>

+            IsContext(C) && t == EvalExpr(C,u) && Step(u) != u &&

+            r == EvalExpr(C, Step(u));

+{

+  Lemma_ContextPossibilities(t);

+  if (Step(t) != t) {

+    // t == Hole[t] and Step applies t.  So, return Hole[Step(t)]

+    return Step(t), Hole, t;

+  } else if (!t.Apply?) {

+    r := t;

+  } else {

+    r, C, u := Lemma_FindAndStep(t.car);  // (*)

+    if (r != t.car) {

+      // t has the form (a b) where a==t.car and b==t.cdr, and a==C[u] for some

+      // context C and some u to which the Step applies.  t can therefore be

+      // denoted by (C[u] b) == (C b)[u] and the Step applies to u.  So, return

+      // (C b)[Step(u)] == (C[Step(u)] b).  Note that FindAndStep(a)

+      // gives C[Step(u)].

+      return Apply(r, t.cdr), C_term(C, t.cdr), u;

+    } else if (IsValue(t.car)) {

+      r, C, u := Lemma_FindAndStep(t.cdr);

+      assert IsTerminal(t.car);  // make sure this is still remembered from (*)

+

+      if (r != t.cdr) {

+        // t has the form (a b) where a==t.car and b==t.cdr and "a" is a Value,

+        // and b==C[u] for some context C and some u to which the Step applies.

+        // t can therefore be denoted by (a C[u]) == (C a)[u] and the Step

+        // applies to u.  So, return (C a)[Step(u)] == (a C[Step(u)]).  Note

+        // that FindAndStep(b) gives C[Step(u)].

+        return Apply(t.car, r), value_C(t.car, C), u;

+      } else {

+        parallel (C,u | IsContext(C) && t == EvalExpr(C,u))

+          ensures Step(u) == u;

+        {

+          // The following assert and the first assert of each "case" are

+          // consequences of the Lemma_ContextPossibilities that was invoked

+          // above.

+          assert t.Apply? && IsValue(t.car);

+          match (C) {

+            case Hole =>

+              assert t == u;

+            case C_term(D, bt) =>

+              assert bt == t.cdr && t.car == EvalExpr(D, u);

+            case value_C(at, D) =>

+              assert at == t.car && t.cdr == EvalExpr(D, u);

+          }

+        }

+        r := t;

+      }

+    } else {

+      r := t;

+    }

+  }

+}

+

+// The proof of the lemma above used one more lemma, namely one that enumerates

+// lays out the options for how to represent a term as a C[u] pair.

+

+ghost method Lemma_ContextPossibilities(t: Term)

+  ensures forall C,u :: IsContext(C) && t == EvalExpr(C, u) ==>

+    (C == Hole && t == u) ||

+    (t.Apply? && exists D :: C == C_term(D, t.cdr) && t.car == EvalExpr(D, u)) ||

+    (t.Apply? && IsValue(t.car) &&

+        exists D :: C == value_C(t.car, D) && t.cdr == EvalExpr(D, u));

+{

+  // Dafny's induction tactic rocks

+}

+

+// We now define a way to record a sequence of reduction steps.

+// IsTrace(trace, t, r) returns true iff "trace" gives witness to a

+// sequence of terms from "t" to "r", each term reducing to its

+// successor in the trace.

+

+datatype Trace = EmptyTrace | ReductionStep(Trace, Term);

+

+function IsTrace(trace: Trace, t: Term, r: Term): bool

+{

+  match trace

+  case EmptyTrace =>

+    t == r

+  case ReductionStep(tr, u) =>

+    IsTrace(tr, t, u) && FindAndStep(u) == r

+}

+

+// Finally, we are ready to give the requested routine "reduction", which

+// keeps applying FindAndStep until quiescence, that is, until Step

+// no longer applies.

+//

+// As required by Verification Task 1, the "reduction" method has two

+// postconditions.  One says that the term returned, "r", was obtained

+// from the original term, "t", by a sequence of reduction steps.  The

+// other says that "r" cannot be reduced any further.

+//

+// Unlike the other competition problems, this one requested code

+// (for "reduction") that may not terminate.  In order to allow reasoning

+// about algorithms that may never terminate, Dafny has a special loop

+// statement (a "while" loop with a declaration "decreases *") that

+// thus comes in handy for "reduction".  (Dafny never allows recursion

+// to be non-terminating, only these special loops.)  Note that use

+// of the special loop statement does not have any effect on the

+// specifications of the enclosing method (but this may change in a

+// future version of Dafny).

+

+method reduction(t: Term) returns (r: Term)

+  // The result was obtained by a sequence of reductions:

+  ensures exists trace :: IsTrace(trace, t, r);

+  // The result "r" cannot be reduced any further:

+  ensures IsTerminal(r);

+{

+  r := t;

+  ghost var trace := EmptyTrace;

+  while (true)

+    invariant IsTrace(trace, t, r);

+    decreases *;  // allow this statement to loop forever

+  {

+    var u := FindAndStep(r);

+    if (u == r) {

+      // we have found a fixpoint

+      Theorem_FindAndStep(r);

+      return;

+    }

+    r, trace := u, ReductionStep(trace, r);

+  }

+}

+

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

+// Verification Task 2

+//

+// This part of the problem asks us to consider the reduction of terms that

+// do not contain S.  The following function formalizes what it means for a term

+// to contain S:

+

+function method ContainsS(t: Term): bool

+{

+  match t

+  case S => true

+  case K => false

+  case Apply(x, y) => ContainsS(x) || ContainsS(y)

+}

+

+// The verification task itself is to prove that "reduction" terminates on any

+// term that does not contain S.  To prove this, we need to supply a loop variant

+// for the loop in "reduction".  However, Dafny does not allow one loop to be

+// proved to terminate in some cases and allowed not to terminate in other cases.

+// There, we meet Verification Task 2 by manually copying the body of "reduction"

+// into a new method (called VerificationTask2) and proving that this new method

+// terminates.  Of course, Dafny does not check that we copy the body correctly,

+// so that needs to be checked by a human.

+//

+// In method VerificationTask2, we added not just the precondition given in the

+// Verification Task and a loop variant, but we also added two loop invariants

+// and one more postcondition.  One of the loop invariants keep track of that

+// there are no S's.  The other loop invariant and the postcondition are for

+// the benefit of Verification Task 3, as we explain later.

+

+method VerificationTask2(t: Term) returns (r: Term)

+  requires !ContainsS(t);  // a sufficient condition for termination

+  // The result was obtained by a sequence of reductions:

+  ensures exists trace :: IsTrace(trace, t, r);

+  // The result "r" cannot be reduced any further:

+  ensures IsTerminal(r);

+  // Later in this file, we define a function TerminatingReduction, and the

+  // following postcondition says that TerminatingReduction computes the same

+  // term as this method does.

+  ensures r == TerminatingReduction(t);

+{

+  r := t;

+  ghost var trace := EmptyTrace;

+  while (true)

+    invariant IsTrace(trace, t, r) && !ContainsS(r);

+    invariant TerminatingReduction(t) == TerminatingReduction(r);

+    decreases TermSize(r);

+  {

+    var u := FindAndStep(r);

+    if (u == r) {

+      // we have found a fixpoint

+      Theorem_FindAndStep(r);

+      return;

+    }

+    r, trace := u, ReductionStep(trace, r);

+  }

+}

+

+// What now follows is the definition TermSize, which is used in the

+// loop variant.  When a Step is applied to a term without S, TermSize

+// is reduced, which is stated as a postcondition of both Step and

+// FindAndStep.  That postcondition of FindAndStep is used in the

+// proof of termination of method VerificationTask2.

+

+// The loop variant is simply the count of nodes in the term:

+

+function TermSize(t: Term): nat

+{

+  match t

+  case S => 1

+  case K => 1

+  case Apply(x, y) => 1 + TermSize(x) + TermSize(y)

+}

+

+// We have already given two methods for computing a reduction:

+// method "reduction", which may or may not terminate, and method

+// "VerificationTask2", whose precondition is strong enough to let

+// us prove that the method will terminate.  The correspondence

+// between the two methods is checked by hand, seeing that

+// VerificationTask2 includes the postconditions of "reduction" and

+// seeing that the code is the same.

+//

+// We now define a third way of computing reductions, this time

+// using a function (not a method).  To prove that this function

+// computes the same thing as method VerificationTask2, we had

+// added a postcondition to VerificationTask2 above.  This function

+// is introduced for the benefit of stating and verifying Verification

+// Task 3.

+

+function TerminatingReduction(t: Term): Term

+  requires !ContainsS(t);  // a sufficient condition for termination

+  decreases TermSize(t);

+{

+  if FindAndStep(t) == t then

+    t  // we have reached a fixpoint

+  else

+    TerminatingReduction(FindAndStep(t))

+}

+

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

+// Verification Task 3

+

+// Here is the function "ks" from Verification Task 3.  It produces a particular

+// family of terms that contain only Apply and K.  Hence, we can establish, as a

+// postcondition of the function, that ks(n) does not contain S.

+

+function method ks(n: nat): Term

+  ensures !ContainsS(ks(n));

+{

+  if n == 0 then K else Apply(ks(n-1), K)

+}

+

+// Verification Task 3 is now established by the following theorem.  It says

+// that reducing ks(n) results in either K and (K K), depending on the parity

+// of n.  The theorem uses function TerminatingReduction to speak of the

+// reduction--remember that (by the last postcondition of method

+// VerificationTask2) it computes the same thing as method VerificationTask2

+// does.

+

+ghost method VerificationTask3()

+  ensures forall n: nat ::

+    TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);

+{

+  parallel (n: nat) {

+    VT3(n);

+  }

+}

+

+ghost method VT3(n: nat)

+  ensures TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);

+{

+  // Dafny's (way cool) induction tactic kicks in and proves the following

+  // assertion automatically:

+  assert forall p :: 2 <= p ==> FindAndStep(ks(p)) == ks(p-2);

+  // And then Dafny's (cool beyond words) induction tactic for ghost methods kicks

+  // in to prove the postcondition.  (If this got you curious, scope out Leino's

+  // VMCAI 2012 paper "Automating Induction with an SMT Solver".)

+}

diff --git a/Test/vstte2012/RingBuffer.dfy b/Test/vstte2012/RingBuffer.dfy
new file mode 100644
index 00000000..5262e462
--- /dev/null
+++ b/Test/vstte2012/RingBuffer.dfy
@@ -0,0 +1,93 @@
+class RingBuffer<T>

+{

+  // public fields that are used to define the abstraction:

+  ghost var Contents: seq<T>;  // the contents of the ring buffer

+  ghost var N: nat;  // the capacity of the ring buffer

+  ghost var Repr: set<object>;  // the set of objects used in the implementation

+

+  // Valid encodes the consistency of RingBuffer objects (think, invariant).

+  // An explanation of this idiom is explained in the README file.

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr && null !in Repr &&

+    data != null && data in Repr &&

+    data.Length == N &&

+    (N == 0 ==> len == first == 0 && Contents == []) &&

+    (N != 0 ==> len <= N && first < N) &&

+    Contents == if first + len <= N then data[first..first+len] 

+                                    else data[first..] + data[..first+len-N]

+  }

+

+  // private implementation:

+  var data: array<T>;

+  var first: nat;

+  var len: nat;

+

+  constructor Create(n: nat)

+    modifies this;

+    ensures Valid() && fresh(Repr - {this});

+    ensures Contents == [] && N == n;

+  {

+    Repr := {this};

+    data := new T[n];

+    Repr := Repr + {data};

+    first, len := 0, 0;

+    Contents, N := [], n;

+  }

+

+  method Clear()

+    requires Valid();

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures Contents == [] && N == old(N);

+  {

+    len := 0;

+    Contents := [];

+  }

+

+  method Head() returns (x: T)

+    requires Valid();

+    requires Contents != [];

+    ensures x == Contents[0];

+  {

+    x := data[first];

+  }

+

+  method Push(x: T)

+    requires Valid();

+    requires |Contents| != N;

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures Contents == old(Contents) + [x] && N == old(N);

+  {

+    var nextEmpty := if first + len < data.Length 

+                     then first + len else first + len - data.Length;

+    data[nextEmpty] := x;

+    len := len + 1;

+    Contents := Contents + [x];

+  }

+

+  method Pop() returns (x: T)

+    requires Valid();

+    requires Contents != [];

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);

+  {

+    x := data[first];

+    first, len := if first + 1 == data.Length then 0 else first + 1, len - 1;

+    Contents := Contents[1..];

+  }

+}

+

+method TestHarness(x: int, y: int, z: int)

+{

+  var b := new RingBuffer<int>.Create(2);

+  b.Push(x);

+  b.Push(y);

+  var h := b.Pop();  assert h == x;

+  b.Push(z);

+  h := b.Pop();  assert h == y;

+  h := b.Pop();  assert h == z;

+}

diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy
new file mode 100644
index 00000000..47ed19a4
--- /dev/null
+++ b/Test/vstte2012/Tree.dfy
@@ -0,0 +1,172 @@
+// The tree datatype

+datatype Tree = Leaf | Node(Tree, Tree);

+

+

+// This datatype is used for the result of the build functions.

+// These functions either fail or yield a tree. Since we use

+// a side-effect free implementation of the helper

+// build_rec, it also has to yield the rest of the sequence,

+// which still needs to be processed. For function build,

+// this part is not used.

+datatype Result = Fail | Res(t: Tree, sOut: seq<int>);

+

+

+// Function toList converts a tree to a sequence.

+// We use Dafny's built-in value type sequence rather than

+// an imperative implementation to simplify verification.

+// The argument d is added to each element of the sequence;

+// it is analogous to the argument d in build_rec.

+// The postconditions state properties that are needed

+// in the completeness proof.

+function toList(d: int, t: Tree): seq<int>

+  ensures toList(d, t) != [] && toList(d, t)[0] >= d;

+  ensures (toList(d, t)[0] == d) == (t == Leaf);

+  decreases t;

+{

+  match t 

+  case Leaf => [d]

+  case Node(l, r) => toList(d+1, l) + toList(d+1, r)

+}

+

+

+// Function build_rec is a side-effect free implementation

+// of the code given in the problem statement.

+// The first postcondition is needed to show that the

+// termination measure indeed decreases.

+// The second postcondition specifies the soundness

+// property; converting the resulting tree back into a

+// sequence yields exactly that portion of the input

+// sequence that has been consumed.

+function method build_rec(d: int, s: seq<int>): Result

+  ensures build_rec(d, s).Res? ==>

+            |build_rec(d, s).sOut| < |s| && 

+            build_rec(d, s).sOut == s[|s|-|build_rec(d, s).sOut|..];

+  ensures build_rec(d, s).Res? ==> 

+            toList(d,build_rec(d, s).t) == s[..|s|-|build_rec(d, s).sOut|];

+  decreases |s|, (if s==[] then 0 else s[0]-d);    

+{

+  if s==[] || s[0] < d then

+    Fail

+  else if s[0] == d then

+    Res(Leaf, s[1..])

+  else

+    var left := build_rec(d+1, s);

+    if left.Fail? then Fail else

+    var right := build_rec(d+1, left.sOut);

+    if right.Fail? then Fail else

+    Res(Node(left.t, right.t), right.sOut)

+}

+

+

+// Function build is a side-effect free implementation

+// of the code given in the problem statement.

+// The postcondition specifies the soundness property;

+// converting the resulting tree back into a

+// sequence yields exactly the input sequence.

+// Completeness is proved as a lemma, see below.

+function method build(s: seq<int>): Result

+  ensures build(s).Res? ==> toList(0,build(s).t) == s;

+{

+  var r := build_rec(0, s);

+  if r.Res? && r.sOut == [] then r else Fail

+}

+

+

+// This ghost methods encodes the main lemma for the

+// completeness theorem. If a sequence s starts with a

+// valid encoding of a tree t then build_rec yields a

+// result (i.e., does not fail) and the rest of the sequence.

+// The body of the method proves the lemma by structural

+// induction on t. Dafny proves termination (using the

+// height of the term t as termination measure), which

+// ensures that the induction hypothesis is applied

+// correctly (encoded by calls to this ghost method).

+ghost method lemma0(t: Tree, d: int, s: seq<int>)

+  ensures build_rec(d, toList(d, t) + s).Res? && 

+          build_rec(d, toList(d, t) + s).sOut == s;

+{

+  match(t) {

+  case Leaf =>

+    assert toList(d, t) == [d];

+  case Node(l, r) =>

+    assert toList(d, t) + s == toList(d+1, l) + (toList(d+1, r) + s);

+

+    lemma0(l, d+1, toList(d+1, r) + s);  // apply the induction hypothesis

+    lemma0(r, d+1, s);  // apply the induction hypothesis

+  }

+}

+

+

+// This ghost method encodes a lemma that states the

+// completeness property. It is proved by applying the

+// main lemma (lemma0). In this lemma, the bound variables

+// of the completeness theorem are passed as arguments;

+// the following two ghost methods replace these arguments

+// by quantified variables.

+ghost method lemma1(t: Tree, s:seq<int>)

+  requires s == toList(0, t) + [];

+  ensures  build(s).Res?;

+{

+  lemma0(t, 0, []);

+}

+

+

+// This ghost method encodes a lemma that introduces the

+// existential quantifier in the completeness property.

+ghost method lemma2(s: seq<int>)

+  ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?;

+{

+  parallel(t | toList(0,t) == s) {

+    lemma1(t, s);

+  } 

+}

+

+

+// This ghost method encodes the completeness theorem.

+// For each sequence for which there is a corresponding 

+// tree, function build yields a result different from Fail.

+// The body of the method converts the argument of lemma2

+// into a universally quantified variable.

+ghost method completeness()

+  ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?);

+{

+  parallel(s) {

+    lemma2(s);

+  }

+}

+

+

+// This method encodes the first test harness

+// given in the problem statement. The local

+// assertions are required by the verifier to

+// unfold the necessary definitions.

+method harness0()

+  ensures build([1,3,3,2]).Res? &&

+          build([1,3,3,2]).t == Node(Leaf, Node(Node(Leaf, Leaf), Leaf));

+{

+  assert build_rec(2, [2]) ==

+         Res(Leaf, []);

+  assert build_rec(2, [3,3,2]) ==

+         Res(Node(Leaf, Leaf), [2]);

+  assert build_rec(1, [3,3,2]) ==

+         Res(Node(Node(Leaf, Leaf), Leaf), []);

+  assert build_rec(1, [1,3,3,2]) ==

+         Res(Leaf, [3,3,2]);

+  assert build_rec(0, [1,3,3,2]) ==

+         Res(

+           Node(build_rec(1, [1,3,3,2]).t,

+                build_rec(1, [3,3,2]).t),

+           []);

+}

+

+

+// This method encodes the second test harness

+// given in the problem statement. The local

+// assertions are required by the verifier to

+// unfold the necessary definitions.

+method harness1()

+  ensures build([1,3,2,2]).Fail?;

+{

+  assert build_rec(3, [2,2]).Fail?;

+  assert build_rec(1, [3,2,2]).Fail?;

+}

diff --git a/Test/vstte2012/Two-Way-Sort.dfy b/Test/vstte2012/Two-Way-Sort.dfy
new file mode 100644
index 00000000..49ff29b4
--- /dev/null
+++ b/Test/vstte2012/Two-Way-Sort.dfy
@@ -0,0 +1,58 @@
+// This method is a slight generalization of the

+// code provided in the problem statement since it

+// is generic in the type of the array elements.

+method swap<T>(a: array<T>, i: int, j: int)

+  requires a != null;

+  requires 0 <= i < j < a.Length;

+  modifies a;

+  ensures a[i] == old(a[j]);

+  ensures a[j] == old(a[i]);

+  ensures forall m :: 0 <= m < a.Length && m != i && m != j ==> a[m] == old(a[m]);

+  ensures multiset(a[..]) == old(multiset(a[..]));

+{

+  var t := a[i];

+  a[i] := a[j];

+  a[j] := t;

+}

+

+// This method is a direct translation of the pseudo

+// code given in the problem statement. 

+// The first postcondition expresses that the resulting

+// array is sorted, that is, all occurrences of "false"

+// come before all occurrences of "true".

+// The second postcondition expresses that the post-state 

+// array is a permutation of the pre-state array. To express

+// this, we use Dafny's built-in multisets. The built-in 

+// function "multiset" takes an array and yields the 

+// multiset of the array elements.

+// Note that Dafny guesses a suitable ranking function

+// for the termination proof of the while loop.

+// We use the loop guard from the given pseudo-code.  However,

+// the program also verifies with the stronger guard "i < j"

+// (without changing any of the other specifications or

+// annotations).

+method two_way_sort(a: array<bool>)

+  requires a != null;

+  modifies a;

+  ensures forall m,n :: 0 <= m < n < a.Length ==> (!a[m] || a[n]);

+  ensures multiset(a[..]) == old(multiset(a[..]));

+{

+  var i := 0;

+  var j := a.Length - 1;

+  while (i <= j)

+    invariant 0 <= i <= j + 1 <= a.Length;

+    invariant forall m :: 0 <= m < i ==> !a[m];

+    invariant forall n :: j < n < a.Length ==> a[n];

+    invariant multiset(a[..]) == old(multiset(a[..]));

+  {

+    if (!a[i]) {

+      i := i+1;

+    } else if (a[j]) {

+      j := j-1;

+    } else {

+      swap(a, i, j);

+      i := i+1;

+      j := j-1;

+    }

+  }

+}

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
new file mode 100644
index 00000000..07b5859e
--- /dev/null
+++ b/Test/vstte2012/runtest.bat
@@ -0,0 +1,24 @@
+@echo off

+setlocal

+

+set BOOGIEDIR=..\..\Binaries

+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

+

+for %%f in (

+    Two-Way-Sort.dfy

+    Combinators.dfy

+    RingBuffer.dfy

+    Tree.dfy

+    BreadthFirstSearch.dfy

+  ) do (

+  echo.

+  echo -------------------- %%f --------------------

+

+  REM The following line will just run the verifier

+  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

+

+  REM Alternatively, the following lines also produce C# code and compile it

+  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

+  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

+)

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index 3c2393bb..19a5e1df 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -7,7 +7,7 @@ using System.Diagnostics;
 using System.Diagnostics.Contracts;

 // Here come the Dafny/Boogie specific imports

 //using PureCollections;

-using Microsoft.Boogie;

+using Bpl = Microsoft.Boogie;

 using Dafny = Microsoft.Dafny;

 using Microsoft.Boogie.AbstractInterpretation;

 using VC;

@@ -112,10 +112,9 @@ namespace DafnyLanguage
     }

 

     static void Initialize() {

-      CommandLineOptions.Clo.RunningBoogieOnSsc = false;

-      CommandLineOptions.Clo.TheProverFactory = ProverFactory.Load("Z3");

-      CommandLineOptions.Clo.ProverName = "Z3";

-      CommandLineOptions.Clo.vcVariety = CommandLineOptions.Clo.TheProverFactory.DefaultVCVariety;

+      if (Dafny.DafnyOptions.O == null) {

+        Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());

+      }

     }

 

     public Dafny.Program Process() {

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index 55f2ee34..4ae02e17 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -76,14 +76,6 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\..\..\Binaries\VCGeneration.dll</HintPath>

     </Reference>

-    <Reference Include="System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>

-    </Reference>

-    <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="EnvDTE, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">

       <EmbedInteropTypes>False</EmbedInteropTypes>

     </Reference>

@@ -130,8 +122,6 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BufferIdleEventUtil.cs" />

-    <Compile Include="Visitor.cs" />

-    <Compile Include="IdentifierTagger.cs" />

     <Compile Include="OutliningTagger.cs" />

     <Compile Include="ResolverTagger.cs" />

     <Compile Include="DafnyDriver.cs" />

@@ -145,7 +135,6 @@
     <Compile Include="Properties\AssemblyInfo.cs" />

   </ItemGroup>

   <ItemGroup>

-    <None Include="app.config" />

     <None Include="source.extension.vsixmanifest">

       <SubType>Designer</SubType>

     </None>

diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index 3ecae08a..80aa8d7e 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,15 +1,15 @@
-# Aste started: 2011-11-12 07:00:04

+# Aste started: 2011-11-16 07:00:04

 # Host id: Boogiebox

 # Configuration: boogie.cfg

 # Task: aste.tasks.boogie.FullBuild

-# [2011-11-12 07:03:24] SpecSharp revision: 31c83dcaabce

-# [2011-11-12 07:03:24] SscBoogie revision: 31c83dcaabce

-# [2011-11-12 07:05:06] Boogie revision: c4b860ad3af4

-[2011-11-12 07:06:26] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

+# [2011-11-16 07:03:29] SpecSharp revision: 441525d3599d

+# [2011-11-16 07:03:29] SscBoogie revision: 441525d3599d

+# [2011-11-16 07:05:22] Boogie revision: 2953138bd568

+[2011-11-16 07:06:54] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

 

     1>corflags : warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


     warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


-[2011-11-12 07:07:59] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

+[2011-11-16 07:07:49] [Error] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

 

     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


@@ -20,12 +20,48 @@
     D:\Temp\aste\Boogie\Source\Core\Parser.cs(111,3): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.


     D:\Temp\aste\Boogie\Source\Core\Parser.cs(116,5): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.


     D:\Temp\aste\Boogie\Source\Core\Parser.cs(119,65): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.ComputeFreeVariables(Microsoft.Boogie.Set)' overrides 'Microsoft.Boogie.Expr.ComputeFreeVariables(Microsoft.Boogie.Set)', thus cannot add Requires.


-    D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(247,7): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(266,7): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1695,11): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1855,11): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\VCGeneration\Check.cs(161,16): warning CS0219: The variable 'expand' is assigned but its value is never used


-    D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(849,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


+    D:\Temp\aste\Boogie\Source\Core\CommandLineOptions.cs(267,7): error CC1002: In method Microsoft.Boogie.CommandLineOptionEngine.Parse(System.String[]): Detected a call to Result with 'System.Int32', should be 'System.Boolean'.


+    D:\Temp\aste\Boogie\Source\Core\CommandLineOptions.cs(267,7): error CC1002: In method Microsoft.Boogie.CommandLineOptionEngine.Parse(System.String[]): Detected a call to Result with 'System.Int32', should be 'System.Boolean'.


+    D:\Temp\aste\Boogie\Source\Core\CommandLineOptions.cs(267,7): error CC1002: In method Microsoft.Boogie.CommandLineOptionEngine.Parse(System.String[]): Detected a call to Result with 'System.Int32', should be 'System.Boolean'.


+    C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v4.0\Microsoft.CodeContracts.targets(240,5): error MSB3073: The command ""C:\Program Files (x86)\Microsoft\Contracts\Bin\ccrewrite" "@Coreccrewrite.rsp"" exited with code 3.


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\AbsInt\bin\Checked\AbsInt.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Z3\bin\Checked\Provers.Z3.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\bin\Checked\Provers.SMTLib.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Z3\bin\Checked\Provers.Z3.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\TPTP\bin\Checked\Provers.TPTP.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Isabelle\bin\Checked\Provers.Isabelle.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\bin\Checked\Provers.SMTLib.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Houdini\bin\Checked\Houdini.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\AbsInt\bin\Checked\AbsInt.dll' could not be found


+    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


     warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     warning CS0162: Unreachable code detected


@@ -35,11 +71,14 @@
     warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.


     warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.


     warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.ComputeFreeVariables(Microsoft.Boogie.Set)' overrides 'Microsoft.Boogie.Expr.ComputeFreeVariables(Microsoft.Boogie.Set)', thus cannot add Requires.


-    warning CS0162: Unreachable code detected


-    warning CS0162: Unreachable code detected


-    warning CS0162: Unreachable code detected


-    warning CS0162: Unreachable code detected


-    warning CS0219: The variable 'expand' is assigned but its value is never used


-    warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


-[2011-11-12 08:05:27] 0 out of 31 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

-# [2011-11-12 08:06:33] Released nightly of Boogie

+    1 error

+    1 error

+    2 error

+    3 error

+    3 error

+    4 error

+    4 error

+    5 error

+    6 error

+    9 error

+    11 failed