Merge

46 files changed, 456 insertions, 3398 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 537dae1d..5b8f8cc5 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -30,6 +30,9 @@ namespace Microsoft.Dafny
       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

         return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, CloneAttributes(dd.Attributes));

+      } else if (d is TupleTypeDecl) {

+        var dd = (TupleTypeDecl)d;

+        return new TupleTypeDecl(dd.Dims, dd.Module);

       } else if (d is IndDatatypeDecl) {

         var dd = (IndDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 56c6edc2..fcf8a2ca 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -107,6 +107,10 @@ namespace Microsoft.Dafny {
           indent += IndentAmount;

         }

         foreach (TopLevelDecl d in m.TopLevelDecls) {

+          bool compileIt = true;

+          if (Attributes.ContainsBool(d.Attributes, "compile", ref compileIt) && !compileIt) {

+            continue;

+          }

           wr.WriteLine();

           if (d is ArbitraryTypeDecl) {

             var at = (ArbitraryTypeDecl)d;

@@ -411,7 +415,12 @@ namespace Microsoft.Dafny {
 

         if (dt is IndDatatypeDecl) {

           Indent(ind); wr.WriteLine("public override string ToString() {");

-          string nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;

+          string nm;

+          if (dt is TupleTypeDecl) {

+            nm = "";

+          } else {

+            nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;

+          }

           Indent(ind + IndentAmount); wr.WriteLine("string s = \"{0}\";", nm);

           if (ctor.Formals.Count != 0) {

             Indent(ind + IndentAmount); wr.WriteLine("s += \"(\";");

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2ab70c4f..5c1148c6 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -739,8 +739,9 @@ Type<out Type/*!*/ ty>
   TypeAndToken<out tok, out ty>

   .

 TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>

-= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-     List<Type/*!*/>/*!*/ gt;

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

+     tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

+     List<Type> gt;

   .)

   ( "bool"                          (. tok = t; .)

   | "nat"                           (. tok = t;  ty = new NatType(); .)

@@ -774,6 +775,20 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
                                          ty = new MapType(gt[0], gt[1]);

                                        }

                                     .)

+  | "("                             (. tok = t; gt = new List<Type>(); .)

+    [ Type<out ty>                  (. gt.Add(ty); .)

+      { "," Type<out ty>            (. gt.Add(ty); .)

+      }

+    ]

+    ")"                             (. if (gt.Count == 1) {

+                                         // just return the type 'ty'

+                                       } else {

+                                         // make sure the nullary tuple type exists

+                                         var dims = gt.Count;

+                                         var tmp = theBuiltIns.TupleType(tok, dims, true);

+                                         ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());

+                                       }

+                                    .)

   | ReferenceType<out tok, out ty>

   )

   .

@@ -1876,25 +1891,51 @@ ConstAtomExpression<out Expression e>
   | "|"                                        (. x = t; .)

       Expression<out e, true>                  (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)

     "|"

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

-      Expression<out e, true>                  (. e = new ParensExpression(x, e); .)

-    ")"

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

-    "("										   (. IToken openParen = t; .)

-	Expression<out e, true>

-	")"										   (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";

-											      IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";

-											      //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });

-												  e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });

-												.)

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

-    "("										   (. IToken openParen = t; .)

-	Expression<out e, true>

-	")"										   (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";

-											      IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";

-											      //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });

-												  e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });

-												.)

+  | ParensExpression<out e>

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

+    "("                                        (. IToken openParen = t; .)

+    Expression<out e, true>

+    ")"                                        (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";

+                                                  IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";

+                                                  //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });

+                                                  e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });

+                                               .)

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

+    "("                                        (. IToken openParen = t; .)

+    Expression<out e, true>

+    ")"                                        (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";

+                                                  IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";

+                                                  //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });

+                                                  e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });

+                                               .)

+  )

+  .

+ParensExpression<out Expression e>

+= (. IToken x;

+     List<Expression> args = null;

+  .)

+  "("                                 (. x = t; e = null; .)

+  ( ")"                               (. // unit

+                                         // make sure the nullary tuple type exists

+                                         var tmp = theBuiltIns.TupleType(x, 0, true);

+                                         e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List<Expression>());

+                                      .)

+  | Expression<out e, true>

+    { ","                             (. if (args == null) {

+                                           args = new List<Expression>();

+                                           args.Add(e);  // add the first argument, which was parsed above

+                                        }

+                                      .)

+      Expression<out e, true>         (. args.Add(e); .)

+    }

+    ")"                               (. if (args == null) {

+                                           e = new ParensExpression(x, e);

+                                         } else {

+                                           // make sure the corresponding tuple type exists

+                                           var tmp = theBuiltIns.TupleType(x, args.Count, true);

+                                           e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);

+                                         }

+                                      .)

   )

   .

 DisplayExpr<out Expression e>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ad98a0c0..55dc973f 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -88,15 +88,17 @@ namespace Microsoft.Dafny {
   {

     public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true);

     Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();

+    Dictionary<int, TupleTypeDecl> tupleTypeDecls = new Dictionary<int, TupleTypeDecl>();

     public readonly ClassDecl ObjectDecl;

     public readonly ClassDecl RealClass;

     //public readonly Function RealToInt;

     //public readonly Function IntToReal;

     public BuiltIns() {

       // create class 'object'

-      ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), null);

+      ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile());

       SystemModule.TopLevelDecls.Add(ObjectDecl);

       // add one-dimensional arrays, since they may arise during type checking

+      // Arrays of other dimensions may be added during parsing as the parser detects the need for these

       UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);

       // add real number functions

       Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List<TypeParameter>(), Token.NoToken,

@@ -108,12 +110,19 @@ namespace Microsoft.Dafny {
         new List<FrameExpression>(), new List<Expression>(), new Specification<Expression>(new List<Expression>(), null),

         null, null, Token.NoToken);

       RealClass = new ClassDecl(Token.NoToken, "Real", SystemModule, new List<TypeParameter>(),

-        new List<MemberDecl>() { RealToInt, IntToReal }, null);

+        new List<MemberDecl>() { RealToInt, IntToReal }, DontCompile());

       RealToInt.EnclosingClass = RealClass;

       IntToReal.EnclosingClass = RealClass;

       RealToInt.IsBuiltin = true;

       IntToReal.IsBuiltin = true;

       SystemModule.TopLevelDecls.Add(RealClass);

+      // Note, in addition to these types, the _System module contains tuple types.  These tuple types are added to SystemModule

+      // by the parser as the parser detects the need for these.

+    }

+

+    private Attributes DontCompile() {

+      var flse = new Attributes.Argument(Token.NoToken, Expression.CreateBoolLiteral(Token.NoToken, false));

+      return new Attributes("compile", new List<Attributes.Argument>() { flse }, null);

     }

 

     public UserDefinedType ArrayType(int dims, Type arg) {

@@ -129,7 +138,7 @@ namespace Microsoft.Dafny {
       typeArgs.Add(arg);

       UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);

       if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {

-        ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);

+        ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile());

         for (int d = 0; d < dims; d++) {

           string name = dims == 1 ? "Length" : "Length" + d;

           string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")";

@@ -152,6 +161,30 @@ namespace Microsoft.Dafny {
         return "array" + dims;

       }

     }

+

+    public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType) {

+      Contract.Requires(tok != null);

+      Contract.Requires(0 <= dims);

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

+

+      TupleTypeDecl tt;

+      if (!tupleTypeDecls.TryGetValue(dims, out tt)) {

+        Contract.Assume(allowCreationOfNewType);  // the parser should ensure that all needed tuple types exist by the time of resolution

+        tt = new TupleTypeDecl(dims, SystemModule);

+        tupleTypeDecls.Add(dims, tt);

+        SystemModule.TopLevelDecls.Add(tt);

+      }

+      return tt;

+    }

+    public static string TupleTypeName(int dims) {

+      Contract.Requires(0 <= dims);

+      return "_tuple#" + dims;

+    }

+    public static bool IsTupleTypeName(string s) {

+      Contract.Requires(s != null);

+      return s.StartsWith("_tuple#");

+    }

+    public const string TupleTypeCtorName = "_#Make";  // the printer wants this name to be uniquely recognizable

   }

 

   public class Attributes {

@@ -714,6 +747,9 @@ namespace Microsoft.Dafny {
     [Pure]

     public override string TypeName(ModuleDefinition context) {

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

+      if (BuiltIns.IsTupleTypeName(Name)) {

+        return "(" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ")";

+      }

       string s = "";

       foreach (var t in Path) {

         if (context != null && t == context.tok) {

@@ -1355,10 +1391,10 @@ namespace Microsoft.Dafny {
 

   public class ArrayClassDecl : ClassDecl {

     public readonly int Dims;

-    public ArrayClassDecl(int dims, ModuleDefinition module)

+    public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)

     : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,

       new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),

-      new List<MemberDecl>(), null)

+      new List<MemberDecl>(), attrs)

     {

       Contract.Requires(1 <= dims);

       Contract.Requires(module != null);

@@ -1367,7 +1403,8 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public abstract class DatatypeDecl : TopLevelDecl {

+  public abstract class DatatypeDecl : TopLevelDecl

+  {

     public readonly List<DatatypeCtor> Ctors;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -1413,6 +1450,52 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class TupleTypeDecl : IndDatatypeDecl

+  {

+    public readonly int Dims;

+    /// <summary>

+    /// Construct a resolved built-in tuple type with "dim" arguments.  "systemModule" is expected to be the _System module.

+    /// </summary>

+    public TupleTypeDecl(int dims, ModuleDefinition systemModule)

+      : this(systemModule, CreateTypeParameters(dims)) {

+      Contract.Requires(0 <= dims);

+      Contract.Requires(systemModule != null);

+    }

+    private TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArgs)

+      : base(Token.NoToken, BuiltIns.TupleTypeName(typeArgs.Count), systemModule, typeArgs, CreateConstructors(typeArgs), null) {

+      Contract.Requires(systemModule != null);

+      Contract.Requires(typeArgs != null);

+      Dims = typeArgs.Count;

+      foreach (var ctor in Ctors) {

+        ctor.EnclosingDatatype = this;  // resolve here

+        DefaultCtor = ctor;

+        TypeParametersUsedInConstructionByDefaultCtor = new bool[typeArgs.Count];

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

+          TypeParametersUsedInConstructionByDefaultCtor[i] = true;

+        }

+      }

+    }

+    private static List<TypeParameter> CreateTypeParameters(int dims) {

+      Contract.Requires(0 <= dims);

+      var ts = new List<TypeParameter>();

+      for (int i = 0; i < dims; i++) {

+        ts.Add(new TypeParameter(Token.NoToken, "T" + i));

+      }

+      return ts;

+    }

+    private static List<DatatypeCtor> CreateConstructors(List<TypeParameter> typeArgs) {

+      Contract.Requires(typeArgs != null);

+      var formals = new List<Formal>();

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

+        var tp = typeArgs[i];

+        var f = new Formal(Token.NoToken, i.ToString(), new UserDefinedType(Token.NoToken, tp.Name, tp), true, false);

+        formals.Add(f);

+      }

+      var ctor = new DatatypeCtor(Token.NoToken, BuiltIns.TupleTypeCtorName, formals, null);

+      return new List<DatatypeCtor>() { ctor };

+    }

+  }

+

   public class CoDatatypeDecl : DatatypeDecl

   {

     public CoDatatypeDecl SscRepr;  // filled in during resolution

@@ -1918,7 +2001,7 @@ namespace Microsoft.Dafny {
       }

       return UniqueName;

     }

-    static char[] specialChars = new char[] { '\'', '_', '?', '\\' };

+    static char[] specialChars = new char[] { '\'', '_', '?', '\\', '#' };

     public static string CompilerizeName(string nm) {

       if ('0' <= nm[0] && nm[0] <= '9') {

         // the identifier is one that consists of just digits

@@ -1942,6 +2025,7 @@ namespace Microsoft.Dafny {
             case '_': name += "__"; break;

             case '?': name += "_q"; break;

             case '\\': name += "_b"; break;

+            case '#': name += "_h"; break;

             default:

               Contract.Assume(false);  // unexpected character

               break;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 969774db..a7f058db 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1115,8 +1115,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 	}

 

 	void TypeAndToken(out IToken/*!*/ tok, out Type/*!*/ ty) {

-		Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-		List<Type/*!*/>/*!*/ gt;

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

+		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

+		List<Type> gt;

 		

 		switch (la.kind) {

 		case 52: {

@@ -1195,6 +1196,30 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			

 			break;

 		}

+		case 11: {

+			Get();

+			tok = t; gt = new List<Type>(); 

+			if (StartOf(10)) {

+				Type(out ty);

+				gt.Add(ty); 

+				while (la.kind == 31) {

+					Get();

+					Type(out ty);

+					gt.Add(ty); 

+				}

+			}

+			Expect(12);

+			if (gt.Count == 1) {

+			 // just return the type 'ty'

+			} else {

+			 // make sure the nullary tuple type exists

+			 var dims = gt.Count;

+			 var tmp = theBuiltIns.TupleType(tok, dims, true);

+			 ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());

+			}

+			

+			break;

+		}

 		case 1: case 5: case 60: {

 			ReferenceType(out tok, out ty);

 			break;

@@ -3352,11 +3377,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			break;

 		}

 		case 11: {

-			Get();

-			x = t; 

-			Expression(out e, true);

-			e = new ParensExpression(x, e); 

-			Expect(12);

+			ParensExpression(out e);

 			break;

 		}

 		case 55: {

@@ -3427,6 +3448,41 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 	}

 

+	void ParensExpression(out Expression e) {

+		IToken x;

+		List<Expression> args = null;

+		

+		Expect(11);

+		x = t; e = null; 

+		if (la.kind == 12) {

+			Get();

+			var tmp = theBuiltIns.TupleType(x, 0, true);

+			e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List<Expression>());

+			

+		} else if (StartOf(16)) {

+			Expression(out e, true);

+			while (la.kind == 31) {

+				Get();

+				if (args == null) {

+				 args = new List<Expression>();

+				 args.Add(e);  // add the first argument, which was parsed above

+				}

+				

+				Expression(out e, true);

+				args.Add(e); 

+			}

+			Expect(12);

+			if (args == null) {

+			 e = new ParensExpression(x, e);

+			} else {

+			 // make sure the corresponding tuple type exists

+			 var tmp = theBuiltIns.TupleType(x, args.Count, true);

+			 e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);

+			}

+			

+		} else SynErr(223);

+	}

+

 	void MapLiteralExpressions(out List<ExpressionPair> elements) {

 		Expression/*!*/ d, r;

 		elements = new List<ExpressionPair/*!*/>(); 

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

 		} else if (la.kind == 125) {

 			Get();

-		} else SynErr(223);

+		} else SynErr(224);

 	}

 

 	void MatchExpression(out Expression e, bool allowSemi) {

@@ -3471,7 +3527,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(10);

 		} else if (StartOf(31)) {

 			if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } 

-		} else SynErr(224);

+		} else SynErr(225);

 		e = new MatchExpr(x, e, cases, usesOptionalBrace); 

 	}

 

@@ -3489,7 +3545,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 122 || la.kind == 123) {

 			Exists();

 			x = t; 

-		} else SynErr(225);

+		} else SynErr(226);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body, allowSemi);

@@ -3537,7 +3593,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			AssumeStmt(out s);

 		} else if (la.kind == 88) {

 			CalcStmt(out s);

-		} else SynErr(226);

+		} else SynErr(227);

 	}

 

 	void LetExpr(out Expression e, bool allowSemi) {

@@ -3577,7 +3633,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-		} else SynErr(227);

+		} else SynErr(228);

 		Expression(out e, false);

 		letRHSs.Add(e); 

 		while (la.kind == 31) {

@@ -3628,7 +3684,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			IdentTypeOptional(out bv);

 			pat = new CasePattern(bv.tok, bv);

 			

-		} else SynErr(228);

+		} else SynErr(229);

 	}

 

 	void CaseExpression(out MatchCaseExpr c, bool allowSemi) {

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

 		} else if (la.kind == 121) {

 			Get();

-		} else SynErr(229);

+		} else SynErr(230);

 	}

 

 	void Exists() {

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

 		} else if (la.kind == 123) {

 			Get();

-		} else SynErr(230);

+		} else SynErr(231);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -3714,8 +3770,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

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

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, 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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,x,x,x, x,x,x,x, x,x,x,x},

 		{x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

@@ -3986,14 +4042,15 @@ public class Errors {
 			case 220: s = "invalid MultiSetExpr"; break;

 			case 221: s = "invalid ConstAtomExpression"; break;

 			case 222: s = "invalid Nat"; break;

-			case 223: s = "invalid QSep"; break;

-			case 224: s = "invalid MatchExpression"; break;

-			case 225: s = "invalid QuantifierGuts"; break;

-			case 226: s = "invalid StmtInExpr"; break;

-			case 227: s = "invalid LetExpr"; break;

-			case 228: s = "invalid CasePattern"; break;

-			case 229: s = "invalid Forall"; break;

-			case 230: s = "invalid Exists"; break;

+			case 223: s = "invalid ParensExpression"; break;

+			case 224: s = "invalid QSep"; break;

+			case 225: s = "invalid MatchExpression"; break;

+			case 226: s = "invalid QuantifierGuts"; break;

+			case 227: s = "invalid StmtInExpr"; break;

+			case 228: s = "invalid LetExpr"; break;

+			case 229: s = "invalid CasePattern"; break;

+			case 230: s = "invalid Forall"; break;

+			case 231: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 0a970498..5be5614d 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1191,9 +1191,16 @@ namespace Microsoft.Dafny {
         wr.Write(((IdentifierExpr)expr).Name);

 

       } else if (expr is DatatypeValue) {

-        DatatypeValue dtv = (DatatypeValue)expr;

-        wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);

-        if (dtv.Arguments.Count != 0) {

+        var dtv = (DatatypeValue)expr;

+        bool printParens;

+        if (dtv.MemberName == BuiltIns.TupleTypeCtorName) {

+          // we're looking at a tuple, whose printed constructor name is essentially the empty string

+          printParens = true;

+        } else {

+          wr.Write("{0}.{1}", dtv.DatatypeName, dtv.MemberName);

+          printParens = dtv.Arguments.Count != 0;

+        }

+        if (printParens) {

           wr.Write("(");

           PrintExpressionList(dtv.Arguments, false);

           wr.Write(")");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 8de010fb..73925aef 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -197,6 +197,7 @@ namespace Microsoft.Dafny
       rewriters.Add(opaqueRewriter);

 

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

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

       foreach (var decl in sortedDecls) {

         if (decl is LiteralModuleDecl) {

           // The declaration is a literal module, so it has members and such that we need

@@ -1019,6 +1020,9 @@ namespace Microsoft.Dafny
       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

         return new ArbitraryTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, null);

+      } else if (d is TupleTypeDecl) {

+        var dd = (TupleTypeDecl)d;

+        return new TupleTypeDecl(dd.Dims, dd.Module);

       } else if (d is IndDatatypeDecl) {

         var dd = (IndDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e2e7155d..3eb06ebc 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -17,6 +17,7 @@ namespace Microsoft.Dafny {
   public class Translator {

     [NotDelayed]

     public Translator() {

+      InsertChecksums = 0 < CommandLineOptions.Clo.VerifySnapshots;

       Bpl.Program boogieProgram = ReadPrelude();

       if (boogieProgram != null) {

         sink = boogieProgram;

@@ -2507,7 +2508,7 @@ namespace Microsoft.Dafny {
     public void InsertUniqueIdForImplementation(Bpl.Declaration decl)

     {

       var impl = decl as Bpl.Implementation;

-      var prefix = UniqueIdPrefix ?? decl.tok.filename;

+      var prefix = UniqueIdPrefix ?? System.Text.RegularExpressions.Regex.Replace(decl.tok.filename, @".v\d+.dfy", ".dfy");

       if (impl != null && !string.IsNullOrEmpty(prefix))

       {

         decl.AddAttribute("id", prefix + ":" + impl.Name + ":0");

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 8f5b5300..01ee269e 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -99,7 +99,7 @@ namespace Microsoft.Dafny
     }

 

 

-    static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames)

+    static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true)

     {

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

 

@@ -110,7 +110,21 @@ namespace Microsoft.Dafny
         {

           Console.WriteLine();

           Console.WriteLine("-------------------- {0} --------------------", f);

-          var ev = ProcessFiles(new List<string> { f });

+          var ev = ProcessFiles(new List<string> { f }, lookForSnapshots);

+          if (exitValue != ev && ev != ExitValue.VERIFIED)

+          {

+            exitValue = ev;

+          }

+        }

+        return exitValue;

+      }

+

+      if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)

+      {

+        var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);

+        foreach (var s in snapshotsByVersion)

+        {

+          var ev = ProcessFiles(new List<string>(s), false);

           if (exitValue != ev && ev != ExitValue.VERIFIED)

           {

             exitValue = ev;

@@ -213,7 +227,7 @@ namespace Microsoft.Dafny
           ExecutionEngine.CollectModSets(program);

           ExecutionEngine.CoalesceBlocks(program);

           ExecutionEngine.Inline(program);

-          return ExecutionEngine.InferAndVerify(program, stats);

+          return ExecutionEngine.InferAndVerify(program, stats, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? "main_program_id" : null);

 

         default:

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

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index 631b0194..cf664364 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -20,7 +20,7 @@
     <OldToolsVersion>3.5</OldToolsVersion>

     <UpgradeBackupLocation />

     <IsWebBootstrapper>false</IsWebBootstrapper>

-    <TargetFrameworkProfile>Client</TargetFrameworkProfile>

+    <TargetFrameworkProfile></TargetFrameworkProfile>

     <PublishUrl>publish\</PublishUrl>

     <Install>true</Install>

     <InstallFrom>Disk</InstallFrom>

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 36b07d60..ba01c04a 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -249,7 +249,8 @@ namespace DafnyLanguage
 

       resolver.ReInitializeVerificationErrors(requestId, boogieProgram.TopLevelDeclarations);

 

-      PipelineOutcome oc = BoogiePipeline(boogieProgram, requestId, er);

+      // TODO(wuestholz): Maybe we should use a fixed program ID to limit the memory overhead due to the program cache in Boogie.

+      PipelineOutcome oc = BoogiePipeline(boogieProgram, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? uniqueIdPrefix : null, requestId, er);

       switch (oc) {

         case PipelineOutcome.Done:

         case PipelineOutcome.VerificationCompleted:

@@ -267,7 +268,7 @@ namespace DafnyLanguage
     /// else.  Hence, any resolution errors and type checking errors are due to errors in

     /// the translation.

     /// </summary>

-    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string requestId, ErrorReporterDelegate er)

+    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string programId, string requestId, ErrorReporterDelegate er)

     {

       Contract.Requires(program != null);

 

@@ -277,7 +278,7 @@ namespace DafnyLanguage
         ExecutionEngine.CollectModSets(program);

         ExecutionEngine.CoalesceBlocks(program);

         ExecutionEngine.Inline(program);  

-        return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), er, requestId);

+        return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), programId, er, requestId);

       }

       return oc;

     }

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 48f5d1b4..5068354a 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -5,6 +5,7 @@ using System.Linq;
 using Microsoft.VisualStudio.Text;

 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Utilities;

+using System.Diagnostics.Contracts;

 

 

 namespace DafnyLanguage

@@ -69,11 +70,12 @@ namespace DafnyLanguage
     }

   }

 

-  internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>

+  internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>, IDisposable

   {

     ITextBuffer _buffer;

     ITextSnapshot _snapshot;

     List<TokenRegion> _regions;

+    bool _disposed;

 

     internal DafnyTokenTagger(ITextBuffer buffer) {

       _buffer = buffer;

@@ -83,6 +85,19 @@ namespace DafnyLanguage
       _buffer.Changed += new EventHandler<TextContentChangedEventArgs>(ReparseFile);

     }

 

+    public void Dispose() {

+      lock (this) {

+        if (!_disposed) {

+          _buffer.Changed -= ReparseFile;

+          _buffer = null;

+          _snapshot = null;

+          _regions = null;

+          _disposed = true;

+        }

+      }

+      GC.SuppressFinalize(this);

+    }

+

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

 

     public IEnumerable<ITagSpan<DafnyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

@@ -148,20 +163,24 @@ namespace DafnyLanguage
     private static List<TokenRegion> Rescan(ITextSnapshot newSnapshot) {

       List<TokenRegion> newRegions = new List<TokenRegion>();

 

-      bool stillScanningLongComment = false;

-      SnapshotPoint commentStart = new SnapshotPoint();  // used only when stillScanningLongComment

-      SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint();  // used only when stillScanningLongComment

+      int longCommentDepth = 0;

+      SnapshotPoint commentStart = new SnapshotPoint();  // used only when longCommentDepth != 0

+      SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint();  // used only when longCommentDepth != 0

       foreach (ITextSnapshotLine line in newSnapshot.Lines) {

         string txt = line.GetText();  // the current line (without linebreak characters)

         int N = txt.Length;  // length of the current line

         int cur = 0;  // offset into the current line

 

-        if (stillScanningLongComment) {

-          if (ScanForEndOfComment(txt, ref cur)) {

+        if (longCommentDepth != 0) {

+          ScanForEndOfComment(txt, ref longCommentDepth, ref cur);

+          if (longCommentDepth == 0) {

+            // we just finished parsing a long comment

             newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKind.Comment));

-            stillScanningLongComment = false;

           } else {

+            // we're still parsing the long comment

+            Contract.Assert(cur == txt.Length);

             commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur);

+            goto OUTER_CONTINUE;

           }

         }

 

@@ -179,9 +198,9 @@ namespace DafnyLanguage
             if ('a' <= ch && ch <= 'z') break;

             if ('A' <= ch && ch <= 'Z') break;

             if ('0' <= ch && ch <= '9') { ty = DafnyTokenKind.Number; break; }

+            if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break;  // parts of identifiers

             if (ch == '"') { ty = DafnyTokenKind.String; break; }

             if (ch == '/') { ty = DafnyTokenKind.Comment; break; }

-            if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break;  // parts of identifiers

           }

 

           // advance to the end of the token

@@ -211,7 +230,7 @@ namespace DafnyLanguage
               }

             }

           } else if (ty == DafnyTokenKind.Comment) {

-            if (end == N) continue;  // this was not the start of a comment

+            if (end == N) continue;  // this was not the start of a comment; it was just a single "/" and we don't care to color it

             char ch = txt[end];

             if (ch == '/') {

               // a short comment

@@ -220,15 +239,18 @@ namespace DafnyLanguage
               // a long comment; find the matching "*/"

               end++;

               commentStart = new SnapshotPoint(newSnapshot, line.Start + cur);

-              if (ScanForEndOfComment(txt, ref end)) {

+              Contract.Assert(longCommentDepth == 0);

+              longCommentDepth = 1;

+              ScanForEndOfComment(txt, ref longCommentDepth, ref end);

+              if (longCommentDepth == 0) {

+                // we finished scanning a long comment, and "end" is set to right after it

                 newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKind.Comment));

               } else {

-                stillScanningLongComment = true;

                 commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end);

               }

               continue;

             } else {

-              // not a comment

+              // not a comment; it was just a single "/" and we don't care to color it

               continue;

             }

           } else {

@@ -322,7 +344,7 @@ namespace DafnyLanguage
                 #endregion

                   break;

                 default:

-                  continue;  // it was an identifier

+                  continue;  // it was an identifier, so we don't color it

               }

             }

           }

@@ -332,26 +354,40 @@ namespace DafnyLanguage
       OUTER_CONTINUE: ;

       }

 

-      if (stillScanningLongComment) {

+      if (longCommentDepth != 0) {

+        // This was a malformed comment, running to the end of the buffer.  Above, we let "commentEndAsWeKnowIt" be the end of the

+        // last line, so we can use it here.

         newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment));

       }

 

       return newRegions;

     }

 

-    private static bool ScanForEndOfComment(string txt, ref int end) {

-      int N = txt.Length;

-      for (; end < N; end++) {

+    /// <summary>

+    /// Scans "txt" beginning with depth "depth", which is assumed to be non-0.  Any occurrences of "/*" or "*/"

+    /// increment or decrement "depth".  If "depth" ever reaches 0, then "end" returns as the number of characters

+    /// consumed from "txt" (including the last "*/").  If "depth" is still non-0 when the entire "txt" has

+    /// been consumed, then "end" returns as the length of "txt".  (Note, "end" may return as the length of "txt"

+    /// if "depth" is still non-0 or if "depth" became 0 from reading the last characters of "txt".)

+    /// </summary>

+    private static void ScanForEndOfComment(string txt, ref int depth, ref int end) {

+      Contract.Requires(depth > 0);

+

+      int Nminus1 = txt.Length - 1;  // no reason ever to look at the last character of the line, unless the second-to-last character is '*' or '/'

+      for (; end < Nminus1; ) {

         char ch = txt[end];

-        if (ch == '*' && end + 1 < N) {

-          ch = txt[end + 1];

-          if (ch == '/') {

-            end += 2;

-            return true;

-          }

+        if (ch == '*' && txt[end + 1] == '/') {

+          end += 2;

+          depth--;

+          if (depth == 0) { return; }

+        } else if (ch == '/' && txt[end + 1] == '*') {

+          end += 2;

+          depth++;

+        } else {

+          end++;

         }

       }

-      return false;  // hit end-of-line without finding end-of-comment

+      end = txt.Length;  // we didn't look at the last character, but we still consumed all the output

     }

   }

 

diff --git a/Test/Makefile b/Test/Makefile
deleted file mode 100644
index 6e02aed0..00000000
--- a/Test/Makefile
+++ /dev/null
@@ -1,17 +0,0 @@
-TESTS_FILE = alltests.txt
-LONG = $(shell awk '{ if (tolower($$2) ~ /^long$$/) print $$1 }' $(TESTS_FILE))
-NORMAL = $(shell awk '{ if (tolower($$2) ~ /^use$$/) print $$1 }' $(TESTS_FILE))
-TESTS = $(NORMAL)
-
-all: dafny
-
-dafny: $(addprefix rundfy-, $(TESTS))
-
-rundfy-%:
-	@cmd /c "runtest.bat $* $(FLAGS)" || :
-
-long:
-	$(MAKE) TESTS="$(NORMAL) $(LONG)" all
-
-show:
-	@echo $(TESTS)
diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer
deleted file mode 100644
index ff491aa5..00000000
--- a/Test/VSComp2010/Answer
+++ /dev/null
@@ -1,20 +0,0 @@
-
--------------------- Problem1-SumMax.dfy --------------------

-

-Dafny program verifier finished with 4 verified, 0 errors

-
--------------------- Problem2-Invert.dfy --------------------

-

-Dafny program verifier finished with 7 verified, 0 errors

-
--------------------- Problem3-FindZero.dfy --------------------

-

-Dafny program verifier finished with 7 verified, 0 errors

-
--------------------- Problem4-Queens.dfy --------------------

-

-Dafny program verifier finished with 9 verified, 0 errors

-
--------------------- Problem5-DoubleEndedQueue.dfy --------------------

-

-Dafny program verifier finished with 21 verified, 0 errors

diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
deleted file mode 100644
index 2cfcdafb..00000000
--- a/Test/VSComp2010/runtest.bat
+++ /dev/null
@@ -1,15 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /verifySeparately %* Problem1-SumMax.dfy Problem2-Invert.dfy Problem3-FindZero.dfy Problem4-Queens.dfy Problem5-DoubleEndedQueue.dfy

-

-rem for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy

-rem             Problem3-FindZero.dfy Problem4-Queens.dfy

-rem             Problem5-DoubleEndedQueue.dfy) do (

-rem   echo.

-rem   echo -------------------- %%f --------------------

-rem   %DAFNY_EXE% /compile:0 %* %%f

-rem )

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
deleted file mode 100644
index 2a4587f4..00000000
--- a/Test/VSI-Benchmarks/Answer
+++ /dev/null
@@ -1,32 +0,0 @@
-

--------------------- b1.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- b2.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-

--------------------- b3.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- b4.dfy --------------------

-

-Dafny program verifier finished with 11 verified, 0 errors

-

--------------------- b5.dfy --------------------

-

-Dafny program verifier finished with 22 verified, 0 errors

-

--------------------- b6.dfy --------------------

-

-Dafny program verifier finished with 21 verified, 0 errors

-

--------------------- b7.dfy --------------------

-

-Dafny program verifier finished with 23 verified, 0 errors

-

--------------------- b8.dfy --------------------

-

-Dafny program verifier finished with 42 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
deleted file mode 100644
index f950cf2a..00000000
--- a/Test/VSI-Benchmarks/runtest.bat
+++ /dev/null
@@ -1,13 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /verifySeparately %* b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy

-

-rem for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

-rem   echo.

-rem   echo -------------------- %%f --------------------

-rem   %DAFNY_EXE% /compile:0 %* %%f

-rem )

diff --git a/Test/alltests.txt b/Test/alltests.txt
deleted file mode 100644
index c586a561..00000000
--- a/Test/alltests.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-dafny0           Use    Dafny functionality tests

-dafny1           Use    Various Dafny examples

-dafny2           Use    More Dafny examples

-dafny3           Use    And more Dafny examples

-dafny4           Use    More, more, more!

-cloudmake        Use    CloudMake formalization and proofs

-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

-VSComp2010       Use    Dafny solutions to VSComp (verified software competition) problems

diff --git a/Test/cloudmake/Answer b/Test/cloudmake/Answer
deleted file mode 100644
index 3758853e..00000000
--- a/Test/cloudmake/Answer
+++ /dev/null
@@ -1,12 +0,0 @@
-

--------------------- CloudMake-ParallelBuilds.dfy --------------------

-

-Dafny program verifier finished with 244 verified, 0 errors

-

--------------------- CloudMake-CachedBuilds.dfy --------------------

-

-Dafny program verifier finished with 104 verified, 0 errors

-

--------------------- CloudMake-ConsistentBuilds.dfy --------------------

-

-Dafny program verifier finished with 59 verified, 0 errors

diff --git a/Test/cloudmake/runtest.bat b/Test/cloudmake/runtest.bat
deleted file mode 100644
index 8fc7ccbb..00000000
--- a/Test/cloudmake/runtest.bat
+++ /dev/null
@@ -1,7 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
deleted file mode 100644
index dc3f1eda..00000000
--- a/Test/dafny0/Answer
+++ /dev/null
@@ -1,2616 +0,0 @@
-

--------------------- Simple.dfy --------------------

-// Simple.dfy

-

-class MyClass<T, U> {

-  var x: int;

-

-  method M(s: bool, lotsaObjects: set<object>)

-      returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)

-    requires s;

-    modifies this, lotsaObjects;

-    ensures t == t;

-    ensures old(null) != this;

-  {

-    x := 12;

-    while x < 100

-      invariant x <= 100;

-    {

-      x := x + 17;

-      if x % 20 == 3 {

-        x := this.x + 1;

-      } else {

-        this.x := x + 0;

-      }

-      t, u, v := M(true, lotsaObjects);

-      var to: MyClass<T,U>;

-      to, u, v := this.M(true, lotsaObjects);

-      to, u, v := to.M(true, lotsaObjects);

-      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

-    }

-  }

-

-  function F(x: int, y: int, h: WildData, k: WildData): WildData

-  {

-    if x < 0 then

-      h

-    else if x == 0 then

-      if if h == k then true else false then

-        h

-      else if y == 0 then

-        k

-      else

-        h

-    else

-      k

-  }

-}

-

-datatype List<T> = Nil | Cons(T, List<T>)

-

-datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>)

-

-class C {

-  var w: WildData;

-  var list: List<bool>;

-}

-

-lemma M(x: int)

-  ensures x < 8;

-{

-}

-

-colemma M'(x': int)

-  ensures true;

-{

-}

-

-Dafny program verifier finished with 0 verified, 0 errors

-

--------------------- TypeTests.dfy --------------------

-TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D)

-TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C)

-TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int)

-TypeTests.dfy(8,13): Error: incorrect type of function argument 1 (expected D, got int)

-TypeTests.dfy(14,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)

-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 0 (expected int, got C)

-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 1 (expected C, got int)

-TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-TypeTests.dfy(56,6): Error: Duplicate local-variable name: z

-TypeTests.dfy(58,6): Error: Duplicate local-variable name: x

-TypeTests.dfy(61,8): Error: Duplicate local-variable name: x

-TypeTests.dfy(64,6): Error: Duplicate local-variable name: y

-TypeTests.dfy(70,11): Error: unresolved identifier: x

-TypeTests.dfy(72,28): Error: unresolved identifier: z

-TypeTests.dfy(73,29): Error: unresolved identifier: w1

-TypeTests.dfy(73,47): Error: unresolved identifier: w0

-TypeTests.dfy(76,28): Error: unresolved identifier: e

-TypeTests.dfy(91,17): Error: member F in type C does not refer to a method

-TypeTests.dfy(92,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(101,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(102,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(103,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(105,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement)

-TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type

-TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(115,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(116,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts

-TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context

-TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context

-TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-33 resolution/type errors detected in TypeTests.dfy

-

--------------------- NatTypes.dfy --------------------

-NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-NatTypes.dfy(34,10): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    NatTypes.dfy(22,3): anon10_LoopHead

-    (0,0): anon10_LoopBody

-    NatTypes.dfy(22,3): anon11_Else

-    (0,0): anon12_Then

-NatTypes.dfy(41,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-NatTypes.dfy(43,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-NatTypes.dfy(60,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-NatTypes.dfy(74,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

-NatTypes.dfy(92,19): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-NatTypes.dfy(107,45): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Else

-    (0,0): anon8_Then

-NatTypes.dfy(130,21): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-

-Dafny program verifier finished with 15 verified, 9 errors

-

--------------------- RealTypes.dfy --------------------

-RealTypes.dfy(8,23): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-RealTypes.dfy(14,12): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    RealTypes.dfy(13,23): anon3_Else

-    (0,0): anon2

-RealTypes.dfy(14,20): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    RealTypes.dfy(13,23): anon3_Else

-    (0,0): anon2

-RealTypes.dfy(22,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 6 verified, 4 errors

-

--------------------- Definedness.dfy --------------------

-Definedness.dfy(11,7): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Definedness.dfy(18,16): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(27,16): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(28,21): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-Definedness.dfy(29,17): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(36,16): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(45,16): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(53,18): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(54,3): Error BP5003: A postcondition might not hold on this return path.

-Definedness.dfy(53,22): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(60,18): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(61,3): Error BP5003: A postcondition might not hold on this return path.

-Definedness.dfy(60,22): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(68,3): Error BP5003: A postcondition might not hold on this return path.

-Definedness.dfy(67,22): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(88,7): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(89,5): Error: possible violation of function precondition

-Definedness.dfy(79,16): Related location

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(89,10): Error: assignment may update an object not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(89,10): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(90,10): Error: possible violation of function precondition

-Definedness.dfy(79,16): Related location

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(95,14): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(95,23): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(96,15): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(101,12): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(108,15): Error: possible division by zero

-Execution trace:

-    Definedness.dfy(108,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    Definedness.dfy(108,5): anon8_Else

-Definedness.dfy(117,23): Error: possible violation of function precondition

-Definedness.dfy(79,16): Related location

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(116,5): anon12_LoopHead

-    (0,0): anon12_LoopBody

-    (0,0): anon13_Then

-Definedness.dfy(123,17): Error: possible violation of function precondition

-Definedness.dfy(79,16): Related location

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(116,5): anon12_LoopHead

-    (0,0): anon12_LoopBody

-    Definedness.dfy(116,5): anon13_Else

-    (0,0): anon14_Then

-    Definedness.dfy(122,5): anon15_LoopHead

-    (0,0): anon15_LoopBody

-    (0,0): anon16_Then

-Definedness.dfy(133,17): Error: possible violation of function precondition

-Definedness.dfy(79,16): Related location

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(132,5): anon6_LoopHead

-    (0,0): anon6_LoopBody

-    (0,0): anon7_Then

-Definedness.dfy(133,22): Error BP5004: This loop invariant might not hold on entry.

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(134,17): Error: possible violation of function precondition

-Definedness.dfy(79,16): Related location

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(132,5): anon6_LoopHead

-    (0,0): anon6_LoopBody

-    (0,0): anon7_Then

-Definedness.dfy(143,15): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(143,5): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    Definedness.dfy(143,5): anon9_Else

-Definedness.dfy(162,15): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(156,5): anon16_LoopHead

-    (0,0): anon16_LoopBody

-    Definedness.dfy(156,5): anon17_Else

-    (0,0): anon18_Then

-    (0,0): anon5

-    (0,0): anon19_Then

-    Definedness.dfy(162,5): anon20_LoopHead

-    (0,0): anon20_LoopBody

-    Definedness.dfy(162,5): anon21_Else

-Definedness.dfy(175,28): Error BP5004: This loop invariant might not hold on entry.

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(181,17): Error: possible violation of function precondition

-Definedness.dfy(79,16): Related location

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(173,5): anon18_LoopHead

-    (0,0): anon18_LoopBody

-    Definedness.dfy(173,5): anon19_Else

-    (0,0): anon20_Then

-    Definedness.dfy(180,5): anon21_LoopHead

-    (0,0): anon21_LoopBody

-    (0,0): anon22_Then

-    (0,0): anon23_Then

-    (0,0): anon11

-Definedness.dfy(196,19): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(194,5): anon6_LoopHead

-    (0,0): anon6_LoopBody

-    (0,0): anon7_Then

-Definedness.dfy(196,23): Error BP5004: This loop invariant might not hold on entry.

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(196,28): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(194,5): anon6_LoopHead

-    (0,0): anon6_LoopBody

-    (0,0): anon7_Then

-Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this return path.

-Definedness.dfy(217,46): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-Definedness.dfy(224,22): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Then

-Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path.

-Definedness.dfy(240,24): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon2

-    (0,0): anon8_Else

-

-Dafny program verifier finished with 21 verified, 37 errors

-

--------------------- FunctionSpecifications.dfy --------------------

-FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold on this return path.

-FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Else

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_Else

-FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold on this return path.

-FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Else

-    (0,0): anon14_Else

-    (0,0): anon15_Then

-FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon3

-FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path.

-FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-FunctionSpecifications.dfy(108,23): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-FunctionSpecifications.dfy(111,23): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-FunctionSpecifications.dfy(126,27): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-FunctionSpecifications.dfy(130,27): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-FunctionSpecifications.dfy(153,15): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-FunctionSpecifications.dfy(165,3): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-FunctionSpecifications.dfy(172,15): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-FunctionSpecifications.dfy(181,3): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path.

-FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Else

-FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-FunctionSpecifications.dfy(160,3): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-FunctionSpecifications.dfy(188,3): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-FunctionSpecifications.dfy(185,20): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 19 verified, 17 errors

-

--------------------- ResolutionErrors.dfy --------------------

-ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

-ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

-ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

-ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree

-ResolutionErrors.dfy(565,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly

-ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements

-ResolutionErrors.dfy(591,11): Error: the body of the enclosing forall statement is not allowed to update heap locations

-ResolutionErrors.dfy(591,14): Error: new allocation not allowed in ghost context

-ResolutionErrors.dfy(601,23): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.

-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.

-ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ResolutionErrors.dfy(700,16): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(702,8): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause

-ResolutionErrors.dfy(724,8): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ResolutionErrors.dfy(732,16): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(734,8): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause

-ResolutionErrors.dfy(762,4): Error: calls to methods with side-effects are not allowed inside a statement expression

-ResolutionErrors.dfy(763,4): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(764,4): Error: wrong number of method result arguments (got 0, expected 1)

-ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(805,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of type object)

-ResolutionErrors.dfy(820,6): Error: RHS (of type int) not assignable to LHS (of type object)

-ResolutionErrors.dfy(821,6): Error: RHS (of type B) not assignable to LHS (of type object)

-ResolutionErrors.dfy(826,6): Error: RHS (of type G) not assignable to LHS (of type object)

-ResolutionErrors.dfy(827,6): Error: RHS (of type Dt) not assignable to LHS (of type object)

-ResolutionErrors.dfy(828,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)

-ResolutionErrors.dfy(890,4): Error: LHS of array assignment must denote an array element (found seq<int>)

-ResolutionErrors.dfy(891,4): Error: LHS of array assignment must denote an array element (found seq<int>)

-ResolutionErrors.dfy(896,10): Error: LHS of assignment must denote a mutable field

-ResolutionErrors.dfy(897,10): Error: LHS of assignment must denote a mutable field

-ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

-ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

-ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

-ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

-ResolutionErrors.dfy(429,2): Error: More than one default constructor

-ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

-ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable

-ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(149,9): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

-ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops

-ResolutionErrors.dfy(235,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)

-ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

-ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

-ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

-ResolutionErrors.dfy(443,9): Error: class Lamb does not have a default constructor

-ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)

-ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

-ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)

-ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)

-ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array<T>)

-ResolutionErrors.dfy(56,14): Error: a field must be selected via an object, not just a class name

-ResolutionErrors.dfy(57,7): Error: unresolved identifier: F

-ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name

-ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance

-ResolutionErrors.dfy(59,7): Error: unresolved identifier: G

-ResolutionErrors.dfy(61,7): Error: unresolved identifier: M

-ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance

-ResolutionErrors.dfy(63,7): Error: unresolved identifier: N

-ResolutionErrors.dfy(66,8): Error: non-function expression is called with parameters

-ResolutionErrors.dfy(67,14): Error: member z does not exist in class Global

-ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

-ResolutionErrors.dfy(91,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(94,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

-ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label

-ResolutionErrors.dfy(263,2): Error: duplicate label

-ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(292,4): Error: a constructor is only allowed to be called when an object is being allocated

-ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)

-ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)

-ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)

-ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts

-ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

-ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

-ResolutionErrors.dfy(365,6): Error: arguments to + must be int or real or a collection type (instead got bool)

-ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)

-ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(374,10): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(384,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ResolutionErrors.dfy(406,6): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint

-ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(473,12): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts

-ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

-ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts

-ResolutionErrors.dfy(546,18): Error: unresolved identifier: w

-ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses

-ResolutionErrors.dfy(913,9): Error: unresolved identifier: s

-135 resolution/type errors detected in ResolutionErrors.dfy

-

--------------------- ParseErrors.dfy --------------------

-ParseErrors.dfy(7,19): error: a chain cannot have more than one != operator

-ParseErrors.dfy(9,37): error: this operator chain cannot continue with a descending operator

-ParseErrors.dfy(10,38): error: this operator chain cannot continue with an ascending operator

-ParseErrors.dfy(15,24): error: this operator chain cannot continue with a descending operator

-ParseErrors.dfy(18,18): error: this operator cannot be part of a chain

-ParseErrors.dfy(19,19): error: this operator cannot be part of a chain

-ParseErrors.dfy(20,18): error: this operator cannot be part of a chain

-ParseErrors.dfy(21,18): error: chaining not allowed from the previous operator

-ParseErrors.dfy(49,8): error: the main operator of a calculation must be transitive

-ParseErrors.dfy(65,2): error: this operator cannot continue this calculation

-ParseErrors.dfy(66,2): error: this operator cannot continue this calculation

-ParseErrors.dfy(71,2): error: this operator cannot continue this calculation

-ParseErrors.dfy(72,2): error: this operator cannot continue this calculation

-ParseErrors.dfy(78,2): error: this operator cannot continue this calculation

-14 parse errors detected in ParseErrors.dfy

-

--------------------- Array.dfy --------------------

-Array.dfy(13,8): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Then

-Array.dfy(20,16): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-Array.dfy(27,6): Error: index out of range

-Execution trace:

-    (0,0): anon0

-Array.dfy(51,20): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Array.dfy(59,8): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Then

-Array.dfy(66,8): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Then

-Array.dfy(110,21): Error: upper bound below lower bound or above length of array

-Execution trace:

-    (0,0): anon0

-    (0,0): anon14_Else

-    (0,0): anon18_Then

-    (0,0): anon19_Then

-    (0,0): anon20_Then

-    (0,0): anon11

-Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_Then

-    (0,0): anon12_Then

-Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_Then

-    (0,0): anon12_Else

-Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_Then

-    (0,0): anon12_Else

-Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_Then

-    (0,0): anon12_Else

-Array.dfy(150,6): Error: insufficient reads clause to read array element

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon8_Then

-    (0,0): anon9_Then

-Array.dfy(158,6): Error: insufficient reads clause to read array element

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon8_Then

-    (0,0): anon9_Then

-Array.dfy(174,6): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-Array.dfy(181,6): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-Array.dfy(206,1): Error BP5003: A postcondition might not hold on this return path.

-Array.dfy(205,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Array.dfy(230,1): Error BP5003: A postcondition might not hold on this return path.

-Array.dfy(229,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Array.dfy(236,1): Error BP5003: A postcondition might not hold on this return path.

-Array.dfy(235,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Array.dfy(251,10): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Then

-Array.dfy(252,5): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Then

-

-Dafny program verifier finished with 41 verified, 20 errors

-

--------------------- MultiDimArray.dfy --------------------

-MultiDimArray.dfy(56,21): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

-    (0,0): anon12_Then

-MultiDimArray.dfy(83,25): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon6_Then

-

-Dafny program verifier finished with 8 verified, 2 errors

-

--------------------- NonGhostQuantifiers.dfy --------------------

-NonGhostQuantifiers.dfy(149,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(153,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(158,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(163,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(186,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'

-NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'

-NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'

-NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

-NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

-NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-20 resolution/type errors detected in NonGhostQuantifiers.dfy

-

--------------------- AdvancedLHS.dfy --------------------

-AdvancedLHS.dfy(34,23): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    (0,0): anon15_Else

-

-Dafny program verifier finished with 7 verified, 1 error

-

--------------------- ModulesCycle.dfy --------------------

-ModulesCycle.dfy(5,9): Error: module T does not exist

-ModulesCycle.dfy(8,7): Error: module definition contains a cycle (note: parent modules implicitly depend on submodules): A -> D -> C -> B

-2 resolution/type errors detected in ModulesCycle.dfy

-

--------------------- Modules0.dfy --------------------

-Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(13,7): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(14,8): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(56,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)

-Modules0.dfy(57,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

-Modules0.dfy(68,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

-Modules0.dfy(75,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)

-Modules0.dfy(75,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?)

-Modules0.dfy(78,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?)

-Modules0.dfy(83,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

-Modules0.dfy(92,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

-Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

-Modules0.dfy(224,8): Error: new can be applied only to reference types (got X)

-Modules0.dfy(233,13): Error: Undeclared type X in module B

-Modules0.dfy(243,13): Error: unresolved identifier: X

-Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)

-Modules0.dfy(283,12): Error: new can be applied only to reference types (got D)

-Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(287,6): Error: expected method call, found expression

-Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(288,6): Error: expected method call, found expression

-Modules0.dfy(310,24): Error: module Q_Imp does not exist

-Modules0.dfy(100,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

-28 resolution/type errors detected in Modules0.dfy

-

--------------------- Modules1.dfy --------------------

-Modules1.dfy(79,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-Modules1.dfy(92,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-Modules1.dfy(94,18): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0

-Execution trace:

-    (0,0): anon0

-Modules1.dfy(62,3): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 26 verified, 5 errors

-

--------------------- Modules2.dfy --------------------

-Modules2.dfy(46,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)

-Modules2.dfy(46,10): Error: new can be applied only to reference types (got C)

-Modules2.dfy(49,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E')

-Modules2.dfy(50,14): Error: The name D ambiguously refers to a type in one of the modules A, B

-Modules2.dfy(52,11): Error: The name f ambiguously refers to a static member in one of the modules A, B

-5 resolution/type errors detected in Modules2.dfy

-

--------------------- BadFunction.dfy --------------------

-BadFunction.dfy(9,3): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-

-Dafny program verifier finished with 2 verified, 1 error

-

--------------------- Comprehensions.dfy --------------------

-Comprehensions.dfy(12,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Then

-    (0,0): anon10_Then

-    (0,0): anon4

-    (0,0): anon11_Then

-    (0,0): anon12_Then

-    (0,0): anon8

-

-Dafny program verifier finished with 6 verified, 1 error

-

--------------------- Basics.dfy --------------------

-Basics.dfy(45,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Basics.dfy(69,42): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon13_Then

-    (0,0): anon14_Then

-    (0,0): anon15_Then

-    Basics.dfy(69,72): anon16_Else

-    Basics.dfy(69,82): anon17_Else

-    Basics.dfy(69,95): anon18_Else

-    (0,0): anon12

-Basics.dfy(113,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon10_Then

-Basics.dfy(132,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value

-Execution trace:

-    (0,0): anon0

-    (0,0): anon10_Then

-    (0,0): anon3

-    (0,0): anon11_Then

-    (0,0): anon6

-    (0,0): anon12_Then

-    (0,0): anon9

-Basics.dfy(146,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value

-Execution trace:

-    (0,0): anon0

-Basics.dfy(158,19): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

-Basics.dfy(160,10): Error: assignment may update an object not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3

-Basics.dfy(160,10): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3

-Basics.dfy(165,12): Error: left-hand sides 0 and 1 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

-    (0,0): anon3

-    (0,0): anon12_Then

-Basics.dfy(176,15): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

-    (0,0): anon3

-    (0,0): anon12_Else

-    (0,0): anon6

-    (0,0): anon13_Then

-    (0,0): anon8

-    (0,0): anon14_Then

-Basics.dfy(238,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value

-Execution trace:

-    (0,0): anon0

-Basics.dfy(429,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon3

-Basics.dfy(440,19): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-Basics.dfy(442,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon3

-

-Dafny program verifier finished with 61 verified, 14 errors

-

--------------------- ControlStructures.dfy --------------------

-ControlStructures.dfy(8,3): Error: missing case in case statement: Purple

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Else

-    (0,0): anon8_Then

-ControlStructures.dfy(8,3): Error: missing case in case statement: Blue

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Else

-    (0,0): anon8_Else

-    (0,0): anon9_Then

-ControlStructures.dfy(17,3): Error: missing case in case statement: Purple

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Else

-    (0,0): anon8_Then

-ControlStructures.dfy(46,5): Error: missing case in case statement: Red

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-ControlStructures.dfy(54,3): Error: missing case in case statement: Red

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Else

-    (0,0): anon9_Else

-    (0,0): anon10_Else

-    (0,0): anon11_Else

-    (0,0): anon12_Then

-ControlStructures.dfy(75,3): Error: alternative cases fail to cover all possibilties

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-ControlStructures.dfy(218,18): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    ControlStructures.dfy(197,3): anon59_LoopHead

-    (0,0): anon59_LoopBody

-    ControlStructures.dfy(197,3): anon60_Else

-    ControlStructures.dfy(197,3): anon61_Else

-    ControlStructures.dfy(201,5): anon62_LoopHead

-    (0,0): anon62_LoopBody

-    ControlStructures.dfy(201,5): anon63_Else

-    ControlStructures.dfy(201,5): anon64_Else

-    (0,0): anon68_Then

-    ControlStructures.dfy(213,9): anon69_LoopHead

-    (0,0): anon69_LoopBody

-    ControlStructures.dfy(213,9): anon70_Else

-    (0,0): anon71_Then

-ControlStructures.dfy(235,21): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    ControlStructures.dfy(197,3): anon59_LoopHead

-    (0,0): anon59_LoopBody

-    ControlStructures.dfy(197,3): anon60_Else

-    ControlStructures.dfy(197,3): anon61_Else

-    ControlStructures.dfy(201,5): anon62_LoopHead

-    (0,0): anon62_LoopBody

-    ControlStructures.dfy(201,5): anon63_Else

-    ControlStructures.dfy(201,5): anon64_Else

-    (0,0): anon68_Then

-    ControlStructures.dfy(213,9): anon69_LoopHead

-    (0,0): anon69_LoopBody

-    ControlStructures.dfy(213,9): anon70_Else

-    ControlStructures.dfy(213,9): anon71_Else

-    (0,0): anon72_Then

-    (0,0): after_4

-    ControlStructures.dfy(224,7): anon74_LoopHead

-    (0,0): anon74_LoopBody

-    ControlStructures.dfy(224,7): anon75_Else

-    ControlStructures.dfy(224,7): anon76_Else

-    (0,0): anon78_Then

-    (0,0): anon38

-    (0,0): anon83_Then

-    (0,0): anon52

-ControlStructures.dfy(238,30): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    ControlStructures.dfy(197,3): anon59_LoopHead

-    (0,0): anon59_LoopBody

-    ControlStructures.dfy(197,3): anon60_Else

-    ControlStructures.dfy(197,3): anon61_Else

-    ControlStructures.dfy(201,5): anon62_LoopHead

-    (0,0): anon62_LoopBody

-    ControlStructures.dfy(201,5): anon63_Else

-    ControlStructures.dfy(201,5): anon64_Else

-    (0,0): anon65_Then

-    (0,0): anon84_Then

-    (0,0): anon85_Then

-    (0,0): anon56

-ControlStructures.dfy(241,17): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    ControlStructures.dfy(197,3): anon59_LoopHead

-    (0,0): anon59_LoopBody

-    ControlStructures.dfy(197,3): anon60_Else

-    ControlStructures.dfy(197,3): anon61_Else

-    ControlStructures.dfy(201,5): anon62_LoopHead

-    (0,0): anon62_LoopBody

-    ControlStructures.dfy(201,5): anon63_Else

-    ControlStructures.dfy(201,5): anon64_Else

-    (0,0): anon68_Then

-    ControlStructures.dfy(213,9): anon69_LoopHead

-    (0,0): anon69_LoopBody

-    ControlStructures.dfy(213,9): anon70_Else

-    ControlStructures.dfy(213,9): anon71_Else

-    (0,0): anon72_Then

-    (0,0): after_4

-    ControlStructures.dfy(224,7): anon74_LoopHead

-    (0,0): anon74_LoopBody

-    ControlStructures.dfy(224,7): anon75_Else

-    ControlStructures.dfy(224,7): anon76_Else

-    (0,0): anon79_Then

-    (0,0): anon82_Then

-    (0,0): anon86_Then

-    (0,0): anon58

-

-Dafny program verifier finished with 22 verified, 10 errors

-

--------------------- Termination.dfy --------------------

-Termination.dfy(359,47): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon8_Then

-    (0,0): anon9_Else

-Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop

-Execution trace:

-    (0,0): anon0

-    Termination.dfy(108,3): anon6_LoopHead

-    (0,0): anon6_LoopBody

-    Termination.dfy(108,3): anon7_Else

-    Termination.dfy(108,3): anon8_Else

-Termination.dfy(116,3): Error: cannot prove termination; try supplying a decreases clause for the loop

-Execution trace:

-    (0,0): anon0

-    Termination.dfy(116,3): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    Termination.dfy(116,3): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon5

-    Termination.dfy(116,3): anon11_Else

-Termination.dfy(125,3): Error: decreases expression might not decrease

-Execution trace:

-    (0,0): anon0

-    Termination.dfy(125,3): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    Termination.dfy(125,3): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon5

-    Termination.dfy(125,3): anon11_Else

-Termination.dfy(126,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

-Execution trace:

-    (0,0): anon0

-    Termination.dfy(125,3): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    Termination.dfy(125,3): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon5

-    Termination.dfy(125,3): anon11_Else

-Termination.dfy(254,35): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Else

-    (0,0): anon8_Then

-Termination.dfy(294,3): Error: decreases expression might not decrease

-Execution trace:

-    Termination.dfy(294,3): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    Termination.dfy(294,3): anon10_Else

-    Termination.dfy(294,3): anon11_Else

-    (0,0): anon12_Else

-

-Dafny program verifier finished with 59 verified, 7 errors

-

--------------------- DTypes.dfy --------------------

-DTypes.dfy(18,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-DTypes.dfy(56,18): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-DTypes.dfy(120,13): Error: assertion violation

-DTypes.dfy(92,30): Related location

-Execution trace:

-    (0,0): anon0

-DTypes.dfy(126,13): Error: assertion violation

-DTypes.dfy(92,20): Related location

-Execution trace:

-    (0,0): anon0

-DTypes.dfy(136,12): Error: assertion violation

-DTypes.dfy(131,6): Related location

-DTypes.dfy(92,20): Related location

-Execution trace:

-    (0,0): anon0

-DTypes.dfy(157,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon6_Then

-    (0,0): anon4

-

-Dafny program verifier finished with 27 verified, 6 errors

-

--------------------- ParallelResolveErrors.dfy --------------------

-ParallelResolveErrors.dfy(10,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable

-ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement

-ParallelResolveErrors.dfy(44,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements

-ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(65,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-ParallelResolveErrors.dfy(66,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods

-ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement

-ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(85,20): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations

-ParallelResolveErrors.dfy(115,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-ParallelResolveErrors.dfy(120,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-21 resolution/type errors detected in ParallelResolveErrors.dfy

-

--------------------- Parallel.dfy --------------------

-Parallel.dfy(34,5): Error BP5002: A precondition for this call might not hold.

-Parallel.dfy(60,14): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon29_Else

-    (0,0): anon32_Else

-    (0,0): anon33_Then

-    (0,0): anon34_Then

-    (0,0): anon35_Then

-    (0,0): anon14

-Parallel.dfy(38,5): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    (0,0): anon29_Else

-    (0,0): anon32_Else

-    (0,0): anon33_Else

-    (0,0): anon36_Then

-    (0,0): anon37_Then

-    (0,0): anon38_Then

-    (0,0): anon20

-Parallel.dfy(42,18): Error: possible violation of postcondition of forall statement

-Execution trace:

-    (0,0): anon0

-    (0,0): anon29_Else

-    (0,0): anon32_Else

-    (0,0): anon33_Else

-    (0,0): anon36_Else

-    (0,0): anon39_Then

-    (0,0): anon40_Then

-    (0,0): anon26

-Parallel.dfy(47,19): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon29_Else

-    (0,0): anon32_Else

-    (0,0): anon33_Else

-    (0,0): anon36_Else

-    (0,0): anon39_Then

-    (0,0): anon40_Then

-Parallel.dfy(93,19): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon10_Else

-    (0,0): anon11_Then

-Parallel.dfy(99,20): Error: possible violation of postcondition of forall statement

-Execution trace:

-    (0,0): anon0

-    (0,0): anon10_Else

-    (0,0): anon11_Then

-    (0,0): anon12_Then

-Parallel.dfy(122,12): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-    (0,0): anon7_Then

-    (0,0): anon3

-Parallel.dfy(185,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon19_Then

-    (0,0): anon20_Then

-    (0,0): anon5

-Parallel.dfy(296,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-

-Dafny program verifier finished with 43 verified, 9 errors

-

--------------------- TypeParameters.dfy --------------------

-TypeParameters.dfy(47,22): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-TypeParameters.dfy(69,27): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-    (0,0): anon2

-TypeParameters.dfy(156,12): Error: assertion violation

-TypeParameters.dfy(156,28): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon20_Then

-    TypeParameters.dfy(156,32): anon21_Else

-    (0,0): anon5

-TypeParameters.dfy(158,12): Error: assertion violation

-TypeParameters.dfy(158,33): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon23_Then

-    TypeParameters.dfy(158,37): anon24_Else

-    (0,0): anon11

-TypeParameters.dfy(160,12): Error: assertion violation

-TypeParameters.dfy(160,20): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon25_Then

-TypeParameters.dfy(162,12): Error: assertion violation

-TypeParameters.dfy(147,5): Related location

-TypeParameters.dfy(162,21): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon26_Then

-TypeParameters.dfy(164,12): Error: assertion violation

-TypeParameters.dfy(149,8): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon27_Then

-TypeParameters.dfy(178,15): Error BP5005: This loop invariant might not be maintained by the loop.

-TypeParameters.dfy(178,38): Related location

-Execution trace:

-    (0,0): anon0

-    TypeParameters.dfy(171,3): anon16_LoopHead

-    (0,0): anon16_LoopBody

-    TypeParameters.dfy(171,3): anon17_Else

-    (0,0): anon19_Then

-    TypeParameters.dfy(177,3): anon20_LoopHead

-    (0,0): anon20_LoopBody

-    TypeParameters.dfy(177,3): anon21_Else

-    TypeParameters.dfy(177,3): anon23_Else

-

-Dafny program verifier finished with 58 verified, 8 errors

-

--------------------- Datatypes.dfy --------------------

-Datatypes.dfy(297,10): Error BP5003: A postcondition might not hold on this return path.

-Datatypes.dfy(295,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon13_Then

-    (0,0): anon14_Else

-    (0,0): anon15_Then

-    (0,0): anon6

-Datatypes.dfy(298,12): Error: missing case in case statement: Appendix

-Execution trace:

-    (0,0): anon0

-    (0,0): anon13_Then

-    (0,0): anon14_Else

-    (0,0): anon15_Else

-    (0,0): anon16_Then

-Datatypes.dfy(349,5): Error: missing case in case statement: Cons

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

-Datatypes.dfy(349,5): Error: missing case in case statement: Nil

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Else

-    (0,0): anon8_Then

-Datatypes.dfy(356,8): Error: missing case in case statement: Cons

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_Then

-Datatypes.dfy(356,8): Error: missing case in case statement: Nil

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_Else

-    (0,0): anon12_Then

-Datatypes.dfy(82,20): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon20_Else

-    (0,0): anon21_Then

-    (0,0): anon4

-    (0,0): anon22_Else

-    (0,0): anon23_Then

-    (0,0): anon24_Else

-    (0,0): anon25_Then

-Datatypes.dfy(170,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-Datatypes.dfy(172,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-    (0,0): anon5_Then

-Datatypes.dfy(201,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'

-Execution trace:

-    (0,0): anon0

-Datatypes.dfy(204,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-Datatypes.dfy(225,17): Error: destructor 'c' can only be applied to datatype values constructed by 'T''

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-

-Dafny program verifier finished with 44 verified, 12 errors

-

--------------------- StatementExpressions.dfy --------------------

-StatementExpressions.dfy(55,11): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-    (0,0): anon8_Then

-StatementExpressions.dfy(59,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-    StatementExpressions.dfy(53,7): anon8_Else

-StatementExpressions.dfy(77,6): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-StatementExpressions.dfy(98,11): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-

-Dafny program verifier finished with 17 verified, 5 errors

-

--------------------- Coinductive.dfy --------------------

-Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed

-Coinductive.dfy(16,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed

-Coinductive.dfy(38,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed

-Coinductive.dfy(64,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed

-Coinductive.dfy(93,8): Error: a copredicate can be called recursively only in positive positions

-Coinductive.dfy(94,8): Error: a copredicate can be called recursively only in positive positions

-Coinductive.dfy(95,8): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(95,21): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(101,5): Error: a copredicate can be called recursively only in positive positions

-Coinductive.dfy(104,27): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(105,28): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(106,17): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(148,5): Error: a recursive call from a copredicate can go only to other copredicates

-16 resolution/type errors detected in Coinductive.dfy

-

--------------------- Corecursion.dfy --------------------

-Corecursion.dfy(17,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Corecursion.dfy(23,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Corecursion.dfy(58,5): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

-Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

-Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Corecursion.dfy(161,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-

-Dafny program verifier finished with 20 verified, 8 errors

-

--------------------- CoResolution.dfy --------------------

-CoResolution.dfy(17,9): Error: member Undeclared# does not exist in class _default

-CoResolution.dfy(18,4): Error: unresolved identifier: Undeclared#

-CoResolution.dfy(21,7): Error: unresolved identifier: _k

-CoResolution.dfy(39,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)

-CoResolution.dfy(50,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any reads clause

-CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause

-CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(95,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-CoResolution.dfy(115,17): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(121,17): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-CoResolution.dfy(135,17): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-21 resolution/type errors detected in CoResolution.dfy

-

--------------------- CoPrefix.dfy --------------------

-CoPrefix.dfy(164,3): Error BP5003: A postcondition might not hold on this return path.

-CoPrefix.dfy(163,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-CoPrefix.dfy(169,3): Error BP5003: A postcondition might not hold on this return path.

-CoPrefix.dfy(168,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-CoPrefix.dfy(176,5): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-CoPrefix.dfy(63,7): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Else

-    (0,0): anon9_Then

-CoPrefix.dfy(76,7): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Else

-    (0,0): anon9_Then

-CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path.

-CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold.

-CoPrefix.dfy(101,17): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-CoPrefix.dfy(138,25): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Then

-    (0,0): anon10_Then

-CoPrefix.dfy(142,25): Error: assertion violation

-CoPrefix.dfy(117,23): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Then

-    (0,0): anon12_Then

-CoPrefix.dfy(151,1): Error BP5003: A postcondition might not hold on this return path.

-CoPrefix.dfy(150,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-

-Dafny program verifier finished with 41 verified, 9 errors

-

--------------------- CoinductiveProofs.dfy --------------------

-CoinductiveProofs.dfy(29,12): Error: assertion violation

-CoinductiveProofs.dfy(13,17): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon6_Then

-CoinductiveProofs.dfy(59,1): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(58,11): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(54,3): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-CoinductiveProofs.dfy(74,12): Error: assertion violation

-CoinductiveProofs.dfy(54,3): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon6_Then

-CoinductiveProofs.dfy(91,1): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(90,11): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(80,3): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-CoinductiveProofs.dfy(100,12): Error: assertion violation

-CoinductiveProofs.dfy(80,3): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon6_Then

-CoinductiveProofs.dfy(111,1): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(110,11): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(106,3): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-CoinductiveProofs.dfy(150,1): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(149,22): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(4,24): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-CoinductiveProofs.dfy(156,1): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(155,22): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(4,24): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-

-Dafny program verifier finished with 35 verified, 8 errors

-

--------------------- TypeAntecedents.dfy --------------------

-TypeAntecedents.dfy(35,13): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-TypeAntecedents.dfy(58,1): Error BP5003: A postcondition might not hold on this return path.

-TypeAntecedents.dfy(57,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon25_Then

-    (0,0): anon6

-    (0,0): anon28_Then

-    (0,0): anon8

-    (0,0): anon29_Else

-    (0,0): anon31_Else

-    (0,0): anon33_Then

-    (0,0): anon20

-    (0,0): anon34_Then

-    (0,0): anon35_Then

-    (0,0): anon24

-TypeAntecedents.dfy(66,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon25_Else

-    (0,0): anon26_Then

-    (0,0): anon27_Else

-

-Dafny program verifier finished with 12 verified, 3 errors

-

--------------------- NoTypeArgs.dfy --------------------

-

-Dafny program verifier finished with 15 verified, 0 errors

-

--------------------- EqualityTypes.dfy --------------------

-EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype

-EqualityTypes.dfy(35,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality

-EqualityTypes.dfy(40,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes a different number of type parameters

-EqualityTypes.dfy(41,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters

-EqualityTypes.dfy(45,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality

-EqualityTypes.dfy(46,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality

-EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)

-EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)

-EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)

-EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)

-EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)

-11 resolution/type errors detected in EqualityTypes.dfy

-

--------------------- SplitExpr.dfy --------------------

-SplitExpr.dfy(92,15): Error: loop invariant violation

-SplitExpr.dfy(86,44): Related location

-Execution trace:

-    SplitExpr.dfy(91,3): anon7_LoopHead

-

-Dafny program verifier finished with 10 verified, 1 error

-

--------------------- LoopModifies.dfy --------------------

-LoopModifies.dfy(8,5): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-LoopModifies.dfy(19,8): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    LoopModifies.dfy(16,4): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    LoopModifies.dfy(16,4): anon9_Else

-    LoopModifies.dfy(16,4): anon11_Else

-LoopModifies.dfy(48,8): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    LoopModifies.dfy(44,4): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    LoopModifies.dfy(44,4): anon9_Else

-    LoopModifies.dfy(44,4): anon11_Else

-LoopModifies.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    LoopModifies.dfy(59,4): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    LoopModifies.dfy(59,4): anon10_Else

-    LoopModifies.dfy(59,4): anon12_Else

-LoopModifies.dfy(76,4): Error: loop modifies clause may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-LoopModifies.dfy(100,8): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    LoopModifies.dfy(92,4): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    LoopModifies.dfy(92,4): anon9_Else

-    LoopModifies.dfy(92,4): anon11_Else

-LoopModifies.dfy(148,11): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    LoopModifies.dfy(136,4): anon17_LoopHead

-    (0,0): anon17_LoopBody

-    LoopModifies.dfy(136,4): anon18_Else

-    LoopModifies.dfy(136,4): anon20_Else

-    LoopModifies.dfy(141,7): anon21_LoopHead

-    (0,0): anon21_LoopBody

-    LoopModifies.dfy(141,7): anon22_Else

-    LoopModifies.dfy(141,7): anon24_Else

-LoopModifies.dfy(199,10): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    LoopModifies.dfy(195,4): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    LoopModifies.dfy(195,4): anon9_Else

-    LoopModifies.dfy(195,4): anon11_Else

-LoopModifies.dfy(287,13): Error: assignment may update an array element not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    LoopModifies.dfy(275,4): anon16_LoopHead

-    (0,0): anon16_LoopBody

-    LoopModifies.dfy(275,4): anon17_Else

-    LoopModifies.dfy(275,4): anon19_Else

-    LoopModifies.dfy(283,7): anon20_LoopHead

-    (0,0): anon20_LoopBody

-    LoopModifies.dfy(283,7): anon21_Else

-    LoopModifies.dfy(283,7): anon23_Else

-

-Dafny program verifier finished with 23 verified, 9 errors

-

--------------------- Refinement.dfy --------------------

-Refinement.dfy(15,5): Error BP5003: A postcondition might not hold on this return path.

-Refinement.dfy(14,17): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Refinement.dfy[B](15,5): Error BP5003: A postcondition might not hold on this return path.

-Refinement.dfy(33,20): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Refinement.dfy(64,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Refinement.dfy(74,17): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Refinement.dfy(93,12): Error BP5003: A postcondition might not hold on this return path.

-Refinement.dfy(72,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Refinement.dfy(96,3): Error BP5003: A postcondition might not hold on this return path.

-Refinement.dfy(77,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path.

-Refinement.dfy[IncorrectConcrete](115,15): Related location: This is the postcondition that might not hold.

-Refinement.dfy(180,9): Related location

-Execution trace:

-    (0,0): anon0

-Refinement.dfy(187,5): Error BP5003: A postcondition might not hold on this return path.

-Refinement.dfy[IncorrectConcrete](123,15): Related location: This is the postcondition that might not hold.

-Refinement.dfy(180,9): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon3

-Refinement.dfy(193,7): Error: assertion violation

-Refinement.dfy[IncorrectConcrete](131,24): Related location

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 48 verified, 9 errors

-

--------------------- RefinementErrors.dfy --------------------

-RefinementErrors.dfy(30,17): Error: a refining method is not allowed to add preconditions

-RefinementErrors.dfy(31,15): Error: a refining method is not allowed to extend the modifies clause

-RefinementErrors.dfy(34,14): Error: a predicate declaration (abc) can only refine a predicate

-RefinementErrors.dfy(35,8): Error: a field re-declaration (xyz) must be to ghostify the field

-RefinementErrors.dfy(37,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F

-RefinementErrors.dfy(38,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')

-RefinementErrors.dfy(38,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')

-RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')

-RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')

-RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines

-RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G

-11 resolution/type errors detected in RefinementErrors.dfy

-

--------------------- ReturnErrors.dfy --------------------

-ReturnErrors.dfy(32,10): Error: cannot have method call in return statement.

-ReturnErrors.dfy(38,10): Error: cannot have effectful parameter in multi-return statement.

-ReturnErrors.dfy(43,10): Error: can only have initialization methods which modify at most 'this'.

-3 resolution/type errors detected in ReturnErrors.dfy

-

--------------------- ReturnTests.dfy --------------------

-

-Dafny program verifier finished with 20 verified, 0 errors

-

--------------------- ChainingDisjointTests.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-

--------------------- CallStmtTests.dfy --------------------

-CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable

-CallStmtTests.dfy(17,8): Error: actual out-parameter 0 is required to be a ghost variable

-2 resolution/type errors detected in CallStmtTests.dfy

-

--------------------- MultiSets.dfy --------------------

-MultiSets.dfy(159,3): Error BP5003: A postcondition might not hold on this return path.

-MultiSets.dfy(158,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-MultiSets.dfy(165,3): Error BP5003: A postcondition might not hold on this return path.

-MultiSets.dfy(164,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-MultiSets.dfy(178,11): Error: new number of occurrences might be negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon3

-MultiSets.dfy(269,24): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

-    (0,0): anon3

-    (0,0): anon12_Then

-    (0,0): anon14_Else

-

-Dafny program verifier finished with 54 verified, 4 errors

-

--------------------- PredExpr.dfy --------------------

-PredExpr.dfy(7,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Else

-PredExpr.dfy(52,17): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-PredExpr.dfy(77,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Else

-    (0,0): anon3

-    PredExpr.dfy(76,20): anon10_Else

-    (0,0): anon6

-

-Dafny program verifier finished with 11 verified, 4 errors

-

--------------------- Predicates.dfy --------------------

-Predicates.dfy[B](21,5): Error BP5003: A postcondition might not hold on this return path.

-Predicates.dfy[B](20,15): Related location: This is the postcondition that might not hold.

-Predicates.dfy(31,9): Related location

-Execution trace:

-    (0,0): anon0

-Predicates.dfy(88,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Predicates.dfy(92,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Predicates.dfy[Tricky_Full](126,5): Error BP5003: A postcondition might not hold on this return path.

-Predicates.dfy[Tricky_Full](125,15): Related location: This is the postcondition that might not hold.

-Predicates.dfy(136,7): Related location

-Predicates.dfy[Tricky_Full](116,9): Related location

-Execution trace:

-    (0,0): anon0

-Predicates.dfy(164,5): Error BP5003: A postcondition might not hold on this return path.

-Predicates.dfy(163,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Predicates.dfy[Q1](154,5): Error BP5003: A postcondition might not hold on this return path.

-Predicates.dfy[Q1](153,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 52 verified, 6 errors

-

--------------------- Skeletons.dfy --------------------

-Skeletons.dfy(45,3): Error BP5003: A postcondition might not hold on this return path.

-Skeletons.dfy(44,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    Skeletons.dfy[C0](32,5): anon11_LoopHead

-    (0,0): anon11_LoopBody

-    Skeletons.dfy[C0](32,5): anon12_Else

-    (0,0): anon13_Then

-    Skeletons.dfy[C0](37,19): anon15_Else

-    (0,0): anon10

-

-Dafny program verifier finished with 9 verified, 1 error

-

--------------------- OpaqueFunctions.dfy --------------------

-OpaqueFunctions.dfy(27,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-OpaqueFunctions.dfy(52,7): Error BP5002: A precondition for this call might not hold.

-OpaqueFunctions.dfy(24,16): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-OpaqueFunctions.dfy(58,20): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-OpaqueFunctions.dfy(60,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-OpaqueFunctions.dfy(63,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-OpaqueFunctions.dfy(66,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-OpaqueFunctions.dfy(77,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-OpaqueFunctions.dfy(79,9): Error BP5002: A precondition for this call might not hold.

-OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-OpaqueFunctions.dfy(86,20): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-OpaqueFunctions.dfy(88,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-OpaqueFunctions.dfy(91,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-OpaqueFunctions.dfy(94,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-OpaqueFunctions.dfy(105,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-OpaqueFunctions.dfy(107,9): Error BP5002: A precondition for this call might not hold.

-OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-OpaqueFunctions.dfy(114,20): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-OpaqueFunctions.dfy(116,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-OpaqueFunctions.dfy(119,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-OpaqueFunctions.dfy(122,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-OpaqueFunctions.dfy(138,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 43 verified, 19 errors

-

--------------------- Maps.dfy --------------------

-Maps.dfy(78,8): Error: element may not be in domain

-Execution trace:

-    (0,0): anon0

-Maps.dfy(128,13): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 32 verified, 2 errors

-

--------------------- LiberalEquality.dfy --------------------

-LiberalEquality.dfy(20,14): Error: arguments must have the same type (got T and U)

-LiberalEquality.dfy(39,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)

-LiberalEquality.dfy(54,14): Error: arguments must have the same type (got array<int> and array<bool>)

-3 resolution/type errors detected in LiberalEquality.dfy

-

--------------------- RefinementModificationChecking.dfy --------------------

-RefinementModificationChecking.dfy(19,4): Error: cannot assign to variable defined previously

-RefinementModificationChecking.dfy(20,4): Error: cannot assign to variable defined previously

-2 resolution/type errors detected in RefinementModificationChecking.dfy

-

--------------------- TailCalls.dfy --------------------

-TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code

-TailCalls.dfy(33,12): Error: 'decreases *' is allowed only on tail-recursive methods

-TailCalls.dfy(40,12): Error: 'decreases *' is allowed only on tail-recursive methods

-TailCalls.dfy(45,12): Error: 'decreases *' is allowed only on tail-recursive methods

-TailCalls.dfy(67,12): Error: 'decreases *' is allowed only on tail-recursive methods

-5 resolution/type errors detected in TailCalls.dfy

-

--------------------- IteratorResolution.dfy --------------------

-IteratorResolution.dfy(62,9): Error: LHS of assignment must denote a mutable field

-IteratorResolution.dfy(67,18): Error: arguments must have the same type (got _T0 and int)

-IteratorResolution.dfy(79,19): Error: RHS (of type bool) not assignable to LHS (of type int)

-IteratorResolution.dfy(82,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called

-IteratorResolution.dfy(86,15): Error: logical negation expects a boolean argument (instead got int)

-IteratorResolution.dfy(20,9): Error: LHS of assignment must denote a mutable field

-IteratorResolution.dfy(22,9): Error: LHS of assignment must denote a mutable field

-IteratorResolution.dfy(126,9): Error: unresolved identifier: _decreases3

-IteratorResolution.dfy(127,21): Error: arguments must have the same type (got int and ?)

-IteratorResolution.dfy(128,2): Error: LHS of assignment must denote a mutable field

-IteratorResolution.dfy(135,9): Error: unresolved identifier: _decreases1

-IteratorResolution.dfy(140,9): Error: unresolved identifier: _decreases0

-12 resolution/type errors detected in IteratorResolution.dfy

-

--------------------- Iterators.dfy --------------------

-Iterators.dfy(251,9): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Else

-Iterators.dfy(274,9): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Else

-Iterators.dfy(284,24): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Else

-Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Else

-Iterators.dfy(326,24): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-Iterators.dfy(343,9): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Else

-Iterators.dfy(353,24): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-Iterators.dfy(370,9): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Else

-Iterators.dfy(103,22): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Iterators.dfy(106,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon3

-Iterators.dfy(177,28): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon15_Then

-Iterators.dfy(208,7): Error: an assignment to _new is only allowed to shrink the set

-Execution trace:

-    (0,0): anon0

-    Iterators.dfy(197,3): anon16_LoopHead

-    (0,0): anon16_LoopBody

-    Iterators.dfy(197,3): anon17_Else

-    Iterators.dfy(197,3): anon19_Else

-    (0,0): anon20_Then

-Iterators.dfy(212,21): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    Iterators.dfy(197,3): anon16_LoopHead

-    (0,0): anon16_LoopBody

-    Iterators.dfy(197,3): anon17_Else

-    Iterators.dfy(197,3): anon19_Else

-    (0,0): anon21_Then

-Iterators.dfy(40,14): Error BP5002: A precondition for this call might not hold.

-Iterators.dfy(4,10): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon35_Then

-    (0,0): anon2

-    (0,0): anon36_Then

-    (0,0): anon5

-    (0,0): anon37_Then

-Iterators.dfy(89,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Iterators.dfy(119,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Iterators.dfy(150,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-Iterators.dfy(155,16): Error BP5002: A precondition for this call might not hold.

-Iterators.dfy(125,10): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon3

-Iterators.dfy(234,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    Iterators.dfy(225,3): anon14_LoopHead

-    (0,0): anon14_LoopBody

-    Iterators.dfy(225,3): anon15_Else

-    Iterators.dfy(225,3): anon18_Else

-    (0,0): anon19_Else

-

-Dafny program verifier finished with 65 verified, 20 errors

-

--------------------- RankPos.dfy --------------------

-

-Dafny program verifier finished with 11 verified, 0 errors

-

--------------------- RankNeg.dfy --------------------

-RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

-RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

-RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

-RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

-

-Dafny program verifier finished with 1 verified, 4 errors

-

--------------------- Computations.dfy --------------------

-

-Dafny program verifier finished with 58 verified, 0 errors

-

--------------------- ComputationsNeg.dfy --------------------

-ComputationsNeg.dfy(7,3): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-ComputationsNeg.dfy(11,1): Error BP5003: A postcondition might not hold on this return path.

-ComputationsNeg.dfy(10,17): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-ComputationsNeg.dfy(23,1): Error BP5003: A postcondition might not hold on this return path.

-ComputationsNeg.dfy(22,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-ComputationsNeg.dfy(36,13): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-ComputationsNeg.dfy(45,13): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 7 verified, 5 errors

-

--------------------- Include.dfy --------------------

-Include.dfy(19,19): Error BP5003: A postcondition might not hold on this return path.

-Includee.dfy(17,20): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-Includee.dfy[Concrete](22,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Include.dfy(27,7): Error BP5003: A postcondition might not hold on this return path.

-Includee.dfy[Concrete](20,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-

-Dafny program verifier finished with 4 verified, 3 errors

-

--------------------- Includee.dfy --------------------

-Includee.dfy(21,3): Error BP5003: A postcondition might not hold on this return path.

-Includee.dfy(20,15): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-Includee.dfy(24,18): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Includee.dfy(6,1): Error BP5003: A postcondition might not hold on this return path.

-Includee.dfy(5,13): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 5 verified, 3 errors

-

--------------------- AutoReq.dfy --------------------

-AutoReq.dfy(247,3): Error: possible violation of function precondition

-AutoReq.dfy(239,12): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-AutoReq.dfy(13,3): Error: possible violation of function precondition

-AutoReq.dfy(5,14): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-AutoReq.dfy(25,3): Error: possible violation of function precondition

-AutoReq.dfy(5,14): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-AutoReq.dfy(38,12): Error: assertion violation

-AutoReq.dfy(31,13): Related location

-AutoReq.dfy(7,5): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Then

-AutoReq.dfy(38,12): Error: possible violation of function precondition

-AutoReq.dfy(5,14): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Then

-AutoReq.dfy(40,12): Error: assertion violation

-AutoReq.dfy(31,27): Related location

-AutoReq.dfy(7,5): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon10_Then

-AutoReq.dfy(40,12): Error: possible violation of function precondition

-AutoReq.dfy(5,14): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon10_Then

-AutoReq.dfy(45,12): Error: assertion violation

-AutoReq.dfy(31,13): Related location

-AutoReq.dfy(7,5): Related location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

-

-Dafny program verifier finished with 52 verified, 8 errors

-

--------------------- DatatypeUpdate.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- ModifyStmt.dfy --------------------

-ModifyStmt.dfy(27,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-ModifyStmt.dfy(42,5): Error: modify statement may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-ModifyStmt.dfy(48,5): Error: modify statement may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-ModifyStmt.dfy(61,5): Error: modify statement may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-ModifyStmt.dfy(70,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-ModifyStmt.dfy(89,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon9_Then

-    ModifyStmt.dfy(81,7): anon10_LoopHead

-    (0,0): anon10_LoopBody

-    ModifyStmt.dfy(81,7): anon11_Else

-    (0,0): anon12_Then

-    (0,0): anon8

-ModifyStmt.dfy(99,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-ModifyStmt.dfy(110,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-ModifyStmt.dfy(122,16): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-ModifyStmt.dfy(134,7): Error: assignment may update an object not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-ModifyStmt.dfy(172,15): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 25 verified, 11 errors

-

--------------------- SeqSlice.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- RealCompare.dfy --------------------

-RealCompare.dfy(35,5): Error: failure to decrease termination measure

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0

-Execution trace:

-    (0,0): anon0

-RealCompare.dfy(141,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    RealCompare.dfy(133,3): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    RealCompare.dfy(133,3): anon8_Else

-    (0,0): anon9_Then

-RealCompare.dfy(156,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    RealCompare.dfy(147,3): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    RealCompare.dfy(147,3): anon10_Else

-    (0,0): anon12_Then

-

-Dafny program verifier finished with 24 verified, 4 errors

-

--------------------- AssumptionVariables0.dfy --------------------

-AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"

-AssumptionVariables0.dfy(9,20): Error: assumption variable must be ghost

-AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool'

-AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"

-AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"

-AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost

-AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool'

-AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

-13 resolution/type errors detected in AssumptionVariables0.dfy

-

--------------------- AssumptionVariables1.dfy --------------------

-

-Dafny program verifier finished with 4 verified, 0 errors

-

--------------------- Superposition.dfy --------------------

-

-Verifying CheckWellformed$$_0_M0.C.M ...

-  [0 proof obligations]  verified

-

-Verifying Impl$$_0_M0.C.M ...

-  [4 proof obligations]  verified

-

-Verifying CheckWellformed$$_0_M0.C.P ...

-  [4 proof obligations]  verified

-

-Verifying CheckWellformed$$_0_M0.C.Q ...

-  [3 proof obligations]  error

-Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this return path.

-Superposition.dfy(28,26): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-

-Verifying CheckWellformed$$_0_M0.C.R ...

-  [3 proof obligations]  error

-Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this return path.

-Superposition.dfy(34,26): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-

-Verifying CheckWellformed$$_1_M1.C.M ...

-  [0 proof obligations]  verified

-

-Verifying Impl$$_1_M1.C.M ...

-  [1 proof obligation]  verified

-

-Verifying CheckWellformed$$_1_M1.C.P ...

-  [1 proof obligation]  error

-Superposition.dfy(50,15): Error BP5003: A postcondition might not hold on this return path.

-Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon9_Then

-    (0,0): anon6

-

-Verifying CheckWellformed$$_1_M1.C.Q ...

-  [0 proof obligations]  verified

-

-Verifying CheckWellformed$$_1_M1.C.R ...

-  [0 proof obligations]  verified

-

-Dafny program verifier finished with 7 verified, 3 errors

-

--------------------- SmallTests.dfy --------------------

-SmallTests.dfy(33,11): Error: index out of range

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(64,36): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Then

-SmallTests.dfy(65,51): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Else

-    (0,0): anon3

-    (0,0): anon13_Else

-SmallTests.dfy(66,22): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Then

-    (0,0): anon3

-    (0,0): anon13_Then

-    (0,0): anon6

-SmallTests.dfy(85,24): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    SmallTests.dfy(84,5): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    (0,0): anon9_Then

-SmallTests.dfy(119,5): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-    (0,0): anon3

-SmallTests.dfy(132,9): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-SmallTests.dfy(134,9): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-SmallTests.dfy(174,9): Error: assignment may update an object field not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon22_Else

-    (0,0): anon24_Else

-    (0,0): anon26_Else

-    (0,0): anon28_Then

-    (0,0): anon29_Then

-    (0,0): anon19

-SmallTests.dfy(198,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-SmallTests.dfy(205,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon3

-    (0,0): anon7_Then

-SmallTests.dfy(207,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon3

-    (0,0): anon7_Else

-SmallTests.dfy(253,24): Error BP5002: A precondition for this call might not hold.

-SmallTests.dfy(231,30): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    SmallTests.dfy(248,19): anon3_Else

-    (0,0): anon2

-SmallTests.dfy(358,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(368,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(378,6): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-SmallTests.dfy(682,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    SmallTests.dfy(679,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    SmallTests.dfy(679,5): anon8_Else

-    (0,0): anon9_Then

-SmallTests.dfy(703,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Then

-    (0,0): anon3

-SmallTests.dfy(288,3): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(282,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon18_Else

-    (0,0): anon23_Then

-    (0,0): anon24_Then

-    (0,0): anon15

-    (0,0): anon25_Else

-SmallTests.dfy(329,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon7

-SmallTests.dfy(336,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(346,4): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-SmallTests.dfy(390,10): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(393,41): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-SmallTests.dfy(553,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-    (0,0): anon2

-SmallTests.dfy(567,20): Error: left-hand sides 0 and 1 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon27_Then

-    (0,0): anon28_Then

-    (0,0): anon4

-    (0,0): anon29_Then

-    (0,0): anon30_Then

-    (0,0): anon9

-    (0,0): anon31_Then

-    (0,0): anon32_Then

-    (0,0): anon12

-SmallTests.dfy(569,15): Error: left-hand sides 1 and 2 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon27_Then

-    SmallTests.dfy(562,18): anon28_Else

-    (0,0): anon4

-    (0,0): anon29_Else

-    (0,0): anon30_Then

-    (0,0): anon9

-    (0,0): anon31_Else

-    (0,0): anon35_Then

-    (0,0): anon36_Then

-    (0,0): anon37_Then

-    (0,0): anon22

-    (0,0): anon38_Then

-SmallTests.dfy(576,25): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(589,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(613,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

-Execution trace:

-    (0,0): anon0

-SmallTests.dfy(636,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon9_Then

-    (0,0): anon4

-    (0,0): anon10_Then

-    (0,0): anon7

-SmallTests.dfy(650,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon6_Then

-    (0,0): anon3

-SmallTests.dfy(652,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Else

-SmallTests.dfy(665,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 87 verified, 33 errors

-

-Dafny program verifier finished with 0 verified, 0 errors

-

--------------------- LetExpr.dfy --------------------

-LetExpr.dfy(8,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-LetExpr.dfy(107,21): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

-LetExpr.dfy(251,19): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-LetExpr.dfy(254,19): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-LetExpr.dfy(256,24): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-LetExpr.dfy(285,14): Error: RHS is not certain to look like the pattern 'Agnes'

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-LetExpr.dfy(302,42): Error: value assigned to a nat must be non-negative

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-LetExpr.dfy(304,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-

-Dafny program verifier finished with 38 verified, 8 errors

-

-Dafny program verifier finished with 0 verified, 0 errors

-

--------------------- Calculations.dfy --------------------

-Calculations.dfy(6,6): Error: index out of range

-Execution trace:

-    (0,0): anon0

-    (0,0): anon24_Then

-Calculations.dfy(11,15): Error: index out of range

-Execution trace:

-    (0,0): anon0

-    (0,0): anon26_Then

-Calculations.dfy(11,19): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon26_Then

-Calculations.dfy(55,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    Calculations.dfy(50,3): anon5_Else

-Calculations.dfy(78,15): Error: index out of range

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Then

-Calculations.dfy(78,19): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Then

-

-Dafny program verifier finished with 9 verified, 6 errors

-

-Dafny program verifier finished with 0 verified, 0 errors

-

--------------------- DirtyLoops.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

-Dafny program verifier finished with 0 verified, 0 errors

-

-Dafny program verifier finished with 44 verified, 0 errors

-Compiled assembly into Compilation.exe

-

-Dafny program verifier finished with 15 verified, 0 errors

-Compilation error: Arbitrary type ('_module.MyType') cannot be compiled

-Compilation error: Iterator _module.Iter has no body

-Compilation error: Method _module._default.M has no body

-Compilation error: Method _module._default.P has no body

-Compilation error: an assume statement cannot be compiled (line 11)

-Compilation error: Function _module._default.F has no body

-Compilation error: Function _module._default.H has no body

-Compilation error: an assume statement cannot be compiled (line 20)

-Compilation error: an assume statement cannot be compiled (line 23)

-Compilation error: an assume statement cannot be compiled (line 28)

-Compilation error: an assume statement cannot be compiled (line 37)

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index f3297ed7..35c17112 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -912,3 +912,34 @@ method DirtyM(S: set<int>) {
   forall s | s in S ensures s < 0;

   assert s < 0; // error: s is unresolved

 }

+

+// ------------------- tuples -------------------

+

+method TupleResolution(x: int, y: int, r: real)

+{

+  var unit: () := ();

+  var expr: int := (x);

+  var pair: (int,int) := (x, x);

+  var triple: (int,int,int) := (y, x, x);

+  var badTriple: (int,real,int) := (y, x, r);  // error: parameters 1 and 2 have the wrong types

+  var quadruple: (int,real,int,real) := (y, r, x);  // error: trying to use a triple as a quadruple

+

+  assert unit == ();

+  assert pair.0 == pair.1;

+  assert triple.2 == x;

+

+  assert triple.2;  // error: 2 has type int, not the expected bool

+  assert triple.3 == pair.x;  // error(s):  3 and x are not destructors

+

+  var k0 := (5, (true, 2, 3.14));

+  var k1 := (((false, 10, 2.7)), 100, 120);

+  if k0.1 == k1.0 {

+    assert false;

+  } else if k0.1.1 < k1.0.1 {

+    assert k1.2 == 120;

+  }

+

+  // int and (int) are the same type (i.e., there are no 1-tuples)

+  var pp: (int) := x;

+  var qq: int := pp;

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 2c0664d9..22f3274e 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -133,4 +133,10 @@ ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only i
 ResolutionErrors.dfy(546,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses

 ResolutionErrors.dfy(913,9): Error: unresolved identifier: s

-135 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))

+ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))

+ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int

+ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3

+ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2

+ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))

+141 resolution/type errors detected in ResolutionErrors.dfy

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

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

+

+method M(x: int)

+{

+  var unit := ();

+  var expr := (x);

+  var pair := (x, x);

+  var triple := (x, x, x);

+}

+

+method N(x: int, y: int)

+{

+  var unit: () := ();

+  var expr: int := (x);

+  var pair: (int,int) := (x, x);

+  var triple: (int,int,int) := (y, x, x);

+

+  assert unit == ();

+  assert pair.0 == pair.1;

+  assert triple.2 == x;

+  assert triple.0 == triple.1;  // error: they may be different

+

+  var k := (24, 100 / y);  // error: possible division by zero

+  assert 2 <= k.0 < 29;

+

+  var k0 := (5, (true, 2, 3.14));

+  var k1 := (((false, 10, 2.7)), 100, 120);

+  if k0.1 == k1.0 {

+    assert false;

+  } else if k0.1.1 < k1.0.1 {

+    assert k1.2 == 120;

+  }

+}

diff --git a/Test/dafny0/Tuples.dfy.expect b/Test/dafny0/Tuples.dfy.expect
new file mode 100644
index 00000000..13c706d3
--- /dev/null
+++ b/Test/dafny0/Tuples.dfy.expect
@@ -0,0 +1,8 @@
+Tuples.dfy(22,19): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Tuples.dfy(24,21): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 3 verified, 2 errors

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
deleted file mode 100644
index 1a371ba3..00000000
--- a/Test/dafny0/runtest.bat
+++ /dev/null
@@ -1,61 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-for %%f in (Simple.dfy) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f

-)

-

-for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy

-            FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy

-            Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

-            ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy

-            Comprehensions.dfy Basics.dfy ControlStructures.dfy

-            Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

-            TypeParameters.dfy Datatypes.dfy StatementExpressions.dfy

-            Coinductive.dfy Corecursion.dfy CoResolution.dfy

-            CoPrefix.dfy CoinductiveProofs.dfy

-            TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy

-            LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

-            ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

-            CallStmtTests.dfy MultiSets.dfy PredExpr.dfy

-            Predicates.dfy Skeletons.dfy OpaqueFunctions.dfy

-            Maps.dfy LiberalEquality.dfy

-            RefinementModificationChecking.dfy TailCalls.dfy

-            IteratorResolution.dfy Iterators.dfy

-            RankPos.dfy RankNeg.dfy

-            Computations.dfy ComputationsNeg.dfy

-            Include.dfy Includee.dfy AutoReq.dfy DatatypeUpdate.dfy ModifyStmt.dfy SeqSlice.dfy

-            RealCompare.dfy

-            AssumptionVariables0.dfy AssumptionVariables1.dfy) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f

-)

-

-for %%f in (Superposition.dfy) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp /tracePOs %* %%f

-)

-

-for %%f in (SmallTests.dfy LetExpr.dfy Calculations.dfy) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.tmp.dfy %* %%f

-  %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy

-)

-

-for %%f in (DirtyLoops.dfy) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f

-  %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy

-)

-

-%DAFNY_EXE% %* Compilation.dfy

-%DAFNY_EXE% %* CompilationErrors.dfy

diff --git a/Test/dafny0/snapshots/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Snapshots0.v0.dfy
new file mode 100644
index 00000000..73db9f9c
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots0.v0.dfy
@@ -0,0 +1,8 @@
+method foo()

+{

+  bar();

+  assert false;

+}

+

+method bar()

+  ensures false;

diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy
new file mode 100644
index 00000000..28f9f283
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots0.v1.dfy
@@ -0,0 +1,8 @@
+method foo()

+{

+  bar();

+  assert false;

+}

+

+method bar()

+  ensures true;

diff --git a/Test/dafny0/snapshots/lit.local.cfg b/Test/dafny0/snapshots/lit.local.cfg
new file mode 100644
index 00000000..07cb869f
--- /dev/null
+++ b/Test/dafny0/snapshots/lit.local.cfg
@@ -0,0 +1,5 @@
+# This test is unusual in that we don't use the .bpl files
+# directly on the command line. So instead we'll invoke
+# files in this directory with extension '.snapshot'. There
+# will only be one for now
+config.suffixes = ['.snapshot']
diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot
new file mode 100644
index 00000000..6d2f880f
--- /dev/null
+++ b/Test/dafny0/snapshots/runtest.snapshot
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
new file mode 100644
index 00000000..7906e7a5
--- /dev/null
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -0,0 +1,7 @@
+

+Dafny program verifier finished with 3 verified, 0 errors

+Snapshots0.v1.dfy(4,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 2 verified, 1 error

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
deleted file mode 100644
index e60451c2..00000000
--- a/Test/dafny1/Answer
+++ /dev/null
@@ -1,124 +0,0 @@
-

--------------------- Queue.dfy --------------------

-

-Dafny program verifier finished with 22 verified, 0 errors

-

--------------------- PriorityQueue.dfy --------------------

-

-Dafny program verifier finished with 24 verified, 0 errors

-

--------------------- ExtensibleArray.dfy --------------------

-

-Dafny program verifier finished with 11 verified, 0 errors

-

--------------------- ExtensibleArrayAuto.dfy --------------------

-

-Dafny program verifier finished with 11 verified, 0 errors

-

--------------------- BinaryTree.dfy --------------------

-

-Dafny program verifier finished with 24 verified, 0 errors

-

--------------------- UnboundedStack.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-

--------------------- SeparationLogicList.dfy --------------------

-

-Dafny program verifier finished with 16 verified, 0 errors

-

--------------------- ListCopy.dfy --------------------

-

-Dafny program verifier finished with 4 verified, 0 errors

-

--------------------- ListReverse.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- ListContents.dfy --------------------

-

-Dafny program verifier finished with 9 verified, 0 errors

-

--------------------- MatrixFun.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

-

--------------------- pow2.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

-

--------------------- SchorrWaite.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- SchorrWaite-stages.dfy --------------------

-

-Dafny program verifier finished with 16 verified, 0 errors

-

--------------------- Cubes.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- SumOfCubes.dfy --------------------

-

-Dafny program verifier finished with 17 verified, 0 errors

-

--------------------- FindZero.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

-

--------------------- TerminationDemos.dfy --------------------

-

-Dafny program verifier finished with 14 verified, 0 errors

-

--------------------- Substitution.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-

--------------------- TreeDatatype.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- KatzManna.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-

--------------------- Induction.dfy --------------------

-

-Dafny program verifier finished with 33 verified, 0 errors

-

--------------------- Rippling.dfy --------------------

-

-Dafny program verifier finished with 141 verified, 0 errors

-

--------------------- MoreInduction.dfy --------------------

-MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 15 verified, 4 errors

-

--------------------- Celebrity.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- BDD.dfy --------------------

-

-Dafny program verifier finished with 5 verified, 0 errors

-

--------------------- UltraFilter.dfy --------------------

-

-Dafny program verifier finished with 19 verified, 0 errors

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
deleted file mode 100644
index f02a7965..00000000
--- a/Test/dafny1/runtest.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ExtensibleArrayAuto.dfy BinaryTree.dfy UnboundedStack.dfy SeparationLogicList.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy MatrixFun.dfy pow2.dfy SchorrWaite.dfy SchorrWaite-stages.dfy Cubes.dfy SumOfCubes.dfy FindZero.dfy TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy Induction.dfy Rippling.dfy MoreInduction.dfy Celebrity.dfy BDD.dfy UltraFilter.dfy

-

-rem for %%f in (Queue.dfy PriorityQueue.dfy

-rem             ExtensibleArray.dfy ExtensibleArrayAuto.dfy

-rem             BinaryTree.dfy

-rem             UnboundedStack.dfy

-rem             SeparationLogicList.dfy

-rem             ListCopy.dfy ListReverse.dfy ListContents.dfy

-rem             MatrixFun.dfy pow2.dfy

-rem             SchorrWaite.dfy SchorrWaite-stages.dfy

-rem             Cubes.dfy SumOfCubes.dfy FindZero.dfy

-rem             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

-rem             Induction.dfy Rippling.dfy MoreInduction.dfy

-rem             Celebrity.dfy BDD.dfy

-rem             UltraFilter.dfy

-rem             ) do (

-rem   echo.

-rem   echo -------------------- %%f --------------------

-rem   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-rem )

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
deleted file mode 100644
index 9fa6f4ef..00000000
--- a/Test/dafny2/Answer
+++ /dev/null
@@ -1,60 +0,0 @@
-

--------------------- Classics.dfy --------------------

-

-Dafny program verifier finished with 5 verified, 0 errors

-

--------------------- TreeBarrier.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

-

--------------------- COST-verif-comp-2011-1-MaxArray.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- COST-verif-comp-2011-2-MaxTree-class.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

-

--------------------- COST-verif-comp-2011-2-MaxTree-datatype.dfy --------------------

-

-Dafny program verifier finished with 5 verified, 0 errors

-

--------------------- COST-verif-comp-2011-3-TwoDuplicates.dfy --------------------

-

-Dafny program verifier finished with 4 verified, 0 errors

-

--------------------- COST-verif-comp-2011-4-FloydCycleDetect.dfy --------------------

-

-Dafny program verifier finished with 25 verified, 0 errors

-

--------------------- StoreAndRetrieve.dfy --------------------

-

-Dafny program verifier finished with 22 verified, 0 errors

-

--------------------- Intervals.dfy --------------------

-

-Dafny program verifier finished with 5 verified, 0 errors

-

--------------------- TreeFill.dfy --------------------

-

-Dafny program verifier finished with 3 verified, 0 errors

-

--------------------- TuringFactorial.dfy --------------------

-

-Dafny program verifier finished with 3 verified, 0 errors

-

--------------------- MajorityVote.dfy --------------------

-

-Dafny program verifier finished with 16 verified, 0 errors

-

--------------------- SegmentSum.dfy --------------------

-

-Dafny program verifier finished with 3 verified, 0 errors

-

--------------------- MonotonicHeapstate.dfy --------------------

-

-Dafny program verifier finished with 36 verified, 0 errors

-

--------------------- Calculations.dfy --------------------

-

-Dafny program verifier finished with 31 verified, 0 errors

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
deleted file mode 100644
index d038acce..00000000
--- a/Test/dafny2/runtest.bat
+++ /dev/null
@@ -1,27 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-REM soon again:    SnapshotableTrees.dfy

-

-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Classics.dfy TreeBarrier.dfy COST-verif-comp-2011-1-MaxArray.dfy COST-verif-comp-2011-2-MaxTree-class.dfy COST-verif-comp-2011-2-MaxTree-datatype.dfy COST-verif-comp-2011-3-TwoDuplicates.dfy COST-verif-comp-2011-4-FloydCycleDetect.dfy StoreAndRetrieve.dfy Intervals.dfy TreeFill.dfy TuringFactorial.dfy MajorityVote.dfy SegmentSum.dfy MonotonicHeapstate.dfy Calculations.dfy

-

-rem for %%f in (

-rem     Classics.dfy

-rem     TreeBarrier.dfy

-rem     COST-verif-comp-2011-1-MaxArray.dfy

-rem     COST-verif-comp-2011-2-MaxTree-class.dfy

-rem     COST-verif-comp-2011-2-MaxTree-datatype.dfy

-rem     COST-verif-comp-2011-3-TwoDuplicates.dfy

-rem     COST-verif-comp-2011-4-FloydCycleDetect.dfy

-rem     StoreAndRetrieve.dfy

-rem     Intervals.dfy TreeFill.dfy TuringFactorial.dfy

-rem     MajorityVote.dfy SegmentSum.dfy

-rem     MonotonicHeapstate.dfy Calculations.dfy

-rem   ) do (

-rem   echo.

-rem   echo -------------------- %%f --------------------

-rem   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-rem )

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
deleted file mode 100644
index 9e8ac835..00000000
--- a/Test/dafny3/Answer
+++ /dev/null
@@ -1,64 +0,0 @@
-
--------------------- Iter.dfy --------------------

-

-Dafny program verifier finished with 15 verified, 0 errors

-
--------------------- Streams.dfy --------------------

-

-Dafny program verifier finished with 52 verified, 0 errors

-
--------------------- Dijkstra.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-
--------------------- CachedContainer.dfy --------------------

-

-Dafny program verifier finished with 47 verified, 0 errors

-
--------------------- SimpleInduction.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-
--------------------- SimpleCoinduction.dfy --------------------

-

-Dafny program verifier finished with 31 verified, 0 errors

-
--------------------- CalcExample.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-
--------------------- InductionVsCoinduction.dfy --------------------

-

-Dafny program verifier finished with 20 verified, 0 errors

-
--------------------- Zip.dfy --------------------

-

-Dafny program verifier finished with 24 verified, 0 errors

-
--------------------- SetIterations.dfy --------------------

-

-Dafny program verifier finished with 13 verified, 0 errors

-
--------------------- Paulson.dfy --------------------

-

-Dafny program verifier finished with 28 verified, 0 errors

-
--------------------- Filter.dfy --------------------

-

-Dafny program verifier finished with 43 verified, 0 errors

-
--------------------- WideTrees.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-
--------------------- InfiniteTrees.dfy --------------------

-

-Dafny program verifier finished with 88 verified, 0 errors

-
--------------------- OpaqueTrees.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-
--------------------- GenericSort.dfy --------------------

-

-Dafny program verifier finished with 36 verified, 0 errors

diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
deleted file mode 100644
index 41971d4e..00000000
--- a/Test/dafny3/runtest.bat
+++ /dev/null
@@ -1,19 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy OpaqueTrees.dfy GenericSort.dfy

-

-rem for %%f in (

-rem   Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy

-rem   SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy

-rem   InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy

-rem   Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy

-rem   OpaqueTrees.dfy GenericSort.dfy

-rem ) do (

-rem   echo.

-rem   echo -------------------- %%f --------------------

-rem   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-rem )

diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer
deleted file mode 100644
index 14986a59..00000000
--- a/Test/dafny4/Answer
+++ /dev/null
@@ -1,43 +0,0 @@
-

--------------------- CoqArt-InsertionSort.dfy --------------------

-

-Dafny program verifier finished with 36 verified, 0 errors

-

--------------------- GHC-MergeSort.dfy --------------------

-

-Dafny program verifier finished with 83 verified, 0 errors

-

--------------------- Fstar-QuickSort.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-

--------------------- Primes.dfy --------------------

-

-Dafny program verifier finished with 24 verified, 0 errors

-

--------------------- KozenSilva.dfy --------------------

-

-Dafny program verifier finished with 47 verified, 0 errors

-

--------------------- SoftwareFoundations-Basics.dfy --------------------

-SoftwareFoundations-Basics.dfy(41,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 82 verified, 1 error

-

--------------------- NumberRepresentations.dfy --------------------

-

-Dafny program verifier finished with 33 verified, 0 errors

-

--------------------- Circ.dfy --------------------

-

-Dafny program verifier finished with 16 verified, 0 errors

-

--------------------- ACL2-extractor.dfy --------------------

-

-Dafny program verifier finished with 33 verified, 0 errors

-

--------------------- ClassRefinement.dfy --------------------

-

-Dafny program verifier finished with 18 verified, 0 errors

diff --git a/Test/dafny4/runtest.bat b/Test/dafny4/runtest.bat
deleted file mode 100644
index cec5d271..00000000
--- a/Test/dafny4/runtest.bat
+++ /dev/null
@@ -1,7 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy ACL2-extractor.dfy ClassRefinement.dfy

diff --git a/Test/runtest.bat b/Test/runtest.bat
deleted file mode 100644
index dfc3ae00..00000000
--- a/Test/runtest.bat
+++ /dev/null
@@ -1,39 +0,0 @@
-@echo off

-rem Usage: runtest.bat <dir>

-if "%1" == "" goto noDirSpecified

-if not exist %1\nul goto noDirExists

-echo ----- Running regression test %1

-pushd %1

-if not exist runtest.bat goto noRunTest

-call runtest.bat -nologo -logPrefix:%* > Output

-rem There seem to be some race between finishing writing to the Output file, and running fc.

-rem Calling fc twice seems to fix (or at least alleviate) the problem.

-fc /W Answer Output > nul

-fc /W Answer Output > nul

-if not errorlevel 1 goto passTest

-echo ============ %1 FAILED ====================================

-goto errorEnd

-

-:passTest

-echo Success: %1

-goto end

-

-:noDirSpecified

-echo runtest: Error: Syntax: runtest testDirectory [ additionalTestArguments ... ]

-goto errorEnd

-

-:noDirExists

-echo runtest: Error: There is no test directory %1

-goto errorEnd

-

-:noRunTest

-echo runtest: Error: no runtest.bat found in test directory %1

-goto errorEnd

-

-:errorEnd

-popd

-exit /b 1

-

-:end

-popd

-exit /b 0

diff --git a/Test/runtestall.bat b/Test/runtestall.bat
deleted file mode 100644
index 207bb030..00000000
--- a/Test/runtestall.bat
+++ /dev/null
@@ -1,24 +0,0 @@
-@echo off

-setlocal

-

-set errors=0

-

-if "%1" == "short" goto UseShort

-

-set IncludeLong=True

-goto Loop

-

-:UseShort

-set IncludeLong=False

-shift

-goto Loop

-

-:Loop

-for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Use call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1

-

-if not %IncludeLong%==True goto End

-

-for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Long call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1

-

-:End

-exit /b %errors%
\ No newline at end of file
diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer
deleted file mode 100644
index 90bbcc78..00000000
--- a/Test/vacid0/Answer
+++ /dev/null
@@ -1,12 +0,0 @@
-

--------------------- LazyInitArray.dfy --------------------

-

-Dafny program verifier finished with 7 verified, 0 errors

-

--------------------- SparseArray.dfy --------------------

-

-Dafny program verifier finished with 9 verified, 0 errors

-

--------------------- Composite.dfy --------------------

-

-Dafny program verifier finished with 16 verified, 0 errors

diff --git a/Test/vacid0/AnswerRuntimeChecking b/Test/vacid0/AnswerRuntimeChecking
deleted file mode 100644
index e69de29b..00000000
--- a/Test/vacid0/AnswerRuntimeChecking
+++ /dev/null
diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
deleted file mode 100644
index d7f31c3b..00000000
--- a/Test/vacid0/runtest.bat
+++ /dev/null
@@ -1,13 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /verifySeparately %* LazyInitArray.dfy SparseArray.dfy Composite.dfy

-

-rem for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

-rem   echo.

-rem   echo -------------------- %%f --------------------

-rem   %DAFNY_EXE% /compile:0 %* %%f

-rem )

diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer
deleted file mode 100644
index 43eddcb1..00000000
--- a/Test/vstte2012/Answer
+++ /dev/null
@@ -1,24 +0,0 @@
-

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

-

--------------------- RingBufferAuto.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 22 verified, 0 errors

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
deleted file mode 100644
index 7e597fd4..00000000
--- a/Test/vstte2012/runtest.bat
+++ /dev/null
@@ -1,23 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Two-Way-Sort.dfy Combinators.dfy RingBuffer.dfy RingBufferAuto.dfy Tree.dfy

-

-echo.

-echo -------------------- BreadthFirstSearch.dfy --------------------

-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /vcsMaxKeepGoingSplits:10 %* BreadthFirstSearch.dfy

-

-rem for %%f in (

-rem     Two-Way-Sort.dfy

-rem     Combinators.dfy

-rem     RingBuffer.dfy RingBufferAuto.dfy

-rem     Tree.dfy

-rem     BreadthFirstSearch.dfy

-rem   ) do (

-rem   echo.

-rem   echo -------------------- %%f --------------------

-rem   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-rem )