22 files changed, 862 insertions, 822 deletions
diff --git a/Test/test1/Arrays.bpl b/Test/test1/Arrays.bpl
index cb21e4ed..2013a69c 100644
--- a/Test/test1/Arrays.bpl
+++ b/Test/test1/Arrays.bpl
@@ -1,226 +1,226 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var one: [int]int;
-var two: [int, int]int;
-
-procedure Good0(x: int, y: int)
-  requires one[x] == two[x,y];
-  modifies one, two;
-{
-  start:
-    one[x] := two[x,y];
-    two[x,y] := one[x];
-    return;
-}
-
-procedure Bad0(x: int, y: int)
-  requires one[x,y] == 7;
-  requires two[x] == 8;
-  modifies one, two;
-{
-  start:
-    one[x,y] := 10;
-    two[x] := 11;
-    return;
-}
-
-var A: [int]bool;
-var B: [bool, ref]int;
-
-procedure Good1(x: int, b: bool, o: ref)
-  requires A[x] && B[b,o] == 18;
-  modifies A, B;
-{
-  start:
-    A[x] := true;
-    B[b,o] := 19;
-    A[100] := false;
-    B[false,null] := 70;
-    return;
-}
-
-procedure Bad1(x: int, b: bool, o: ref)
-  requires A[b];
-  requires A[x] == 7;
-  requires B[x,x] < 12;
-  requires B[b,b] == B[o,o];
-  requires B[null,5];
-  requires B[7,7] == A[7];
-  modifies A, B;
-{
-  start:
-    A[b] := true;
-    B[3,14] := null;
-    A[A[x]] := 9;
-    B[false,false] := 70;
-    return;
-}
-
-var M: [ [int,int]bool, [name]name ]int;
-var Q: [int,int][int]int;
-var R: [int][int,int]int;
-
-procedure Good2(k: [int,int]bool, l: [name]name) returns (n: int)
-  modifies M, Q, R;
-{
-  var m: [ [int,int]bool, [name]name ]int;
-  var p: [int,int]bool;
-  var q: [int]int;
-  var qq: [int,int][int]int;
-  var r: [int,int]int;
-
-  start:
-    n := M[k,l];
-    m := M;
-    p := k;
-    p[5,8] := true;
-    m[p,l] := 13;
-    M := m;
-    goto next;
-
-  next:
-    qq := Q;
-    q := Q[13,21];
-    n := n + Q[34,55][89];
-    R[1] := R[2];
-    n := n + R[1][2,3];
-    Q[144,233] := q;
-    goto deepUpdate;
-
-  deepUpdate:
-    // To effectively do:
-    //     Q[5,8][13] := 21;
-    // do:
-    q := Q[5,8];
-    q[13] := 21;
-    Q[5,8] := q;
-    return;
-}
-
-const Sven: name;
-const Mia: name;
-const Tryggve: name;
-const Gunnel: name;
-
-procedure Bad2(k: [int,int]bool, l: [name]name) returns (n: int)
-  modifies M, Q, R;
-{
-  var m: [ [int,int]bool, [name]name ]int;
-  var p: [int,int]bool;
-  var q: [int]int;
-  var qq: [int,int][int]int;
-  var qqx: [int,int][name]int;
-
-  start:
-    n := M[Sven,l];
-    m := p;
-    p := l[Mia];
-    p[5,8] := Tryggve;
-    m[p,Gunnel] := 13;
-    M := qq;
-    goto next;
-
-  next:
-    qq := Q;  // okay
-    q := Q[13];
-    n := n - Q[89][34,55];
-    Q[true,233] := q;
-    qqx := qq;
-    Q := qqx;
-    qqx := qqx;  // okay
-    Q := Q;  // okay
-    n := n + Q[34,55][144,169];
-    R[1,2] := 0;
-    R[1] := R[2,3];
-    n := n + R[1][2];
-    n := n + R[1,2];
-    return;
-}
-
-type MyType;
-var S0: bool;
-var S1: [ref]bool;
-var S2: [ref,int]bool;
-var S3: [[ref,int]bool,MyType]MyType;
-var S4: <a>[int,a]bool;
-var S5: [int,int]bool;
-var S6: [any,any]bool;
-var S7: [int,any]any;
-var S8: [any]bool;
-
-function Sf(any) returns (bool);
-
-procedure SubtypesGood(a: any)
-  modifies S0;
-{
-  var t: MyType;
-  var b: bool;
-
-  start:
-    S0 := S1[null];  // bool := bool
-    S0 := S2[null,0];  // bool := bool
-    t := S3[S2,t];
-    goto next;
-  next:
-    b := S4[4,a];
-    b := S4[5,null];  // any := ref
-    b := S4[6,S4];  // any := [int,any]bool
-    b := Sf(S5);
-    return;
-}
-
-procedure SubtypesBad()
-  modifies S4,S5,S6;
-  modifies S8;
-{
-  start:
-    S4 := S4;
-    S4 := S5;  // no
-    S5 := S4;  // no
-    S4 := S6;  // no
-    S6 := S4;  // no
-    S8 := S1;  // no
-    return;
-}
-
-// ----------------------------------------------------
-
-var ArrayA: [int]bool;
-var ArrayB: <a>[a]bool;
-
-procedure ArrayP(x: int, y: any)
-  requires ArrayA[x];
-  requires ArrayA[y];  // error
-  requires ArrayB[x];
-  requires ArrayB[y];
-  modifies ArrayA, ArrayB;
-{
-  start:
-    ArrayA[x] := true;
-    ArrayA[y] := true;  // error
-    ArrayB[x] := true;
-    ArrayB[y] := true;
-    return;
-}
-
-// ----------------------------------------------------
-
-procedure IntMethod(p: any) returns (r: int);
-procedure AnyMethod(p: int) returns (r: any);
-
-procedure IntMethodCaller()
-{
-  var x: any, y: int;
-  entry:
-    call x := AnyMethod(y);  // types are exact
-    call x := IntMethod(y);  // error: type mismatch for out-parameter
-    x := y;
-    y := x;  // error: cannot assign any to int
-    call y := IntMethod(x);  // types are exact
-    call y := AnyMethod(x);  // type error on both in-parameter and out-parameter
-    return;
-}
-
-
-type ref, any, name;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var one: [int]int;
+var two: [int, int]int;
+
+procedure Good0(x: int, y: int)
+  requires one[x] == two[x,y];
+  modifies one, two;
+{
+  start:
+    one[x] := two[x,y];
+    two[x,y] := one[x];
+    return;
+}
+
+procedure Bad0(x: int, y: int)
+  requires one[x,y] == 7;
+  requires two[x] == 8;
+  modifies one, two;
+{
+  start:
+    one[x,y] := 10;
+    two[x] := 11;
+    return;
+}
+
+var A: [int]bool;
+var B: [bool, ref]int;
+
+procedure Good1(x: int, b: bool, o: ref)
+  requires A[x] && B[b,o] == 18;
+  modifies A, B;
+{
+  start:
+    A[x] := true;
+    B[b,o] := 19;
+    A[100] := false;
+    B[false,null] := 70;
+    return;
+}
+
+procedure Bad1(x: int, b: bool, o: ref)
+  requires A[b];
+  requires A[x] == 7;
+  requires B[x,x] < 12;
+  requires B[b,b] == B[o,o];
+  requires B[null,5];
+  requires B[7,7] == A[7];
+  modifies A, B;
+{
+  start:
+    A[b] := true;
+    B[3,14] := null;
+    A[A[x]] := 9;
+    B[false,false] := 70;
+    return;
+}
+
+var M: [ [int,int]bool, [name]name ]int;
+var Q: [int,int][int]int;
+var R: [int][int,int]int;
+
+procedure Good2(k: [int,int]bool, l: [name]name) returns (n: int)
+  modifies M, Q, R;
+{
+  var m: [ [int,int]bool, [name]name ]int;
+  var p: [int,int]bool;
+  var q: [int]int;
+  var qq: [int,int][int]int;
+  var r: [int,int]int;
+
+  start:
+    n := M[k,l];
+    m := M;
+    p := k;
+    p[5,8] := true;
+    m[p,l] := 13;
+    M := m;
+    goto next;
+
+  next:
+    qq := Q;
+    q := Q[13,21];
+    n := n + Q[34,55][89];
+    R[1] := R[2];
+    n := n + R[1][2,3];
+    Q[144,233] := q;
+    goto deepUpdate;
+
+  deepUpdate:
+    // To effectively do:
+    //     Q[5,8][13] := 21;
+    // do:
+    q := Q[5,8];
+    q[13] := 21;
+    Q[5,8] := q;
+    return;
+}
+
+const Sven: name;
+const Mia: name;
+const Tryggve: name;
+const Gunnel: name;
+
+procedure Bad2(k: [int,int]bool, l: [name]name) returns (n: int)
+  modifies M, Q, R;
+{
+  var m: [ [int,int]bool, [name]name ]int;
+  var p: [int,int]bool;
+  var q: [int]int;
+  var qq: [int,int][int]int;
+  var qqx: [int,int][name]int;
+
+  start:
+    n := M[Sven,l];
+    m := p;
+    p := l[Mia];
+    p[5,8] := Tryggve;
+    m[p,Gunnel] := 13;
+    M := qq;
+    goto next;
+
+  next:
+    qq := Q;  // okay
+    q := Q[13];
+    n := n - Q[89][34,55];
+    Q[true,233] := q;
+    qqx := qq;
+    Q := qqx;
+    qqx := qqx;  // okay
+    Q := Q;  // okay
+    n := n + Q[34,55][144,169];
+    R[1,2] := 0;
+    R[1] := R[2,3];
+    n := n + R[1][2];
+    n := n + R[1,2];
+    return;
+}
+
+type MyType;
+var S0: bool;
+var S1: [ref]bool;
+var S2: [ref,int]bool;
+var S3: [[ref,int]bool,MyType]MyType;
+var S4: <a>[int,a]bool;
+var S5: [int,int]bool;
+var S6: [any,any]bool;
+var S7: [int,any]any;
+var S8: [any]bool;
+
+function Sf(any) returns (bool);
+
+procedure SubtypesGood(a: any)
+  modifies S0;
+{
+  var t: MyType;
+  var b: bool;
+
+  start:
+    S0 := S1[null];  // bool := bool
+    S0 := S2[null,0];  // bool := bool
+    t := S3[S2,t];
+    goto next;
+  next:
+    b := S4[4,a];
+    b := S4[5,null];  // any := ref
+    b := S4[6,S4];  // any := [int,any]bool
+    b := Sf(S5);
+    return;
+}
+
+procedure SubtypesBad()
+  modifies S4,S5,S6;
+  modifies S8;
+{
+  start:
+    S4 := S4;
+    S4 := S5;  // no
+    S5 := S4;  // no
+    S4 := S6;  // no
+    S6 := S4;  // no
+    S8 := S1;  // no
+    return;
+}
+
+// ----------------------------------------------------
+
+var ArrayA: [int]bool;
+var ArrayB: <a>[a]bool;
+
+procedure ArrayP(x: int, y: any)
+  requires ArrayA[x];
+  requires ArrayA[y];  // error
+  requires ArrayB[x];
+  requires ArrayB[y];
+  modifies ArrayA, ArrayB;
+{
+  start:
+    ArrayA[x] := true;
+    ArrayA[y] := true;  // error
+    ArrayB[x] := true;
+    ArrayB[y] := true;
+    return;
+}
+
+// ----------------------------------------------------
+
+procedure IntMethod(p: any) returns (r: int);
+procedure AnyMethod(p: int) returns (r: any);
+
+procedure IntMethodCaller()
+{
+  var x: any, y: int;
+  entry:
+    call x := AnyMethod(y);  // types are exact
+    call x := IntMethod(y);  // error: type mismatch for out-parameter
+    x := y;
+    y := x;  // error: cannot assign any to int
+    call y := IntMethod(x);  // types are exact
+    call y := AnyMethod(x);  // type error on both in-parameter and out-parameter
+    return;
+}
+
+
+type ref, any, name;
+const null : ref;
diff --git a/Test/test1/AssertVerifiedUnder0.bpl b/Test/test1/AssertVerifiedUnder0.bpl
new file mode 100644
index 00000000..e419a5ef
--- /dev/null
+++ b/Test/test1/AssertVerifiedUnder0.bpl
@@ -0,0 +1,8 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+    assert {:verified_under 4} true;
+    assert {:verified_under 3.0} true;
+}
diff --git a/Test/test1/AssertVerifiedUnder0.bpl.expect b/Test/test1/AssertVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..6d3c04cd
--- /dev/null
+++ b/Test/test1/AssertVerifiedUnder0.bpl.expect
@@ -0,0 +1,3 @@
+AssertVerifiedUnder0.bpl(6,11): Error: attribute :verified_under accepts only one argument of type bool
+AssertVerifiedUnder0.bpl(7,11): Error: attribute :verified_under accepts only one argument of type bool
+2 type checking errors detected in AssertVerifiedUnder0.bpl
diff --git a/Test/test1/AssumptionVariables0.bpl b/Test/test1/AssumptionVariables0.bpl
index 7046ea59..7ebd3d24 100644
--- a/Test/test1/AssumptionVariables0.bpl
+++ b/Test/test1/AssumptionVariables0.bpl
@@ -1,57 +1,57 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure Test0()
-{
-    var {:assumption} a0: bool where a0;  // error
-}
-
-
-procedure Test1()
-{
-    var {:assumption} a0: bool;
-
-    a0 := a0 && true;
-}
-
-
-procedure Test2()
-{
-    var {:assumption} a0: bool;
-
-    a0 := true;  // error
-}
-
-
-procedure Test3()
-{
-    var {:assumption} a0: bool;
-    var {:assumption} a1: bool;
-
-    a0 := a1 && true;  // error
-}
-
-
-procedure Test4()
-{
-    var {:assumption} a0: bool;
-
-    a0 := a0 && true;
-    a0 := a0 && true;  // error
-}
-
-
-procedure Test5()
-  modifies a0;
-{
-    a0 := a0 && true;
-}
-
-
-var {:assumption} a0: bool;
-
-
-procedure Test6()
-  modifies a0;
-{
-    a0 := a0 && true;  // error
-}
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure Test0()
+{
+    var {:assumption} a0: bool where a0;  // error
+}
+
+
+procedure Test1()
+{
+    var {:assumption} a0: bool;
+
+    a0 := a0 && true;
+}
+
+
+procedure Test2()
+{
+    var {:assumption} a0: bool;
+
+    a0 := true;  // error
+}
+
+
+procedure Test3()
+{
+    var {:assumption} a0: bool;
+    var {:assumption} a1: bool;
+
+    a0 := a1 && true;  // error
+}
+
+
+procedure Test4()
+{
+    var {:assumption} a0: bool;
+
+    a0 := a0 && true;
+    a0 := a0 && true;  // error
+}
+
+
+procedure Test5()
+  modifies a0;
+{
+    a0 := a0 && true;
+}
+
+
+var {:assumption} a0: bool;
+
+
+procedure Test6()
+  modifies a0;
+{
+    a0 := a0 && true;  // error
+}
diff --git a/Test/test1/AssumptionVariables1.bpl b/Test/test1/AssumptionVariables1.bpl
index 3125650c..918a9b63 100644
--- a/Test/test1/AssumptionVariables1.bpl
+++ b/Test/test1/AssumptionVariables1.bpl
@@ -1,6 +1,6 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure Test0()
-{
-    var {:assumption} a0: int;  // error
-}
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure Test0()
+{
+    var {:assumption} a0: int;  // error
+}
diff --git a/Test/test1/AssumptionVariables1.bpl.expect b/Test/test1/AssumptionVariables1.bpl.expect
index 9e894bf9..badc18b3 100644
--- a/Test/test1/AssumptionVariables1.bpl.expect
+++ b/Test/test1/AssumptionVariables1.bpl.expect
@@ -1,2 +1,2 @@
-AssumptionVariables1.bpl(5,22): Error: assumption variable must be of type 'bool'
-1 type checking errors detected in AssumptionVariables1.bpl
+AssumptionVariables1.bpl(5,22): Error: assumption variable must be of type 'bool'
+1 type checking errors detected in AssumptionVariables1.bpl
diff --git a/Test/test1/AttributeTyping.bpl b/Test/test1/AttributeTyping.bpl
index bcd98feb..713f464c 100644
--- a/Test/test1/AttributeTyping.bpl
+++ b/Test/test1/AttributeTyping.bpl
@@ -1,38 +1,38 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-
-const {:Incorrect pux0 ++ F0(pux1)} pux0: int;
-
-function {:Incorrect F0(pux0 < 0) + pux1} F0(int) returns (int);
-
-axiom {:Incorrect F0(pux0 == pux1)} true;
-
-var {:Incorrect pux0 && pux1} pux1: int;
-
-procedure {:Incorrect !(pux0 - pux1)} P();
-
-implementation {:Incorrect pux0 ==> pux1} P()
-{
-}
-
-// ------  and here are various correct things
-
-
-
-const {:Correct hux0 + F1(hux1)} hux0: int;
-
-function {:Correct F1(hux0) + hux1} F1(int) returns (int);
-
-axiom {:Correct F1(hux0 + hux1)} true;
-
-var {:Correct hux0*hux1} hux1: int;
-
-procedure {:Correct hux0 - hux1} H();
-
-implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} H()
-{
-}
-
-
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+const {:Incorrect pux0 ++ F0(pux1)} pux0: int;
+
+function {:Incorrect F0(pux0 < 0) + pux1} F0(int) returns (int);
+
+axiom {:Incorrect F0(pux0 == pux1)} true;
+
+var {:Incorrect pux0 && pux1} pux1: int;
+
+procedure {:Incorrect !(pux0 - pux1)} P();
+
+implementation {:Incorrect pux0 ==> pux1} P()
+{
+}
+
+// ------  and here are various correct things
+
+
+
+const {:Correct hux0 + F1(hux1)} hux0: int;
+
+function {:Correct F1(hux0) + hux1} F1(int) returns (int);
+
+axiom {:Correct F1(hux0 + hux1)} true;
+
+var {:Correct hux0*hux1} hux1: int;
+
+procedure {:Correct hux0 - hux1} H();
+
+implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} H()
+{
+}
+
+
 type any;
 \ No newline at end of file
diff --git a/Test/test1/EmptyCallArgs.bpl b/Test/test1/EmptyCallArgs.bpl
index 8f5ae31f..3c2aa177 100644
--- a/Test/test1/EmptyCallArgs.bpl
+++ b/Test/test1/EmptyCallArgs.bpl
@@ -1,22 +1,22 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type C;
-
-procedure P(x:int, y:bool) returns (z:C);
-procedure Q<a>(x:int, y:a) returns (z:a);
-
-procedure CallP() {
-  var x:int;
-  var y:bool;
-  var z:C;
-
-  call z := P(x, y);
-}
-
-procedure CallQ() {
-  var x:int;
-  var y:bool;
-  var z:bool;
-
-  call x := Q(x, y);   // type error
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type C;
+
+procedure P(x:int, y:bool) returns (z:C);
+procedure Q<a>(x:int, y:a) returns (z:a);
+
+procedure CallP() {
+  var x:int;
+  var y:bool;
+  var z:C;
+
+  call z := P(x, y);
+}
+
+procedure CallQ() {
+  var x:int;
+  var y:bool;
+  var z:bool;
+
+  call x := Q(x, y);   // type error
 }
 \ No newline at end of file
diff --git a/Test/test1/Family.bpl b/Test/test1/Family.bpl
index fec96332..0ec5fb20 100644
--- a/Test/test1/Family.bpl
+++ b/Test/test1/Family.bpl
@@ -1,49 +1,49 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type T;
-
-var Heap: <x>[ref,Field x]x;
-
-function IsHeap(<x>[ref,Field x]x) returns (bool);
-
-const alloc: Field bool;
-const C.x: Field int;
-
-axiom (forall h: <x>[ref,Field x]x, f: Field ref, o: ref :: IsHeap(h) && o != null ==> h[h[o,f], alloc]);
-
-procedure P(this: ref) returns (r: int)
-  modifies Heap;
-{
-  start:
-    r := Heap[this, C.x];
-    Heap[this, C.x] := r;
-    return;
-}
-
-// -----------------
-
-procedure R(this: ref)
-  modifies Heap;
-{
-  var field: any, refField: Field ref, yField: Field y, anyField: Field any;
-  var b: bool, a: any;
-
-  start:
-    b := Heap[this, C.x];     // type error
-    Heap[this, C.x] := true;  // type error
-    Heap[this, refField] := this;
-    Heap[this, yField] := 2;  // type error
-    Heap[this, field] := a;   // type error
-    Heap[this, field] := b;   // type error
-    Heap[this, anyField] := a;
-    Heap[this, anyField] := b;
-    Heap[this, anyField] := anyField;
-    Heap[this, anyField] := yField;
-    Heap[this, anyField] := field;
-    return;
-}
-
-type Field a;
-type y;
-type ref, any;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type T;
+
+var Heap: <x>[ref,Field x]x;
+
+function IsHeap(<x>[ref,Field x]x) returns (bool);
+
+const alloc: Field bool;
+const C.x: Field int;
+
+axiom (forall h: <x>[ref,Field x]x, f: Field ref, o: ref :: IsHeap(h) && o != null ==> h[h[o,f], alloc]);
+
+procedure P(this: ref) returns (r: int)
+  modifies Heap;
+{
+  start:
+    r := Heap[this, C.x];
+    Heap[this, C.x] := r;
+    return;
+}
+
+// -----------------
+
+procedure R(this: ref)
+  modifies Heap;
+{
+  var field: any, refField: Field ref, yField: Field y, anyField: Field any;
+  var b: bool, a: any;
+
+  start:
+    b := Heap[this, C.x];     // type error
+    Heap[this, C.x] := true;  // type error
+    Heap[this, refField] := this;
+    Heap[this, yField] := 2;  // type error
+    Heap[this, field] := a;   // type error
+    Heap[this, field] := b;   // type error
+    Heap[this, anyField] := a;
+    Heap[this, anyField] := b;
+    Heap[this, anyField] := anyField;
+    Heap[this, anyField] := yField;
+    Heap[this, anyField] := field;
+    return;
+}
+
+type Field a;
+type y;
+type ref, any;
+const null : ref;
diff --git a/Test/test1/Frame0.bpl b/Test/test1/Frame0.bpl
index 6155fc27..a3ef6138 100644
--- a/Test/test1/Frame0.bpl
+++ b/Test/test1/Frame0.bpl
@@ -1,17 +1,17 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g0: int;
-var g1: int;
-
-var h0: [ref, name]any;
-var h1: [ref, name]any;
-
-const X: name;
-
-procedure P(a: ref, hh: [ref, name]any) returns (b: int, hout: [ref, name]any);
-  modifies a;  // in-parameters are not mutable
-  modifies h1, g0;
-  modifies b;  // out-parameters are not allowed explicitly in modifies clause
-
-
-type ref, name, any;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g0: int;
+var g1: int;
+
+var h0: [ref, name]any;
+var h1: [ref, name]any;
+
+const X: name;
+
+procedure P(a: ref, hh: [ref, name]any) returns (b: int, hout: [ref, name]any);
+  modifies a;  // in-parameters are not mutable
+  modifies h1, g0;
+  modifies b;  // out-parameters are not allowed explicitly in modifies clause
+
+
+type ref, name, any;
diff --git a/Test/test1/Frame1.bpl b/Test/test1/Frame1.bpl
index 2ec70270..5e637660 100644
--- a/Test/test1/Frame1.bpl
+++ b/Test/test1/Frame1.bpl
@@ -1,99 +1,99 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g0: int;
-var g1: int;
-
-var h0: [ref, name]int;
-var h1: [ref, name]int;
-
-const X: name;
-
-procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);
-  modifies h1, g0;
-
-implementation P(a: ref, hh: [ref, name]int)
-               returns (b: int, hout: [ref, name]any) {
-  start:
-    g0 := 5;
-    g1 := 6;  // error: g1 is not in modifies clause
-    a := null;  // error: in-parameters are not mutable 
-    b := 12;
-    goto next;
-  next:
-    havoc g0;
-    havoc g1;  // error: g1 is not in modifies clause
-    havoc a;  // error: in-parameters are not mutable
-    havoc b;
-    goto more;
-  more:
-    hh[a,X] := 101;  // error: in-parameter (hh) is not mutable
-    h0[a,X] := 102;  // error: h0 is not in modifies clause
-    h1[a,X] := 103;
-    hh := h0;  // error: in-parameter is not mutable
-    h0 := h1;  // error: h0 is not in modifies clause
-    h1 := hh;
-    havoc hh;  // error: in-parameter is not mutable
-    havoc h0;  // error: h0 is not in modifies clause
-    havoc h1;
-    return;
-}
-
-procedure PX();
-  modifies h1, g0;
-
-procedure PY()
-  modifies h1, g0;
-{
-  start:
-    call PX();
-    call PY();
-    return;
-}
-
-procedure PZ()
-  modifies h1;
-{
-  start:
-    call PX();  // error: PX has larger frame than PZ
-    return;
-}
-
-procedure Q() returns (x: int, y: int, h: [ref, name]int)
-{
-  start:
-    return;
-}
-
-procedure QCallerBad()
-{
-  start:
-    call g0, g1, h0 := Q();
-    return;
-}
-
-procedure QCallerGood()
-  modifies g0, h0;
-{
-  var t: int;
-
-  start:
-    call t, g0, h0 := Q();
-    return;
-}
-
-procedure MismatchedTypes(x: int);
-
-implementation MismatchedTypes(x: bool)  // error
-{
-  start:
-    return;
-}
-implementation MismatchedTypes(y: bool)  // error (this time with a different name for the formal)
-{
-  start:
-    return;
-}
-
-
-type ref, name, any;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g0: int;
+var g1: int;
+
+var h0: [ref, name]int;
+var h1: [ref, name]int;
+
+const X: name;
+
+procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);
+  modifies h1, g0;
+
+implementation P(a: ref, hh: [ref, name]int)
+               returns (b: int, hout: [ref, name]any) {
+  start:
+    g0 := 5;
+    g1 := 6;  // error: g1 is not in modifies clause
+    a := null;  // error: in-parameters are not mutable 
+    b := 12;
+    goto next;
+  next:
+    havoc g0;
+    havoc g1;  // error: g1 is not in modifies clause
+    havoc a;  // error: in-parameters are not mutable
+    havoc b;
+    goto more;
+  more:
+    hh[a,X] := 101;  // error: in-parameter (hh) is not mutable
+    h0[a,X] := 102;  // error: h0 is not in modifies clause
+    h1[a,X] := 103;
+    hh := h0;  // error: in-parameter is not mutable
+    h0 := h1;  // error: h0 is not in modifies clause
+    h1 := hh;
+    havoc hh;  // error: in-parameter is not mutable
+    havoc h0;  // error: h0 is not in modifies clause
+    havoc h1;
+    return;
+}
+
+procedure PX();
+  modifies h1, g0;
+
+procedure PY()
+  modifies h1, g0;
+{
+  start:
+    call PX();
+    call PY();
+    return;
+}
+
+procedure PZ()
+  modifies h1;
+{
+  start:
+    call PX();  // error: PX has larger frame than PZ
+    return;
+}
+
+procedure Q() returns (x: int, y: int, h: [ref, name]int)
+{
+  start:
+    return;
+}
+
+procedure QCallerBad()
+{
+  start:
+    call g0, g1, h0 := Q();
+    return;
+}
+
+procedure QCallerGood()
+  modifies g0, h0;
+{
+  var t: int;
+
+  start:
+    call t, g0, h0 := Q();
+    return;
+}
+
+procedure MismatchedTypes(x: int);
+
+implementation MismatchedTypes(x: bool)  // error
+{
+  start:
+    return;
+}
+implementation MismatchedTypes(y: bool)  // error (this time with a different name for the formal)
+{
+  start:
+    return;
+}
+
+
+type ref, name, any;
+const null : ref;
diff --git a/Test/test1/FunBody.bpl b/Test/test1/FunBody.bpl
index fc566681..caaf06f5 100644
--- a/Test/test1/FunBody.bpl
+++ b/Test/test1/FunBody.bpl
@@ -1,15 +1,15 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-function g0<beta>(x:beta) returns (beta);
-function g1<beta>() returns (beta);
-
-function {:inline true} f1() returns (int) { 13 }
-function {:inline true} f2() returns (int) { true }                  // wrong type
-function {:inline true} f3<alpha>(x:alpha) returns (alpha) { g0(x) }
-function {:inline true} f4<alpha>(x:alpha) returns (alpha) { g0(5) } // wrong type
-function {:inline true} f5<alpha>() returns (alpha) { g1() }
-function {:inline true} f6<alpha>() returns (alpha) { g1():int }     // wrong type
-
-
-
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function g0<beta>(x:beta) returns (beta);
+function g1<beta>() returns (beta);
+
+function {:inline true} f1() returns (int) { 13 }
+function {:inline true} f2() returns (int) { true }                  // wrong type
+function {:inline true} f3<alpha>(x:alpha) returns (alpha) { g0(x) }
+function {:inline true} f4<alpha>(x:alpha) returns (alpha) { g0(5) } // wrong type
+function {:inline true} f5<alpha>() returns (alpha) { g1() }
+function {:inline true} f6<alpha>() returns (alpha) { g1():int }     // wrong type
+
+
+
diff --git a/Test/test1/IfThenElse0.bpl b/Test/test1/IfThenElse0.bpl
index 19918827..65ae65f6 100644
--- a/Test/test1/IfThenElse0.bpl
+++ b/Test/test1/IfThenElse0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
 procedure foo()
 {
   var b:bool, i:int;
diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl
index 962aadf3..7b3d77e5 100644
--- a/Test/test1/IntReal.bpl
+++ b/Test/test1/IntReal.bpl
@@ -1,50 +1,50 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const i: int;
-const r: real;
-
-axiom i == 0;
-axiom i >= 0.0;                // type error
-axiom i <= 0.0e0;              // type error
-axiom i < 0.0e-0;              // type error
-axiom i > 0.0e20;              // type error
-
-axiom -i == r;                 // type error
-axiom i + r == 0.0;            // type error
-axiom i - r == 0.0;            // type error
-axiom i * r == 0.0;            // type error
-axiom i div r == 0;            // type error
-axiom i mod r == 0;            // type error
-
-axiom i / i == 0;              // type error
-axiom i / i == 0.0;
-axiom i / r == 0.0;
-axiom r / i == 0.0;
-axiom r / r == 0.0;
-
-axiom i ** r == 0.0;           // type error
-axiom r ** r == 0.0;
-
-axiom real(i) == 0.0;
-axiom real(i) == i;            // type error
-axiom int(r) == 0;
-axiom int(r) == r;             // type error
-axiom int(real(i)) == i;
-axiom real(int(r)) == r;
-axiom int(int(r)) == i;        // type error
-axiom real(real(i)) == r;      // type error
-
-axiom i == 0;
-axiom real(i) >= 0.0;
-axiom real(i) <= 0.0e0;
-axiom r < 0.0e-0;
-axiom r > 0.0e20;
-
-axiom -r == real(i);
-axiom real(i) + r == 0.0;
-axiom r - real(0) == 0.0;
-axiom r * r == 0.0;
-axiom r div 0 == 0;            // type error
-axiom r mod 0 == 0;            // type error
-
-axiom r ** r == 0.0;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const i: int;
+const r: real;
+
+axiom i == 0;
+axiom i >= 0.0;                // type error
+axiom i <= 0.0e0;              // type error
+axiom i < 0.0e-0;              // type error
+axiom i > 0.0e20;              // type error
+
+axiom -i == r;                 // type error
+axiom i + r == 0.0;            // type error
+axiom i - r == 0.0;            // type error
+axiom i * r == 0.0;            // type error
+axiom i div r == 0;            // type error
+axiom i mod r == 0;            // type error
+
+axiom i / i == 0;              // type error
+axiom i / i == 0.0;
+axiom i / r == 0.0;
+axiom r / i == 0.0;
+axiom r / r == 0.0;
+
+axiom i ** r == 0.0;           // type error
+axiom r ** r == 0.0;
+
+axiom real(i) == 0.0;
+axiom real(i) == i;            // type error
+axiom int(r) == 0;
+axiom int(r) == r;             // type error
+axiom int(real(i)) == i;
+axiom real(int(r)) == r;
+axiom int(int(r)) == i;        // type error
+axiom real(real(i)) == r;      // type error
+
+axiom i == 0;
+axiom real(i) >= 0.0;
+axiom real(i) <= 0.0e0;
+axiom r < 0.0e-0;
+axiom r > 0.0e20;
+
+axiom -r == real(i);
+axiom real(i) + r == 0.0;
+axiom r - real(0) == 0.0;
+axiom r * r == 0.0;
+axiom r div 0 == 0;            // type error
+axiom r mod 0 == 0;            // type error
+
+axiom r ** r == 0.0;
diff --git a/Test/test1/Lambda.bpl b/Test/test1/Lambda.bpl
index 016bece7..5136a1e5 100644
--- a/Test/test1/Lambda.bpl
+++ b/Test/test1/Lambda.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
 procedure foo()
 {
   var a: [int,int]int;
diff --git a/Test/test1/LogicalExprs.bpl b/Test/test1/LogicalExprs.bpl
index 02174a32..a5d3f987 100644
--- a/Test/test1/LogicalExprs.bpl
+++ b/Test/test1/LogicalExprs.bpl
@@ -1,8 +1,8 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const P: bool;
-const Q: bool;
-
-axiom (forall x: int :: x < 0);
-axiom Q ==> P;
-axiom (forall x: int :: x < 0) ==> P;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const P: bool;
+const Q: bool;
+
+axiom (forall x: int :: x < 0);
+axiom Q ==> P;
+axiom (forall x: int :: x < 0) ==> P;
diff --git a/Test/test1/MapsTypeErrors.bpl b/Test/test1/MapsTypeErrors.bpl
index bedb02ec..4b1bfec6 100644
--- a/Test/test1/MapsTypeErrors.bpl
+++ b/Test/test1/MapsTypeErrors.bpl
@@ -1,129 +1,129 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var m: []int;
-var p: <a>[]a;
-
-type ref;
-const null: ref;
-
-procedure P()
-  requires m[] == 5;
-  modifies m;
-  modifies p;
-  ensures m[] == 30;
-  ensures p[] + p[] == 24;
-  ensures p[] == null;
-{
-  m[] := 12;
-  p[] := 12;
-  p[] := true;
-  assert p[] == m[];
-  assert p[];
-  m := m[:= 30];
-  p := p[:=null];
-}
-
-procedure A()
-{
-  m[] := 12;  // error: illegal assignment, because m is not in modifies clause
-}
-
-procedure B()
-  modifies m;
-{
-  m := m[];  // type error
-  m[] := m;  // type error
-}
-
-procedure C()
-  modifies m;
-{
-  m[] := true;  // type error
-}
-
-// -----
-
-procedure Genrc<T>(x: int) returns (t: T);
-
-procedure Caller() returns (b: bool)
-{
-  var y: ref;
-  call y := Genrc(5);
-  b := y == null;
-}
-
-// ----
-
-type Field a;
-type HeapType = <a>[ref, Field a]a;
-const F0: Field int;
-const F1: Field bool;
-const alloc: Field bool;
-var Heap: HeapType;
-
-function LiberalEqual<a,b>(a, b) returns (bool);
-function StrictEqual<a>(a,a) returns (bool);
-function IntEqual(Field int,Field int) returns (bool);
-
-procedure FrameCondition(this: ref)
-  requires F0 == F1;  // error
-  requires LiberalEqual(F0, F1);
-  requires StrictEqual(F0, F0);
-  requires StrictEqual(F0, F1);  // error
-  modifies Heap;
-  ensures (forall<alpha> o: ref, f: Field alpha ::
-    Heap[o,f] == old(Heap)[o,f] ||
-    !old(Heap)[o,alloc] ||
-    (o == this && StrictEqual(f, F0)) ||  // error: f and F0 don't have the same type
-    (o == this && LiberalEqual(f, f)) ||
-    (o == this && IntEqual(F0, f))  // error: f and F0 don't have the same type
-    );
-{
-}
-
-// ---- bitvector inference ----
-
-function Gimmie<T>() returns (T);
-function Same<T>(T,T) returns (T);
-procedure ConsumeAnything<T>(t: T);
-
-procedure Bvs(x: bv31, y: int) returns (a: bv32)
-{
-  a := x[50 : 18];  // error
-  a := y[50 : 18];  // error
-
-  a := Gimmie();  // fine, this can be made to have at least 32 bits
-  a := Gimmie()[50 : 18];  // fine, result is always 32 bits and Gimmie() can be made to have at least 50 bits
-  a := Gimmie()[50 : 17];  // error, result is 33 bits (but there's nothing wrong with Gimmie())
-
-  a := Gimmie() ++ Gimmie() ++ Gimmie();
-  a := Gimmie() ++ Gimmie()[20:0];
-  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[27:0];
-  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[22:0];
-  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0] ++ Gimmie();
-  a := Gimmie() ++ 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0];
-  a := Same(Gimmie(), Gimmie());
-  a := Same(Gimmie()[20:0], Gimmie());  // error, have only bv20, need bv32
-
-  a := Same(Gimmie() ++ Gimmie()[20:0], 0bv32);
-  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie());
-  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie() ++ Gimmie());
-  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie()[40:30] ++ Gimmie());
-  call ConsumeAnything(Same(Gimmie() ++ Gimmie()[20:0], 0bv18));  // error, can't make things smaller
-}
-
-// ---- maps again ----
-
-procedure Mmm() returns (a: [int,int]bool, b: HeapType, c: int)
-{
-  if (Gimmie()[null] == Gimmie()) {
-    a := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie());
-    b := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie());
-    a := Same(Gimmie()[Gimmie(), Gimmie() := 4], Gimmie());  // error
-    b := Same(Gimmie()[Gimmie(), Gimmie() := 5], Gimmie());
-    b := Same(Gimmie()[Gimmie(), 6 := Gimmie()], Gimmie());  // error
-  }
-  c := Gimmie()[Gimmie() := 10][null];
-  c := Gimmie()[Gimmie() := Gimmie()][null];
-  c := Gimmie()[Gimmie() := false][null];
-}
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var m: []int;
+var p: <a>[]a;
+
+type ref;
+const null: ref;
+
+procedure P()
+  requires m[] == 5;
+  modifies m;
+  modifies p;
+  ensures m[] == 30;
+  ensures p[] + p[] == 24;
+  ensures p[] == null;
+{
+  m[] := 12;
+  p[] := 12;
+  p[] := true;
+  assert p[] == m[];
+  assert p[];
+  m := m[:= 30];
+  p := p[:=null];
+}
+
+procedure A()
+{
+  m[] := 12;  // error: illegal assignment, because m is not in modifies clause
+}
+
+procedure B()
+  modifies m;
+{
+  m := m[];  // type error
+  m[] := m;  // type error
+}
+
+procedure C()
+  modifies m;
+{
+  m[] := true;  // type error
+}
+
+// -----
+
+procedure Genrc<T>(x: int) returns (t: T);
+
+procedure Caller() returns (b: bool)
+{
+  var y: ref;
+  call y := Genrc(5);
+  b := y == null;
+}
+
+// ----
+
+type Field a;
+type HeapType = <a>[ref, Field a]a;
+const F0: Field int;
+const F1: Field bool;
+const alloc: Field bool;
+var Heap: HeapType;
+
+function LiberalEqual<a,b>(a, b) returns (bool);
+function StrictEqual<a>(a,a) returns (bool);
+function IntEqual(Field int,Field int) returns (bool);
+
+procedure FrameCondition(this: ref)
+  requires F0 == F1;  // error
+  requires LiberalEqual(F0, F1);
+  requires StrictEqual(F0, F0);
+  requires StrictEqual(F0, F1);  // error
+  modifies Heap;
+  ensures (forall<alpha> o: ref, f: Field alpha ::
+    Heap[o,f] == old(Heap)[o,f] ||
+    !old(Heap)[o,alloc] ||
+    (o == this && StrictEqual(f, F0)) ||  // error: f and F0 don't have the same type
+    (o == this && LiberalEqual(f, f)) ||
+    (o == this && IntEqual(F0, f))  // error: f and F0 don't have the same type
+    );
+{
+}
+
+// ---- bitvector inference ----
+
+function Gimmie<T>() returns (T);
+function Same<T>(T,T) returns (T);
+procedure ConsumeAnything<T>(t: T);
+
+procedure Bvs(x: bv31, y: int) returns (a: bv32)
+{
+  a := x[50 : 18];  // error
+  a := y[50 : 18];  // error
+
+  a := Gimmie();  // fine, this can be made to have at least 32 bits
+  a := Gimmie()[50 : 18];  // fine, result is always 32 bits and Gimmie() can be made to have at least 50 bits
+  a := Gimmie()[50 : 17];  // error, result is 33 bits (but there's nothing wrong with Gimmie())
+
+  a := Gimmie() ++ Gimmie() ++ Gimmie();
+  a := Gimmie() ++ Gimmie()[20:0];
+  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[27:0];
+  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[22:0];
+  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0] ++ Gimmie();
+  a := Gimmie() ++ 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0];
+  a := Same(Gimmie(), Gimmie());
+  a := Same(Gimmie()[20:0], Gimmie());  // error, have only bv20, need bv32
+
+  a := Same(Gimmie() ++ Gimmie()[20:0], 0bv32);
+  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie());
+  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie() ++ Gimmie());
+  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie()[40:30] ++ Gimmie());
+  call ConsumeAnything(Same(Gimmie() ++ Gimmie()[20:0], 0bv18));  // error, can't make things smaller
+}
+
+// ---- maps again ----
+
+procedure Mmm() returns (a: [int,int]bool, b: HeapType, c: int)
+{
+  if (Gimmie()[null] == Gimmie()) {
+    a := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie());
+    b := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie());
+    a := Same(Gimmie()[Gimmie(), Gimmie() := 4], Gimmie());  // error
+    b := Same(Gimmie()[Gimmie(), Gimmie() := 5], Gimmie());
+    b := Same(Gimmie()[Gimmie(), 6 := Gimmie()], Gimmie());  // error
+  }
+  c := Gimmie()[Gimmie() := 10][null];
+  c := Gimmie()[Gimmie() := Gimmie()][null];
+  c := Gimmie()[Gimmie() := false][null];
+}
diff --git a/Test/test1/Orderings.bpl b/Test/test1/Orderings.bpl
index 4ab28a48..bad7c2ad 100644
--- a/Test/test1/Orderings.bpl
+++ b/Test/test1/Orderings.bpl
@@ -1,10 +1,10 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-type C;
-
-const c1:C;
-const c2:C extends c1;
-const c0:C extends a;         // error: parent of wrong type
-
-const a:int;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type C;
+
+const c1:C;
+const c2:C extends c1;
+const c0:C extends a;         // error: parent of wrong type
+
+const a:int;
diff --git a/Test/test1/StatementIds0.bpl b/Test/test1/StatementIds0.bpl
new file mode 100644
index 00000000..abf26159
--- /dev/null
+++ b/Test/test1/StatementIds0.bpl
@@ -0,0 +1,24 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+    assume {:id "s0"} true;
+    assert {:id "s0"} true;
+}
+
+procedure test1()
+{
+    call {:id "s0"} P();
+}
+
+procedure test2(n: int)
+{
+    while (*)
+      invariant {:id "s0"} true;
+      invariant {:id "s0"} true;
+    {
+    }
+}
+
+procedure P();
diff --git a/Test/test1/StatementIds0.bpl.expect b/Test/test1/StatementIds0.bpl.expect
new file mode 100644
index 00000000..4783d912
--- /dev/null
+++ b/Test/test1/StatementIds0.bpl.expect
@@ -0,0 +1,5 @@
+StatementIds0.bpl(7,4): Error: more than one statement with same id: s0
+StatementIds0.bpl(12,4): Error: more than one statement with same id: s0
+StatementIds0.bpl(18,6): Error: more than one statement with same id: s0
+StatementIds0.bpl(19,6): Error: more than one statement with same id: s0
+4 name resolution errors detected in StatementIds0.bpl
diff --git a/Test/test1/UpdateExprTyping.bpl b/Test/test1/UpdateExprTyping.bpl
index bf8fd47c..41b88a3c 100644
--- a/Test/test1/UpdateExprTyping.bpl
+++ b/Test/test1/UpdateExprTyping.bpl
@@ -1,45 +1,45 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P(a: [int]bool, b: [int]ref, c: [bool]bool)
-{
-  assert a == b;  // type error
-  assert a == c;  // type error
-
-  assert a == a[5 := true];
-  assert a == a[true := true];  // type error
-  assert a == a[5 := 5]; // type error in RHS
-  assert a == b[5 := null];  // type error
-}
-
-procedure Q(aa: [int,ref]bool)
-{
-  assert aa[5,null := true] != aa[2,null := false];
-  assert aa == aa[null,null := true];  // type error, index 0
-  assert aa == aa[5,true := true];  // type error, index 1
-  assert aa == aa[5,null := null];  // type error, RHS
-}
-
-type Field a;
-const unique IntField: Field int;
-const unique RefField: Field ref;
-const unique SomeField: Field any;
-
-procedure R(H: <x>[ref,Field x]x, this: ref)
-{
-  var i: int, r: ref, y: any;
-  var K: <wz>[ref,Field wz]wz;
-
-  i := H[this, IntField];
-  r := H[this, RefField];
-  y := H[this, IntField];       // type error, wrong LHS
-  y := H[this, SomeField];
-
-  K := H[this, IntField := i][this, RefField := r][this, SomeField := y];
-  K := H[this, SomeField := r]; // type error, wrong RHS
-
-  K := K[this, IntField := r];  // RHS has wrong type (ref, expecting int)
-  K := K[this, RefField := i];  // RHS has wrong type (int, expecting ref)
-}
-
-type ref, any;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P(a: [int]bool, b: [int]ref, c: [bool]bool)
+{
+  assert a == b;  // type error
+  assert a == c;  // type error
+
+  assert a == a[5 := true];
+  assert a == a[true := true];  // type error
+  assert a == a[5 := 5]; // type error in RHS
+  assert a == b[5 := null];  // type error
+}
+
+procedure Q(aa: [int,ref]bool)
+{
+  assert aa[5,null := true] != aa[2,null := false];
+  assert aa == aa[null,null := true];  // type error, index 0
+  assert aa == aa[5,true := true];  // type error, index 1
+  assert aa == aa[5,null := null];  // type error, RHS
+}
+
+type Field a;
+const unique IntField: Field int;
+const unique RefField: Field ref;
+const unique SomeField: Field any;
+
+procedure R(H: <x>[ref,Field x]x, this: ref)
+{
+  var i: int, r: ref, y: any;
+  var K: <wz>[ref,Field wz]wz;
+
+  i := H[this, IntField];
+  r := H[this, RefField];
+  y := H[this, IntField];       // type error, wrong LHS
+  y := H[this, SomeField];
+
+  K := H[this, IntField := i][this, RefField := r][this, SomeField := y];
+  K := H[this, SomeField := r]; // type error, wrong RHS
+
+  K := K[this, IntField := r];  // RHS has wrong type (ref, expecting int)
+  K := K[this, RefField := i];  // RHS has wrong type (int, expecting ref)
+}
+
+type ref, any;
+const null : ref;
diff --git a/Test/test1/WhereTyping.bpl b/Test/test1/WhereTyping.bpl
index 0884e8ef..b3675f45 100644
--- a/Test/test1/WhereTyping.bpl
+++ b/Test/test1/WhereTyping.bpl
@@ -1,47 +1,47 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g: int where g == 12;
-
-procedure P(x: int where x > 0) returns (y: int where y < 0);
-  requires x < 100;
-  modifies g;
-  ensures -100 < y;
-
-implementation P(xx: int) returns (yy: int)
-{
-  var a: int;
-  var b: int;
-
-  start:
-    a := xx;
-    call b := P(a);
-    yy := b;
-    return;
-}
-
-type double;
-function F(double) returns (double);
-function G(double) returns (bool);
-
-procedure Q(omega: double where omega == F(omega),
-            psi: double where psi + 1 == 0,  // error: psi doesn't have right type for +
-            pi: double where F(pi),          // error: F has wrong return type
-            sigma: double where G(sigma));
-
-
-const SomeConstant: name;
-function fgh(int) returns (int);
-
-procedure Cnst(n: name where n <: SomeConstant /*this SomeConstant refers to the const*/) returns (SomeConstant: int)
-{
-  var k: int where k != SomeConstant;  // fine, since SomeConstants refers to the out parameter
-  var m: name where m != SomeConstant;  // error: types don't match up
-  var r: ref where (forall abc: int :: abc == SomeConstant);
-  var b: bool;
-  start:
-    b := (forall x: int :: fgh(x) < SomeConstant);
-    b := (forall l: name :: l == SomeConstant);  // error: SomeConstant here refers to the out parameter
-    return;
-}
-
-type ref, name;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g: int where g == 12;
+
+procedure P(x: int where x > 0) returns (y: int where y < 0);
+  requires x < 100;
+  modifies g;
+  ensures -100 < y;
+
+implementation P(xx: int) returns (yy: int)
+{
+  var a: int;
+  var b: int;
+
+  start:
+    a := xx;
+    call b := P(a);
+    yy := b;
+    return;
+}
+
+type double;
+function F(double) returns (double);
+function G(double) returns (bool);
+
+procedure Q(omega: double where omega == F(omega),
+            psi: double where psi + 1 == 0,  // error: psi doesn't have right type for +
+            pi: double where F(pi),          // error: F has wrong return type
+            sigma: double where G(sigma));
+
+
+const SomeConstant: name;
+function fgh(int) returns (int);
+
+procedure Cnst(n: name where n <: SomeConstant /*this SomeConstant refers to the const*/) returns (SomeConstant: int)
+{
+  var k: int where k != SomeConstant;  // fine, since SomeConstants refers to the out parameter
+  var m: name where m != SomeConstant;  // error: types don't match up
+  var r: ref where (forall abc: int :: abc == SomeConstant);
+  var b: bool;
+  start:
+    b := (forall x: int :: fgh(x) < SomeConstant);
+    b := (forall l: name :: l == SomeConstant);  // error: SomeConstant here refers to the out parameter
+    return;
+}
+
+type ref, name;