Merge

23 files changed, 392 insertions, 76 deletions

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index f6477708..391ca5f7 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -42,12 +42,12 @@ class A {
     assert zz2 != zz0;  // holds because zz2 is newly allocated

     var o: object := zz0;

     assert this != o;  // holds because zz0 has a different type

-    /******  This would be a good thing to be able to verify, but the current encoding is not up to the task

+

     if (zz0 != null && zz1 != null && 2 <= zz0.Length && zz0.Length == zz1.Length) {

       o := zz1[1];

       assert zz0[1] == o ==> o == null;  // holds because zz0 and zz1 have different element types

     }

-    ******/

+

     assert zz2[20] == null;  // error: no reason that this must hold

   }

 

@@ -152,7 +152,7 @@ class A {
     ensures fresh(b) && Q1(b[..]);

 }

 

-type B;

+class B { }

 

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

 

@@ -301,3 +301,29 @@ method AllocationBusiness2(a: array2<MyClass>, i: int, j: int)
   var c := new MyClass;

   assert c !in a[i,j].Repr;  // the proof requires allocation axioms for multi-dim arrays

 }

+

+// ------- a regression test, testing that dtype is set correctly after allocation ------

+

+module DtypeRegression {

+  predicate array_equal(a: array<int>, b: array<int>)

+    requires a != null && b != null;

+    reads a, b;

+  {

+    a[..] == b[..]

+  }

+

+  method duplicate_array(input: array<int>, len: int) returns (output: array<int>) 

+    requires input != null && len == input.Length;

+    ensures output != null && array_equal(input, output);

+  {

+    output := new int[len];

+    var i := 0;

+    while i < len

+      invariant 0 <= i <= len;

+      invariant forall j :: 0 <= j < i ==> output[j] == input[j];

+    {

+      output[i] := input[i];

+      i := i + 1;

+    }

+  }

+}

diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect
index 081fd258..bf4da25f 100644
--- a/Test/dafny0/Array.dfy.expect
+++ b/Test/dafny0/Array.dfy.expect
@@ -13,6 +13,14 @@ Execution trace:
 Array.dfy(51,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

+    (0,0): anon12_Then

+    (0,0): anon13_Then

+    (0,0): anon14_Then

+    (0,0): anon6

+    (0,0): anon15_Then

+    (0,0): anon16_Then

+    (0,0): anon9

+    (0,0): anon11

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

 Execution trace:

     (0,0): anon0

@@ -104,4 +112,4 @@ Execution trace:
     (0,0): anon2

     (0,0): anon6_Then

 

-Dafny program verifier finished with 46 verified, 20 errors

+Dafny program verifier finished with 49 verified, 20 errors

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 6e71e5b2..26baa35f 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -427,23 +427,23 @@ method HexTest()
   assert forall i :: 0 <= i < |first16upper| ==> first16upper[i] == i;

 

   var randomHex := [ 0xCF4458F2, 0x9A5C5BAF, 0x26A6ABD6, 0x00EB3933, 0x9123D2CF, 0xBE040001, 0x5AD038FA, 0xC75597A6, 0x7CF821A7, 0xCDEFB617, 0x4889D968, 0xB05F896A,

-             0x75B18DB2, 0xCAD773B0, 0xD8845EF8, 0x8EFA513D, 0x8EBAD321, 0x9C405DDE, 0x0EA9DF16, 0xCD48236A, 0x8A6892CF, 0x99BF0779, 0xEA52E108, 0x0379BF46, 

-             0x610D0339, 0xDB433BC7, 0xE94C026E, 0xFC18735C, 0x6A5FBDB3, 0xFDA622F9, 0x6204DB79, 0x52050F94, 0x5ABDD3FD, 0x7F1CFCDF, 0xEC7C907F, 0xFA41A43D, 

-             0x02FBF254, 0x9E76751A, 0xF753002C, 0x9635D361, 0xBA2C14E6, 0x415CA2FB, 0xA478EF6C, 0x7F80D7EC, 0xB4DD8598, 0x06C4ED20, 0xBFC9F800, 0x69F9675D, 

-             0x730D85E7, 0x30152491, 0x0226b79d, 0x6c7f895c, 0x4f466fa2, 0x2e470749, 0xacacf22e, 0x455ab875, 0xa0927dc7, 0xe27c93d7, 0x4f134daf, 0xd2c6c190, 

-             0xc95f056e, 0x45547ddf, 0x6a5c2767, 0xadc55905, 0xc5d6217d, 0x4ae4453e, 0xbe11d3d9, 0x339b8b14, 0xe68f7571, 0xf528199d, 0x0e640ee0, 0x9f716143, 

-             0x1520b76f, 0x7bfe38e9, 0x8c289b71, 0x677ff535, 0x0bb94f4e, 0xfb417c00, 0xa1cac03a, 0x5e3cdaf2, 0x7616f734, 0xb55744fb, 0x27642f2b, 0xa161c47e, 

-             0xbfcd3fff, 0xa62df579, 0x3ea317b0, 0xc87063bf, 0x0038c98d, 0x95a5e874, 0x76d824f6, 0x18687e3e, 0x4be6d02a, 0x2c2cc14c, 0x6e91d56b, 0x76e2bb30, 

-             0xcd85f1cc, 0x6219d3ae, 0xbe59d8d4, 0xd8C6FAF7 ];

+             0x75B1_8DB2, 0xCAD773B0, 0xD8845EF8, 0x8EFA513D, 0x8EBAD321, 0x9C405DDE, 0x0EA9DF16, 0xCD48236A, 0x8A6892CF, 0x99BF0779, 0xEA52E108, 0x0379BF46, 

+             0x610D_0339, 0xDB433BC7, 0xE94C026E, 0xFC18735C, 0x6A5FBDB3, 0xFDA622F9, 0x6204DB79, 0x52050F94, 0x5ABDD3FD, 0x7F1CFCDF, 0xEC7C907F, 0xFA41A43D, 

+             0x02FB_F254, 0x9E76751A, 0xF753002C, 0x9635D361, 0xBA2C14E6, 0x415CA2FB, 0xA478EF6C, 0x7F80D7EC, 0xB4DD8598, 0x06C4ED20, 0xBFC9F800, 0x69F9675D, 

+             0x730D_85E7, 0x30152491, 0x0226b79d, 0x6c7f895c, 0x4f466fa2, 0x2e470749, 0xacacf22e, 0x455ab875, 0xa0927dc7, 0xe27c93d7, 0x4f134daf, 0xd2c6c190, 

+             0xc95f_056e, 0x45547ddf, 0x6a5c2767, 0xadc55905, 0xc5d6217d, 0x4ae4453e, 0xbe11d3d9, 0x339b8b14, 0xe68f7571, 0xf528199d, 0x0e640ee0, 0x9f716143, 

+             0x1520_b76f, 0x7bfe38e9, 0x8c289b71, 0x677ff535, 0x0bb94f4e, 0xfb417c00, 0xa1cac03a, 0x5e3cdaf2, 0x7616f734, 0xb55744fb, 0x27642f2b, 0xa161c47e, 

+             0xbfcd_3fff, 0xa62df579, 0x3ea317b0, 0xc87063bf, 0x0038c98d, 0x95a5e874, 0x76d824f6, 0x18687e3e, 0x4be6d02a, 0x2c2cc14c, 0x6e91d56b, 0x76e2bb30, 

+             0xcd85_f1cc, 0x6219d3ae, 0xbe59d8d4, 0xd_8_C_6_F_A_F_7 ];

   var randomDec := [ 3477362930, 2589744047, 648457174, 15415603, 2435044047, 3187933185, 1523595514, 3344275366, 2096636327, 3455038999, 1216993640, 2959051114, 

-             1974570418, 3403117488, 3632553720, 2398769469, 2394608417, 2621464030, 246013718, 3444056938, 2322109135, 2579433337, 3931300104, 58310470, 

-             1628242745, 3678616519, 3914072686, 4229460828, 1784659379, 4255523577, 1644485497, 1376063380, 1522390013, 2132606175, 3967586431, 4198605885, 

-             50066004, 2658563354, 4149411884, 2520109921, 3123451110, 1096590075, 2759389036, 2139150316, 3034416536, 113569056, 3217684480, 1777952605, 

-             1930266087, 806691985, 36091805, 1820297564, 1330016162, 776406857, 2897015342, 1163573365, 2693955015, 3799815127, 1326665135, 3536241040,

-             3378447726, 1163165151, 1784424295, 2915391749, 3319144829, 1256473918, 3188839385, 865831700, 3868161393, 4113045917, 241438432, 2675007811,

+             1_974_570_418, 3403117488, 3632553720, 2398769469, 2394608417, 2621464030, 246013718, 3444056938, 2322109135, 2579433337, 3931300104, 58310470, 

+             1_628_242_745, 3678616519, 3914072686, 4229460828, 1784659379, 4255523577, 1644485497, 1376063380, 1522390013, 2132606175, 3967586431, 4198605885, 

+             50_066_004, 2658563354, 4149411884, 2520109921, 3123451110, 1096590075, 2759389036, 2139150316, 3034416536, 113569056, 3217684480, 1777952605, 

+             1_930_266_087, 806691985, 36091805, 1820297564, 1330016162, 776406857, 2897015342, 1163573365, 2693955015, 3799815127, 1326665135, 3536241040,

+             3_378_447_726, 1163165151, 1784424295, 2915391749, 3319144829, 1256473918, 3188839385, 865831700, 3868161393, 4113045917, 241438432, 2675007811,

              354465647, 2080258281, 2351471473, 1736439093, 196693838, 4215372800, 2714419258, 1581046514, 1981216564, 3042395387, 660877099, 2707539070,

              3217899519, 2788029817, 1050875824, 3362808767,  3721613, 2510678132, 1993876726, 409501246, 1273417770, 741130572, 1855051115, 1994570544,

-             3448107468, 1645859758, 3193559252, 3636919031 ];

+             3448107468, 1645859758, 3_1_9_3_5_5_9_2_5_2, 3636919031 ];

   assert forall i :: 0 <= i < |randomHex| ==> randomHex[i] == randomDec[i];

 }

 

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 2bff422f..d8ff3989 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -210,3 +210,20 @@ module GhostLetExpr {
     G(5, xyz)

   }

 }

+

+class DigitUnderscore_Names {

+  // the following would be the same integers, but they are different fields

+  var 0_1_0: int;

+  var 010: int;

+  var 10: int;

+  // ... as we see here:

+  method M()

+    modifies this;

+  {

+    this.0_1_0 := 007;

+    this.010 := 000_008;

+    this.10 := 0x0000_0009;

+    assert this.0_1_0 == int(00_07.0_0) && this.010 == 8 && this.10 == 9;

+    this.10 := 20;

+  }

+}

diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect
index af8ed2fc..0a1938ae 100644
--- a/Test/dafny0/Compilation.dfy.expect
+++ b/Test/dafny0/Compilation.dfy.expect
@@ -1,3 +1,3 @@
 

-Dafny program verifier finished with 44 verified, 0 errors

+Dafny program verifier finished with 46 verified, 0 errors

 Compiled assembly into Compilation.exe

diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy
index 09f07dd3..7869fba3 100644
--- a/Test/dafny0/DatatypeUpdate.dfy
+++ b/Test/dafny0/DatatypeUpdate.dfy
@@ -21,3 +21,10 @@ method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:
 

     assert abc[myint := abc.myint - 2] == foo[myint := x];

 }

+

+// regression test (for a previous bug in the Translator.Substituter):

+datatype Dt = Ctor(x: int, y: bool)

+function F(d: Dt): Dt

+{

+  d[x := 5]

+}

diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect
index 069e7767..52595bf9 100644
--- a/Test/dafny0/DatatypeUpdate.dfy.expect
+++ b/Test/dafny0/DatatypeUpdate.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 2 verified, 0 errors

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy
index 6a49e733..5d356f0a 100644
--- a/Test/dafny0/DirtyLoops.dfy
+++ b/Test/dafny0/DirtyLoops.dfy
@@ -1,6 +1,21 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"

 // RUN: %diff "%s.expect" "%t"

 

-method M(S: set<int>) {

+method M0(S: set<int>) {

   forall s | s in S ensures s < 0;

 }

+

+method M1(x: int)

+{

+  var i := x;

+  while (0 < i)

+    invariant i <= x;

+}

+

+method M2(x: int)

+{

+  var i := x;

+  while (0 < i)

+    invariant i <= x;

+    decreases i;

+}

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

-Dafny program verifier finished with 2 verified, 0 errors

+Dafny program verifier finished with 6 verified, 0 errors

 

 Dafny program verifier finished with 0 verified, 0 errors

diff --git a/Test/dafny0/LhsDuplicates.dfy b/Test/dafny0/LhsDuplicates.dfy
new file mode 100644
index 00000000..6a84c5a5
--- /dev/null
+++ b/Test/dafny0/LhsDuplicates.dfy
@@ -0,0 +1,70 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+class MyClass<T> {

+  var f: T;

+}

+

+method M<T>()

+{

+  var a, b := new T[100], new T[100];

+  forall i | 0 <= i < 100 {

+    a[3] := *;  // RHS is * -- this is okay

+  }

+  forall i | 0 <= i < 100 {

+    a[0] := b[0];  // RHSs are the same -- this is okay

+  }

+  forall i | 0 <= i < 100 {

+    a[0] := b[i];  // error: LHS's may be the same (while RHSs are different)

+  }

+}

+

+method N<T>(a: MyClass<T>, b: MyClass<T>)

+  requires a != null && b != null;

+  modifies a, b;

+{

+  var q := [a, b];

+  forall i | 0 <= i < 2 {

+    q[0].f := *;  // RHS is * -- this is okay

+  }

+  forall i | 0 <= i < 2 {

+    q[0].f := q[0].f;  // RHSs are the same -- this is okay

+  }

+  forall i | 0 <= i < 2 {

+    q[0].f := q[i].f;  // error: LHS's may be the same (while RHSs are different)

+  }

+}

+

+method P<T>(t0: T, t1: T, t2: T) {

+  var a: T, b: T;

+  a, a, a := *, t0, *;  // only one non-* RHS per variable -- this is okay

+  a, a, b, a, b := *, t1, t2, *, *;  // only one non-* RHS per variable -- this is okay

+  a, a, b, a, b := *, t1, t2, t0, *;  // error: duplicate LHS -- t0 and t1 may be different

+}

+

+method Q<T>(c0: MyClass<T>, c1: MyClass<T>)

+  requires c0 != null && c1 != null;

+  modifies c0, c1;

+{

+  c0.f, c1.f := c0.f, c0.f;  // okay -- RHSs are the same

+  c0.f, c0.f, c0.f, c0.f := *, *, c1.f, *;  // okay -- only one RHS is non-*

+  c0.f, c0.f, c0.f, c0.f := c0.f, *, c1.f, *;  // error -- duplicate LHR

+}

+

+method R<T>(i: nat, j: nat)

+  requires i < 10 && j < 10;

+{

+  var a := new T[10];

+  a[i], a[j] := a[5], a[5];  // okay -- RHSs are the same

+  a[i], a[i], a[i], a[i] := *, *, a[5], *;  // okay -- only one RHS is non-*

+  a[i], a[i], a[i], a[j] := *, a[i], a[j], a[i];  // error -- possible duplicate LHS

+}

+

+method S<T>(i: nat, j: nat)

+  requires i < 10 && j < 20;

+{

+  var a := new T[10,20];

+  a[i,j], a[i,i] := a[5,7], a[5,7];  // okay -- RHSs are the same

+  a[i,j], a[i,j], a[i,j], a[i,j] := *, *, a[5,7], *;  // okay -- only one RHS is non-*

+  a[i,j], a[i,j], a[i,j], a[i,i] := *, a[i,i], a[i,j], a[i,i];  // error -- possible duplicate LHS

+}

diff --git a/Test/dafny0/LhsDuplicates.dfy.expect b/Test/dafny0/LhsDuplicates.dfy.expect
new file mode 100644
index 00000000..a864390f
--- /dev/null
+++ b/Test/dafny0/LhsDuplicates.dfy.expect
@@ -0,0 +1,28 @@
+LhsDuplicates.dfy(18,10): Error: left-hand sides for different forall-statement bound variables may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon16_Else

+    (0,0): anon18_Else

+    (0,0): anon21_Then

+    (0,0): anon13

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon16_Else

+    (0,0): anon18_Else

+    (0,0): anon21_Then

+    (0,0): anon13

+LhsDuplicates.dfy(42,12): Error: when left-hand sides 1 and 3 refer to the same location, they must be assigned the same value

+Execution trace:

+    (0,0): anon0

+LhsDuplicates.dfy(51,18): Error: when left-hand sides 0 and 2 refer to the same location, they must be assigned the same value

+Execution trace:

+    (0,0): anon0

+LhsDuplicates.dfy(60,16): Error: when left-hand sides 1 and 2 may refer to the same location, they must be assigned the same value

+Execution trace:

+    (0,0): anon0

+LhsDuplicates.dfy(69,20): Error: when left-hand sides 1 and 2 refer to the same location, they must be assigned the same value

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 6 verified, 6 errors

diff --git a/Test/dafny0/RealTypes.dfy b/Test/dafny0/RealTypes.dfy
index 76ac9d93..1004a015 100644
--- a/Test/dafny0/RealTypes.dfy
+++ b/Test/dafny0/RealTypes.dfy
@@ -23,10 +23,10 @@ method R2(ghost x: real, ghost y: real) {
 

 // Check that literals are handled properly

 method R3() {

-  ghost var x := 1.5;

-  ghost var y := real(3);

-  assert x == y / 2.0000000;  

-  assert x == y / 2.000000000000000000000000001;  // error

+  ghost var x := 000_00_0_1.5_0_0_00_000_0;  // 1.5

+  ghost var y := real(000_000_003);  // 3

+  assert x == y / 2.000_000_0;

+  assert x == y / 2.000_000_000_000_000_000_000_000_001;  // error

 }

 

 // Check that real value in decreases clause doesn't scare Dafny

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 79e7ac57..e324393d 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1240,3 +1240,22 @@ module NonInferredTypeVariables {
      */

   }

 }

+

+// -------------- signature completion ------------------

+

+module SignatureCompletion {

+  // datatype signatures do not allow auto-declared type parameters on the LHS

+  datatype Dt = Ctor(X -> Dt)  // error: X is not a declared type

+  datatype Et<Y> = Ctor(X -> Et, Y)  // error: X is not a declared type

+

+  // For methods and functions, signatures can auto-declare type parameters

+  method My0(s: set, x: A -> B)

+  method My1(x: A -> B, s: set)

+  method My2<A,B>(s: set, x: A -> B)

+  method My3<A,B>(x: A -> B, s: set)

+

+  function F0(s: set, x: A -> B): int

+  function F1(x: A -> B, s: set): int

+  function F2<A,B>(s: set, x: A -> B): int

+  function F3<A,B>(x: A -> B, s: set): int

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 1b802687..3b768c84 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -83,6 +83,8 @@ ResolutionErrors.dfy(1220,26): Error: the type of this variable is underspecifie
 ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

+ResolutionErrors.dfy(1249,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

 ResolutionErrors.dfy(429,2): Error: More than one anonymous 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

@@ -180,4 +182,4 @@ ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-182 resolution/type errors detected in ResolutionErrors.dfy

+184 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy
new file mode 100644
index 00000000..d4c98424
--- /dev/null
+++ b/Test/dafny0/SeqFromArray.dfy
@@ -0,0 +1,90 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method Main() { }

+

+method H(a: array<int>, c: array<int>, n: nat, j: nat)

+  requires a != null && c != null

+  requires j < n == a.Length == c.Length

+{

+  var A := a[..];

+  var C := c[..];

+

+  if {

+    case A[j] == C[j] =>

+      assert a[j] == c[j];

+    case forall i :: 0 <= i < n ==> A[i] == C[i] =>

+      assert a[j] == c[j];

+    case forall i :: 0 <= i < n ==> A[i] == C[i] =>

+      assert forall i :: 0 <= i < n ==> a[i] == c[i];

+    case A == C =>

+      assert forall i :: 0 <= i < n ==> A[i] == C[i];

+    case A == C =>

+      assert forall i :: 0 <= i < n ==> a[i] == c[i];

+    case true =>

+  }

+}

+

+method K(a: array<int>, c: array<int>, n: nat)

+  requires a != null && c != null

+  requires n <= a.Length && n <= c.Length

+{

+  var A := a[..n];

+  var C := c[..n];

+  if {

+    case A == C =>

+      assert forall i :: 0 <= i < n ==> A[i] == C[i];

+    case A == C =>

+      assert forall i :: 0 <= i < n ==> a[i] == c[i];

+    case true =>

+  }

+}

+

+method L(a: array<int>, c: array<int>, n: nat)

+  requires a != null && c != null

+  requires n <= a.Length == c.Length

+{

+  var A := a[n..];

+  var C := c[n..];

+  var h := a.Length - n;

+  if {

+    case A == C =>

+      assert forall i :: 0 <= i < h ==> A[i] == C[i];

+    case A == C =>

+      assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i];

+    case true =>

+  }

+}

+

+method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)

+  requires a != null && c != null

+  requires k + m <= a.Length;

+  requires l + n <= c.Length

+{

+  if {

+    case true =>

+      var A := a[k..k+m];

+      var C := c[l..l+n];

+      if A == C {

+        if * {

+          assert m == n;

+        } else if * {

+          assert forall i :: 0 <= i < n ==> A[i] == C[i];

+        } else if * {

+          assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k];

+        } else if * {

+          assert forall i :: 0 <= i < n ==> A[i] == a[k+i];

+        } else if * {

+          assert forall i :: 0 <= i < n ==> C[i] == c[l+i];

+        } else if * {

+          assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];

+        }

+      } 

+    case l+k+m <= c.Length && forall i :: k <= i < k+m ==> a[i] == c[l+i] =>

+      assert a[k..k+m] == c[l+k..l+k+m];

+    case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>

+      assert a[..m] == c[l..l+m];

+    case l+a.Length <= c.Length && forall i :: k <= i < a.Length ==> a[i] == c[l+i] =>

+      assert a[k..] == c[l+k..l+a.Length];

+  }

+}

diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect
new file mode 100644
index 00000000..af845d3e
--- /dev/null
+++ b/Test/dafny0/SeqFromArray.dfy.expect
@@ -0,0 +1,5 @@
+

+Dafny program verifier finished with 10 verified, 0 errors

+Program compiled successfully

+Running...

+

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index d6658671..7d8628a9 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -432,10 +432,6 @@ class AttributeTests {
     ensures {:boolAttr false} true;

     ensures {:intAttr 0} true;

     ensures {:intAttr 1} true;

-    free ensures {:boolAttr true} true;

-    free ensures {:boolAttr false} true;

-    free ensures {:intAttr 0} true;

-    free ensures {:intAttr 1} true;

     modifies {:boolAttr true} this`f;

     modifies {:boolAttr false} this`f;

     modifies {:intAttr 0} this`f;

@@ -459,10 +455,6 @@ class AttributeTests {
       invariant {:boolAttr false} true;

       invariant {:intAttr 0} true;

       invariant {:intAttr 1} true;

-      free invariant {:boolAttr true} true;

-      free invariant {:boolAttr false} true;

-      free invariant {:intAttr 0} true;

-      free invariant {:intAttr 1} true;

       modifies {:boolAttr true} this`f;

       modifies {:boolAttr false} this`f;

       modifies {:intAttr 0} this`f;

@@ -505,6 +497,15 @@ class AttributeTests {
     } else {

       return new AttributeTests.C() {:intAttr 0};

     }

+

+    // forall statements resolve their attributes once the bound variables have been

+    // added to the scope

+    var y: bool, x: real;

+    var aa := new real[120];

+    forall y: int, x, z {:trgr x == y} {:tri z == z} | x < y  // the range will infer the type of x

+      ensures z && 0 <= x < aa.Length ==> aa[x] == 0.0;  // ensures clause will infer type of z

+    {

+    }

   }

 }

 

@@ -512,10 +513,10 @@ class AttributeTests {
 

 static method TestAttributesVarDecls()

 {

-  var {:foo} foo := null;

-  var {:bar} bar := 0;

-  var {:foo} {:bar} foobar : set<int> := {};

-  var {:baz} baz, {:foobaz} foobaz := true, false;

+  var {:foo foo} foo := null;

+  var {:bar bar} bar := 0;

+  var {:foo foobar} {:bar foobar} foobar : set<int> := {};

+  var {:baz baz && foobaz} baz, {:foobaz foobaz != baz} foobaz := true, false;

 }

 

 // ----------------------- Pretty printing of !(!expr) --------

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 1e71ec8b..824ad991 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -94,14 +94,14 @@ SmallTests.dfy(385,6): Error: cannot prove termination; try supplying a decrease
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(689,14): Error: assertion violation

+SmallTests.dfy(690,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(686,5): anon7_LoopHead

+    SmallTests.dfy(687,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    SmallTests.dfy(686,5): anon8_Else

+    SmallTests.dfy(687,5): anon8_Else

     (0,0): anon9_Then

-SmallTests.dfy(710,14): Error: assertion violation

+SmallTests.dfy(711,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

@@ -133,12 +133,12 @@ SmallTests.dfy(400,41): Related location: This is the postcondition that might n
 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-SmallTests.dfy(560,12): Error: assertion violation

+SmallTests.dfy(561,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-SmallTests.dfy(574,20): Error: left-hand sides 0 and 1 may refer to the same location

+SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -150,11 +150,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-SmallTests.dfy(576,15): Error: left-hand sides 1 and 2 may refer to the same location

+SmallTests.dfy(577,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(569,18): anon28_Else

+    SmallTests.dfy(570,18): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon30_Then

@@ -165,16 +165,16 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(583,25): Error: target object may be null

+SmallTests.dfy(584,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(596,10): Error: assertion violation

+SmallTests.dfy(597,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(620,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(643,10): Error: assertion violation

+SmallTests.dfy(644,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -182,17 +182,17 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-SmallTests.dfy(657,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(658,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(659,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(660,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(672,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(673,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 900b6110..aa3d7671 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -335,7 +335,7 @@ module ArrayTypeMagic {
     return b[..];

   }

 

-  datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)

+  datatype ArrayCubeTree<T> = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)

   datatype AnotherACT<T> = Leaf(array3) | Node(AnotherACT, AnotherACT)

   datatype OneMoreACT<T,U> = Leaf(array3) | Node(OneMoreACT, OneMoreACT)

 

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 6086fcf1..141e48cb 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -144,3 +144,28 @@ ghost method GhostM() returns (x: int)
 {

   x :| true;  // no problem (but there once was a problem with this case, where an error was generated for no reason)

 }

+

+// ------------------ cycles that could arise from proxy assignments ---------

+

+module ProxyCycles {

+  datatype Dt<X> = Ctor(X -> Dt<X>)

+  method M0()

+  {

+    var dt: Dt<int>;

+    var f := x => x;

+    dt := Ctor(f);  // error: cannot infer a type for f

+  }

+  method M1()

+  {

+    var dt: Dt;

+    var f := x => x;

+    dt := Ctor(f);  // error: cannot infer a type for f

+  }

+

+  function method F<X>(x: X): set<X>

+  method N()

+  {

+    var x;

+    x := F(x);  // error: cannot infer type for x

+  }

+}

diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 5d78fe16..55fc916c 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -1,3 +1,6 @@
+TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

+TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

+TypeTests.dfy(169,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)

 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)

@@ -31,4 +34,4 @@ TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification
 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

+36 resolution/type errors detected in TypeTests.dfy

diff --git a/Test/dafny4/BinarySearch.dfy b/Test/dafny4/BinarySearch.dfy
index a06f6c4a..b11fc0d1 100644
--- a/Test/dafny4/BinarySearch.dfy
+++ b/Test/dafny4/BinarySearch.dfy
@@ -4,15 +4,15 @@
 // Binary search using standard integers

 

 method BinarySearch(a: array<int>, key: int) returns (r: int)

-  requires a != null;

-  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

-  ensures 0 <= r ==> r < a.Length && a[r] == key;

-  ensures r < 0 ==> key !in a[..];

+  requires a != null

+  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]

+  ensures 0 <= r ==> r < a.Length && a[r] == key

+  ensures r < 0 ==> key !in a[..]

 {

   var lo, hi := 0, a.Length;

   while lo < hi

-    invariant 0 <= lo <= hi <= a.Length;

-    invariant key !in a[..lo] && key !in a[hi..];

+    invariant 0 <= lo <= hi <= a.Length

+    invariant key !in a[..lo] && key !in a[hi..]

   {

     var mid := (lo + hi) / 2;

     if key < a[mid] {

@@ -28,18 +28,18 @@ method BinarySearch(a: array<int>, key: int) returns (r: int)
 

 // Binary search using bounded integers

 

-newtype int32 = x | -0x80000000 <= x < 0x80000000

+newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000

 

 method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32)

-  requires a != null && a.Length < 0x80000000;

-  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

-  ensures 0 <= r ==> r < int32(a.Length) && a[r] == key;

-  ensures r < 0 ==> key !in a[..];

+  requires a != null && a.Length < 0x8000_0000

+  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]

+  ensures 0 <= r ==> r < int32(a.Length) && a[r] == key

+  ensures r < 0 ==> key !in a[..]

 {

   var lo, hi := 0, int32(a.Length);

   while lo < hi

-    invariant 0 <= lo <= hi <= int32(a.Length);

-    invariant key !in a[..lo] && key !in a[hi..];

+    invariant 0 <= lo <= hi <= int32(a.Length)

+    invariant key !in a[..lo] && key !in a[hi..]

   {

     var mid := (lo + hi) / 2;  // error: possible overflow

     if key < a[mid] {

@@ -54,15 +54,15 @@ method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32)
 }

 

 method BinarySearchInt32_good(a: array<int>, key: int) returns (r: int32)

-  requires a != null && a.Length < 0x80000000;

-  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

-  ensures 0 <= r ==> r < int32(a.Length) && a[r] == key;

-  ensures r < 0 ==> key !in a[..];

+  requires a != null && a.Length < 0x8000_0000

+  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]

+  ensures 0 <= r ==> r < int32(a.Length) && a[r] == key

+  ensures r < 0 ==> key !in a[..]

 {

   var lo, hi := 0, int32(a.Length);

   while lo < hi

-    invariant 0 <= lo <= hi <= int32(a.Length);

-    invariant key !in a[..lo] && key !in a[hi..];

+    invariant 0 <= lo <= hi <= int32(a.Length)

+    invariant key !in a[..lo] && key !in a[hi..]

   {

     var mid := lo + (hi - lo) / 2;  // this is how to do it

     if key < a[mid] {

diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy
index 7ce99e56..50b5569b 100644
--- a/Test/hofs/Fold.dfy
+++ b/Test/hofs/Fold.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:3 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-datatype List = Nil | Cons(A,List<A>);
+datatype List<A> = Nil | Cons(A,List<A>);
 
 datatype Expr = Add(List<Expr>) | Mul(List<Expr>) | Lit(int);