chore: Clean up build

.gitignore

@@ -81,3 +81,6 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/server/*.bvd
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/model
 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/*.html
 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/**/*.html
+Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.dtr
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary-lib
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary.doo

.pre-commit-config.yaml

@@ -4,5 +4,6 @@ repos:
  - id: dotnet-format
  name: dotnet-format
  language: system
- entry: dotnet format whitespace Source/Dafny.sln -v:d --include 
+ entry: dotnet format whitespace Source/Dafny.sln -v:d --include
+ exclude: 'GeneratedFromDafny|Source/DafnyRuntime/DafnyRuntimeSystemModule.cs'
  types_or: ["c#"]

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy.expect

@@ -1,2 +1,2 @@
-
+
 Dafny program verifier finished with 3 verified, 0 errors

Source/IntegrationTests/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 => ...

Source/IntegrationTests/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

Source/IntegrationTests/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

Source/IntegrationTests/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

Source/IntegrationTests/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
 

Source/IntegrationTests/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

Source/IntegrationTests/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
 

Source/IntegrationTests/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

Source/IntegrationTests/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'
 

Source/IntegrationTests/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) == {}

Source/IntegrationTests/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

Source/IntegrationTests/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

Source/IntegrationTests/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

Source/IntegrationTests/TestFiles/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

Source/IntegrationTests/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)

Source/IntegrationTests/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

Source/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

Source/IntegrationTests/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)

Source/IntegrationTests/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

Source/IntegrationTests/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

Source/IntegrationTests/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'

Source/IntegrationTests/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
 

Source/IntegrationTests/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

Source/IntegrationTests/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'))

Source/IntegrationTests/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)

Source/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

Source/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

Source/IntegrationTests/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
 

Source/IntegrationTests/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 _ => ...

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy.expect

@@ -1,4 +1,4 @@
-non-negative.dfy(6,8): Error: sequence size might be negative
+non-negative.dfy(6,8): Error: sequence size might be negative
  Asserted expression: 0 <= -1
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy.expect

@@ -1,4 +1,4 @@
-non-null.dfy(6,6): Error: target object might be null
+non-null.dfy(6,6): Error: target object might be null
  Asserted expression: a != null
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/not-ghost-variant.dfy.expect

@@ -1,4 +1,4 @@
-not-ghost-variant.dfy(8,7): Error: in a compiled context, discriminator 'C0?' cannot be applied to a datatype value of a ghost variant (ghost constructor 'G0' or 'G1')
+not-ghost-variant.dfy(8,7): Error: in a compiled context, discriminator 'C0?' cannot be applied to a datatype value of a ghost variant (ghost constructor 'G0' or 'G1')
  Asserted expression: !(d.G0? || d.G1?)
 not-ghost-variant.dfy(15,7): Error: in a compiled context, equality cannot be applied to a datatype value of a ghost variant (ghost constructor 'G0' or 'G1')
  Asserted expression: !(d.G0? || d.G1?)

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy.expect

@@ -1,4 +1,4 @@
-ordinal-subtraction-is-natural.dfy(7,7): Error: RHS of ORDINAL subtraction must be a natural number, but the given RHS might be larger
+ordinal-subtraction-is-natural.dfy(7,7): Error: RHS of ORDINAL subtraction must be a natural number, but the given RHS might be larger
  Asserted expression: o1.IsNat
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy.expect

@@ -1,4 +1,4 @@
-ordinal-subtraction-underflow.dfy(7,7): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
+ordinal-subtraction-underflow.dfy(7,7): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
  Asserted expression: o1.Offset <= o0.Offset
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/pattern-shape-is-valid.dfy.expect

@@ -1,4 +1,4 @@
-pattern-shape-is-valid.dfy(7,11): Error: assertion might not hold
+pattern-shape-is-valid.dfy(7,11): Error: assertion might not hold
  Asserted expression: d.D0?
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/precondition-satisfied.dfy.expect

@@ -1,4 +1,4 @@
-precondition-satisfied.dfy(12,4): Error: function precondition could not be proved
+precondition-satisfied.dfy(12,4): Error: function precondition could not be proved
  Asserted expression: b != 0
 precondition-satisfied.dfy(5,15): Related location: this proposition could not be proved
 precondition-satisfied.dfy(23,4): Error: divisor must be nonzero

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/prefix-equality-limit.dfy.expect

@@ -1,4 +1,4 @@
-prefix-equality-limit.dfy(7,19): Error: prefix-equality limit must be at least 0
+prefix-equality-limit.dfy(7,19): Error: prefix-equality limit must be at least 0
  Asserted expression: 0 <= i
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/requires-weaker.dfy.expect

@@ -1,4 +1,4 @@
-requires-weaker.dfy(15,2): Error: the method must provide an equal or more permissive precondition than in its parent trait
+requires-weaker.dfy(15,2): Error: the method must provide an equal or more permissive precondition than in its parent trait
  Asserted expression: P(i') && Q(i') ==> P(i' + 1) ==> Q(i' + 1)
 requires-weaker.dfy(15,2): Error: the method must provide an equal or more permissive precondition than in its parent trait
  Asserted expression: P(i') && Q(i') ==> Q(i' * 2)

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect

@@ -1,4 +1,4 @@
-shift-lower-bound.dfy(5,6): Error: rotate amount must be non-negative
+shift-lower-bound.dfy(5,6): Error: rotate amount must be non-negative
  Asserted expression: 0 <= -1
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy.expect

@@ -1,4 +1,4 @@
-shift-upper-bound.dfy(5,6): Error: rotate amount must not exceed the width of the result (2)
+shift-upper-bound.dfy(5,6): Error: rotate amount must not exceed the width of the result (2)
  Asserted expression: 3 <= 2
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/subrange-check-no-type-system-refresh.dfy.expect

@@ -1,4 +1,4 @@
-subrange-check-no-type-system-refresh.dfy(5,30): Error: value of expression (of type 'object?') is not known to be an instance of type 'object', because it might be null
+subrange-check-no-type-system-refresh.dfy(5,30): Error: value of expression (of type 'object?') is not known to be an instance of type 'object', because it might be null
  Asserted expression: o is object
 subrange-check-no-type-system-refresh.dfy(6,28): Error: value does not satisfy the subset constraints of 'T -> U' (possible cause: it may be partial or have read effects)
 subrange-check-no-type-system-refresh.dfy(7,31): Error: value does not satisfy the subset constraints of 'T --> U' (possible cause: it may have read effects)

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/subrange-check.dfy.expect

@@ -1,4 +1,4 @@
-subrange-check.dfy(5,30): Error: value of expression (of type 'object?') is not known to be an instance of type 'object', because it might be null
+subrange-check.dfy(5,30): Error: value of expression (of type 'object?') is not known to be an instance of type 'object', because it might be null
  Asserted expression: o is object
 subrange-check.dfy(6,28): Error: value does not satisfy the subset constraints of 'T -> U' (possible cause: it may be partial or have read effects)
  Asserted expression: p is T -> U

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/valid-constructor-names.dfy.expect

@@ -1,4 +1,4 @@
-valid-constructor-names.dfy(7,14): Error: source of datatype update must be constructed by 'D2' or 'D0'
+valid-constructor-names.dfy(7,14): Error: source of datatype update must be constructed by 'D2' or 'D0'
  Asserted expression: d.D2? || d.D0?
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy.expect

@@ -1,4 +1,4 @@
-witness-check.dfy(4,8): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
+witness-check.dfy(4,8): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
  Asserted expression: 0 > 0
 
 Dafny program verifier finished with 0 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/yield-ensures.dfy.expect

@@ -1,4 +1,4 @@
-yield-ensures.dfy(8,24): Error: possible violation of yield-ensures condition
+yield-ensures.dfy(8,24): Error: possible violation of yield-ensures condition
  Asserted expression: count == val
 yield-ensures.dfy(5,25): Related location: this proposition could not be proved
 yield-ensures.dfy(8,24): Error: possible violation of yield-ensures condition