remove byte-order mark from test files

dafny-lang · alex-chew · May 30, 2024 · May 30, 2024 · May 30, 2024 · May 31, 2024
commit 1a3d7902dc8d2a330cf8ce2a58994faf8fea69cb
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --relax-definite-assignment "%s" > "%t"
+// RUN: %verify --relax-definite-assignment "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C<G>

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy.expect
@@ -1,2 +1,2 @@
-
+
 Dafny program verifier finished with 3 verified, 0 errors
diff --git a/...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/alternative-is-complete.dfy b/...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/alternative-is-complete.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype D = D0 | D1

diff --git a/...Tests/TestFiles/LitTests/LitTest/proof-obligation-desc/alternative-is-complete.dfy.expect b/...Tests/TestFiles/LitTests/LitTest/proof-obligation-desc/alternative-is-complete.dfy.expect
@@ -1,4 +1,4 @@
-alternative-is-complete.dfy(7,2): Error: alternative cases fail to cover all possibilities
+alternative-is-complete.dfy(7,2): Error: alternative cases fail to cover all possibilities
  Asserted expression: false
  in an added catch-all case:
  case true => ...

diff --git a/...ce/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy b/...ce/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method ArrayInitEmpty<T>() {

diff --git a/...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy.expect
@@ -1,4 +1,4 @@
-array-init-empty.dfy(5,13): Error: unless an initializer is provided for the array elements, a new array of 'T' must have empty size
+array-init-empty.dfy(5,13): Error: unless an initializer is provided for the array elements, a new array of 'T' must have empty size
  Asserted expression: 1 == 0
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy b/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method ArrayInitSizeValid() {

diff --git a/...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy.expect b/...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy.expect
@@ -1,4 +1,4 @@
-array-init-size-valid.dfy(5,21): Error: given array size must agree with the number of expressions in the initializing display (0)
+array-init-size-valid.dfy(5,21): Error: given array size must agree with the number of expressions in the initializing display (0)
  Asserted expression: 1 == |[]|
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/.../IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/assignment-shrinks.dfy b/.../IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/assignment-shrinks.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 iterator Repeat(val: int, count: nat) yields (res: int)

diff --git a/...ationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/assignment-shrinks.dfy.expect b/...ationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/assignment-shrinks.dfy.expect
@@ -1,4 +1,4 @@
-assignment-shrinks.dfy(18,11): Error: an assignment to _new is only allowed to shrink the set
+assignment-shrinks.dfy(18,11): Error: an assignment to _new is only allowed to shrink the set
  Asserted expression: old(allocated(repeat)) && repeat._new <= old(repeat._new)
 
 Dafny program verifier finished with 2 verified, 1 error
diff --git a/...ationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy b/...ationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --unicode-char=false --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --unicode-char=false --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function CanOverflow(c0: char, c1: char): char {

diff --git a/...sts/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy.expect b/...sts/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy.expect
@@ -1,4 +1,4 @@
-CLI: Warning: the option unicode-char has been deprecated.
+CLI: Warning: the option unicode-char has been deprecated.
 char-overflow-non-unicode.dfy(5,7): Error: char addition might overflow
  Asserted expression: 0 <= c0 as int + c1 as int && c0 as int + c1 as int < 65536
 

diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy b/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function CanOverflow(c0: char, c1: char): char {

diff --git a/...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy.expect b/...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy.expect
@@ -1,4 +1,4 @@
-char-overflow-unicode.dfy(5,7): Error: char addition might overflow
+char-overflow-unicode.dfy(5,7): Error: char addition might overflow
  Asserted expression: (0 <= c0 as int + c1 as int && c0 as int + c1 as int < 55296) || (57344 <= c0 as int + c1 as int && c0 as int + c1 as int < 1114112)
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy b/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --unicode-char=false --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --unicode-char=false --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function CanUnderflow(c0: char, c1: char): char {

diff --git a/...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy.expect b/...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy.expect
@@ -1,4 +1,4 @@
-CLI: Warning: the option unicode-char has been deprecated.
+CLI: Warning: the option unicode-char has been deprecated.
 char-underflow-non-unicode.dfy(5,7): Error: char subtraction might underflow
  Asserted expression: 0 <= c0 as int - c1 as int && c0 as int - c1 as int < 65536
 

diff --git a/...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy b/...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function CanUnderflow(c0: char, c1: char): char {

diff --git a/...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy.expect b/...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy.expect
@@ -1,4 +1,4 @@
-char-underflow-unicode.dfy(5,7): Error: char subtraction might underflow
+char-underflow-unicode.dfy(5,7): Error: char subtraction might underflow
  Asserted expression: (0 <= c0 as int - c1 as int && c0 as int - c1 as int < 55296) || (57344 <= c0 as int - c1 as int && c0 as int - c1 as int < 1114112)
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/comprehension-no-alias.dfy b/...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/comprehension-no-alias.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function ComprehensionNoAlias(i: nat, j: nat): map<int, nat>

diff --git a/...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/comprehension-no-alias.dfy.expect b/...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/comprehension-no-alias.dfy.expect
@@ -1,4 +1,4 @@
-comprehension-no-alias.dfy(6,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
+comprehension-no-alias.dfy(6,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 comprehension-no-alias.dfy(6,45): Error: key expressions might be referring to the same value
  Asserted expression: forall x: nat, y: nat, x': nat, y': nat | x < i && y < j && x' < i && y' < j && (x != x' || y != y') :: x + y != x' + y' || x == x'
 

diff --git a/...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/concurrent-frame-empty.dfy b/...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/concurrent-frame-empty.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions --reads-clauses-on-methods "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions --reads-clauses-on-methods "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C<T> {}

diff --git a/...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/concurrent-frame-empty.dfy.expect b/...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/concurrent-frame-empty.dfy.expect
@@ -1,4 +1,4 @@
-concurrent-frame-empty.dfy(6,23): Error: reads clause could not be proved to be empty ({:concurrent} restriction)
+concurrent-frame-empty.dfy(6,23): Error: reads clause could not be proved to be empty ({:concurrent} restriction)
  Asserted expression: forall c: C<T> :: ReadsEmpty.reads(c) == {}
 concurrent-frame-empty.dfy(12,21): Error: modifies clause could not be proved to be empty ({:concurrent} restriction)
  Asserted expression: forall c: C<T> :: ModifiesEmpty.modifies(c) == {}

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function ConversionFit(i: int): bv8

diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy.expect b/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy.expect
@@ -1,4 +1,4 @@
-conversion-fit.dfy(6,6): Error: value to be converted might not fit in bv8
+conversion-fit.dfy(6,6): Error: value to be converted might not fit in bv8
  Asserted expression: 0 < i && i <= 1 << 8
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy b/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function ConversionIsNatural(ord: ORDINAL): int

diff --git a/...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy.expect b/...onTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy.expect
@@ -1,4 +1,4 @@
-conversion-is-natural.dfy(6,8): Error: value to be converted might be bigger than every natural number
+conversion-is-natural.dfy(6,8): Error: value to be converted might be bigger than every natural number
  Asserted expression: ord is nat
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy b/...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function ConversionPositive(i: int): ORDINAL

diff --git a/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy.expect b/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy.expect
@@ -1,4 +1,4 @@
-conversion-positive.dfy(6,6): Error: a negative integer cannot be converted to an ORDINAL
+conversion-positive.dfy(6,6): Error: a negative integer cannot be converted to an ORDINAL
  Asserted expression: 0 <= i
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...sts/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy b/...sts/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint8 = x: int | 0 <= x < 0x100

diff --git a/...tFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy.expect b/...tFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy.expect
@@ -1,4 +1,4 @@
-conversion-satisfies-constraints.dfy(8,6): Error: result of operation might violate newtype constraint for 'uint8'
+conversion-satisfies-constraints.dfy(8,6): Error: result of operation might violate newtype constraint for 'uint8'
  Asserted expression: 0 <= i && i < 256
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy b/...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C<G>

diff --git a/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect b/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect
@@ -1,4 +1,4 @@
-definite-assignment.dfy(16,4): Error: field 'x', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
+definite-assignment.dfy(16,4): Error: field 'x', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
  Asserted expression: assigned(x)
 definite-assignment.dfy(16,4): Error: field 'y', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
  Asserted expression: assigned(y)

diff --git a/...ce/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/destructor-valid.dfy b/...ce/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/destructor-valid.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype D = D0(n: nat) | D1 | D2(b: bool, n: nat)

diff --git a/...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/destructor-valid.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/destructor-valid.dfy.expect
@@ -1,4 +1,4 @@
-destructor-valid.dfy(7,13): Error: destructor 'n' can only be applied to datatype values constructed by 'D0' or 'D2'
+destructor-valid.dfy(7,13): Error: destructor 'n' can only be applied to datatype values constructed by 'D0' or 'D2'
  Asserted expression: d.D0? || d.D2?
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/distinct-lhs.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/distinct-lhs.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method AssignArray(i: nat, j: nat, a: array<int>, x: int)

diff --git a/...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/distinct-lhs.dfy.expect b/...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/distinct-lhs.dfy.expect
@@ -1,4 +1,4 @@
-distinct-lhs.dfy(9,9): Error: when left-hand sides a[j] and a[i] refer to the same location, they must be assigned the same value
+distinct-lhs.dfy(9,9): Error: when left-hand sides a[j] and a[i] refer to the same location, they must be assigned the same value
  Asserted expression: a != a || j != i
 distinct-lhs.dfy(19,17): Error: when left-hand sides a[j0, j1] and a[i0, i1] refer to the same location, they must be assigned the same value
  Asserted expression: a != a || j0 != i0 || j1 != i1

diff --git a/...ce/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ensures-stronger.dfy b/...ce/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ensures-stronger.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 predicate P(i: int)

diff --git a/...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ensures-stronger.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ensures-stronger.dfy.expect
@@ -1,4 +1,4 @@
-ensures-stronger.dfy(16,2): Error: the method must provide an equal or more detailed postcondition than in its parent trait
+ensures-stronger.dfy(16,2): Error: the method must provide an equal or more detailed postcondition than in its parent trait
  Asserted expression: P(res') ==> b' ==> Q(res')
 ensures-stronger.dfy(16,2): Error: the method must provide an equal or more detailed postcondition than in its parent trait
  Asserted expression: P(res') ==> P(res' + 1)

diff --git a/...ntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy b/...ntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method ForRangeAssignable()

diff --git a/...ionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy.expect b/...ionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy.expect
@@ -1,4 +1,4 @@
-for-range-assignable.dfy(6,8): Error: entire range must be assignable to index variable, but some value does not satisfy the subset constraints of 'nat'
+for-range-assignable.dfy(6,8): Error: entire range must be assignable to index variable, but some value does not satisfy the subset constraints of 'nat'
  Asserted expression: forall i: nat | -1 <= i && i <= 0 :: i is nat
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy b/...egrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method ForRangeBoundsValid()

diff --git a/...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy.expect b/...nTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy.expect
@@ -1,4 +1,4 @@
-for-range-bounds-valid.dfy(6,13): Error: lower bound must not exceed upper bound
+for-range-bounds-valid.dfy(6,13): Error: lower bound must not exceed upper bound
  Asserted expression: 1 <= 0
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-lhs-unique.dfy b/...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-lhs-unique.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method ForallLHSUniqueArray(a: array<int>)

diff --git a/...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-lhs-unique.dfy.expect b/...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-lhs-unique.dfy.expect
@@ -1,4 +1,4 @@
-forall-lhs-unique.dfy(7,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
+forall-lhs-unique.dfy(7,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 forall-lhs-unique.dfy(15,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 forall-lhs-unique.dfy(8,13): Error: left-hand sides for different forall-statement bound variables might refer to the same location (and right-hand sides might not be equivalent)
  Asserted expression: forall i: int, i': int | 0 <= i < a.Length && 0 <= i' && i' < a.Length && i != i' :: a != a || 0 != 0 || i == i'

diff --git a/...ntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy b/...ntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method ForallPostcondition()

diff --git a/...ionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy.expect b/...ionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy.expect
@@ -1,4 +1,4 @@
-forall-postcondition.dfy(6,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
+forall-postcondition.dfy(6,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 forall-postcondition.dfy(6,27): Error: possible violation of postcondition of forall statement
  Asserted expression: b
 

diff --git a/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/frame-dereference-non-null.dfy b/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/frame-dereference-non-null.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C { var f: int }

diff --git a/...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/frame-dereference-non-null.dfy.expect b/...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/frame-dereference-non-null.dfy.expect
@@ -1,4 +1,4 @@
-frame-dereference-non-null.dfy(7,12): Error: frame expression might dereference null
+frame-dereference-non-null.dfy(7,12): Error: frame expression might dereference null
  Asserted expression: c != null
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/function-contract-override.dfy b/...tionTests/TestFiles/LitTests/LitTest/proof-obligation-desc/function-contract-override.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 predicate P(x: int)

diff --git a/...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/function-contract-override.dfy.expect b/...ts/TestFiles/LitTests/LitTest/proof-obligation-desc/function-contract-override.dfy.expect
@@ -1,4 +1,4 @@
-function-contract-override.dfy(14,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+function-contract-override.dfy(14,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait
  Asserted expression: F(i') < 10 ==> this.F(i') < 5
 function-contract-override.dfy(14,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait
  Asserted expression: F(i') < 10 ==> P(this.F(i'))

diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/indices-in-domain.dfy b/...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/indices-in-domain.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method IndicesInDomain() {

diff --git a/...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/indices-in-domain.dfy.expect b/...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/indices-in-domain.dfy.expect
@@ -1,4 +1,4 @@
-indices-in-domain.dfy(5,14): Error: all array indices must be in the domain of the initialization function
+indices-in-domain.dfy(5,14): Error: all array indices must be in the domain of the initialization function
  Asserted expression: forall i0: int | 0 <= i0 < 1 :: ((i: nat) requires i > 0 => 1).requires(i0)
 indices-in-domain.dfy(6,14): Error: all array indices must be in the domain of the initialization function
  Asserted expression: forall i0: int, i1: int | (0 <= i0 < 1) && (0 <= i1 < 1) :: ((i: nat, j: int) requires i > 0 && j < 0 => 1).requires(i0, i1)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C {

diff --git a/...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy.expect b/...IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy.expect
@@ -1,4 +1,4 @@
-is-allocated.dfy(11,19): Error: receiver could not be proved to be allocated in the state in which its fields are accessed
+is-allocated.dfy(11,19): Error: receiver could not be proved to be allocated in the state in which its fields are accessed
  Asserted expression: old(allocated(c))
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function IsInteger(r: real): int

diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy.expect b/...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy.expect
@@ -1,4 +1,4 @@
-is-integer.dfy(6,6): Error: the real-based number must be an integer (if you want truncation, apply .Floor to the real-based number)
+is-integer.dfy(6,6): Error: the real-based number must be an integer (if you want truncation, apply .Floor to the real-based number)
  Asserted expression: r == r.Floor as real
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/loop-invariant.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/loop-invariant.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method LoopInvariant() {

diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/loop-invariant.dfy.expect b/...tegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/loop-invariant.dfy.expect
@@ -1,4 +1,4 @@
-loop-invariant.dfy(7,16): Error: this invariant could not be proved to be maintained by the loop
+loop-invariant.dfy(7,16): Error: this invariant could not be proved to be maintained by the loop
  Related message: loop invariant violation
  Asserted expression: 0 <= i <= 10
 

diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/match-is-complete.dfy b/...e/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/match-is-complete.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype D = D0 | D1

diff --git a/...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/match-is-complete.dfy.expect b/...rationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/match-is-complete.dfy.expect
@@ -1,4 +1,4 @@
-match-is-complete.dfy(7,2): Error: missing case in match expression: D1
+match-is-complete.dfy(7,2): Error: missing case in match expression: D1
  Asserted expression: false
  in an added catch-all case:
  case _ => ...