Update expect files and run formatter

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

@@ -14,32 +14,32 @@ Definedness.dfy(60,21): Related location: this is the postcondition that could n
 Definedness.dfy(68,2): Error: a postcondition could not be proved on this return path
 Definedness.dfy(67,21): Related location: this is the postcondition that could not be proved
 Definedness.dfy(88,6): Error: target object might be null
-Definedness.dfy(89,4): Error: function precondition could not be proved
+Definedness.dfy(89,5): Error: function precondition could not be proved
 Definedness.dfy(79,15): Related location: this proposition could not be proved
 Definedness.dfy(89,9): Error: assignment might update an object not in the enclosing context's modifies clause
 Definedness.dfy(89,9): Error: target object might be null
-Definedness.dfy(90,9): Error: function precondition could not be proved
+Definedness.dfy(90,10): Error: function precondition could not be proved
 Definedness.dfy(79,15): Related location: this proposition could not be proved
 Definedness.dfy(95,13): Error: possible division by zero
 Definedness.dfy(95,22): Error: possible division by zero
 Definedness.dfy(96,14): Error: possible division by zero
 Definedness.dfy(101,11): Error: possible division by zero
 Definedness.dfy(108,14): Error: possible division by zero
-Definedness.dfy(117,22): Error: function precondition could not be proved
+Definedness.dfy(117,23): Error: function precondition could not be proved
 Definedness.dfy(79,15): Related location: this proposition could not be proved
-Definedness.dfy(123,16): Error: function precondition could not be proved
+Definedness.dfy(123,17): Error: function precondition could not be proved
 Definedness.dfy(79,15): Related location: this proposition could not be proved
-Definedness.dfy(133,16): Error: function precondition could not be proved
+Definedness.dfy(133,17): Error: function precondition could not be proved
 Definedness.dfy(79,15): Related location: this proposition could not be proved
 Definedness.dfy(133,21): Error: this loop invariant could not be proved on entry
  Related message: loop invariant violation
-Definedness.dfy(134,16): Error: function precondition could not be proved
+Definedness.dfy(134,17): Error: function precondition could not be proved
 Definedness.dfy(79,15): Related location: this proposition could not be proved
 Definedness.dfy(143,14): Error: possible division by zero
 Definedness.dfy(162,14): Error: possible division by zero
 Definedness.dfy(175,27): Error: this loop invariant could not be proved on entry
  Related message: loop invariant violation
-Definedness.dfy(181,16): Error: function precondition could not be proved
+Definedness.dfy(181,17): Error: function precondition could not be proved
 Definedness.dfy(79,15): Related location: this proposition could not be proved
 Definedness.dfy(196,18): Error: possible division by zero
 Definedness.dfy(196,22): Error: this loop invariant could not be proved on entry

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

@@ -2,7 +2,7 @@ IteratorResolution.dfy(22,9): Error: LHS of assignment must denote a mutable fie
 IteratorResolution.dfy(24,9): Error: LHS of assignment must denote a mutable field
 IteratorResolution.dfy(64,9): Error: LHS of assignment must denote a mutable field
 IteratorResolution.dfy(69,18): Error: arguments must have comparable types (got _T0 and int)
-IteratorResolution.dfy(84,16): Error: incorrect argument type for constructor in-parameter 't' (expected bool, found int)
+IteratorResolution.dfy(84,36): Error: incorrect argument type for constructor in-parameter 't' (expected bool, found int)
 IteratorResolution.dfy(81,19): Error: RHS (of type bool) not assignable to LHS (of type int)
 IteratorResolution.dfy(129,11): Error: unresolved identifier: _decreases3
 IteratorResolution.dfy(131,4): Error: LHS of assignment must denote a mutable field
@@ -21,8 +21,8 @@ IteratorResolution.dfy(173,40): Error: type parameter 0 (A) passed to constructo
 IteratorResolution.dfy(174,40): Error: type parameter 1 (B) passed to constructor Init must support auto-initialization (got Six)
 IteratorResolution.dfy(179,24): Error: type parameter 0 (A) passed to method MyMethod must support equality (got Stream)
 IteratorResolution.dfy(180,22): Error: type parameter 1 (B) passed to method MyMethod must support auto-initialization (got Six)
-IteratorResolution.dfy(185,13): Error: type parameter 0 (A) passed to function MyFunction must support equality (got Stream)
-IteratorResolution.dfy(186,13): Error: type parameter 1 (B) passed to function MyFunction must support auto-initialization (got Six)
+IteratorResolution.dfy(185,35): Error: type parameter 0 (A) passed to function MyFunction must support equality (got Stream)
+IteratorResolution.dfy(186,33): Error: type parameter 1 (B) passed to function MyFunction must support auto-initialization (got Six)
 IteratorResolution.dfy(213,22): Error: type parameter 0 (A) passed to type MyIter must support equality (got Stream)
 IteratorResolution.dfy(213,22): Error: type parameter 0 (A) passed to type MyIter must support equality (got Stream)
 IteratorResolution.dfy(216,22): Error: type parameter 0 (A) passed to type MyIter must support equality (got Stream)

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

@@ -2,28 +2,28 @@ OpaqueFunctions.dfy(214,2): Error: assertion might not hold
 OpaqueFunctions.dfy(229,2): Error: assertion might not hold
 OpaqueFunctions.dfy(38,6): Error: assertion might not hold
 OpaqueFunctions.dfy(69,7): Error: a precondition for this call could not be proved
-OpaqueFunctions.dfy(35,15): Related location: this is the precondition that could not be proved
+OpaqueFunctions.dfy(35,20): Related location: this is the precondition that could not be proved
 OpaqueFunctions.dfy(75,4): Error: assertion might not hold
 OpaqueFunctions.dfy(77,6): Error: assertion might not hold
 OpaqueFunctions.dfy(80,6): Error: assertion might not hold
 OpaqueFunctions.dfy(96,8): Error: assertion might not hold
 OpaqueFunctions.dfy(98,11): Error: a precondition for this call could not be proved
-OpaqueFunctions.dfy[A'](35,15): Related location: this is the precondition that could not be proved
+OpaqueFunctions.dfy[A'](35,20): Related location: this is the precondition that could not be proved
 OpaqueFunctions.dfy(102,6): Error: assertion might not hold
 OpaqueFunctions.dfy(109,4): Error: assertion might not hold
 OpaqueFunctions.dfy(111,6): Error: assertion might not hold
 OpaqueFunctions.dfy(114,6): Error: assertion might not hold
 OpaqueFunctions.dfy(123,31): Error: assertion might not hold
 OpaqueFunctions.dfy(146,6): Error: assertion might not hold
 OpaqueFunctions.dfy(148,9): Error: a precondition for this call could not be proved
-OpaqueFunctions.dfy[A'](35,15): Related location: this is the precondition that could not be proved
+OpaqueFunctions.dfy[A'](35,20): Related location: this is the precondition that could not be proved
 OpaqueFunctions.dfy(155,4): Error: assertion might not hold
 OpaqueFunctions.dfy(157,6): Error: assertion might not hold
 OpaqueFunctions.dfy(160,6): Error: assertion might not hold
 OpaqueFunctions.dfy(165,31): Error: assertion might not hold
 OpaqueFunctions.dfy(181,4): Error: assertion might not hold
-OpaqueFunctions.dfy(246,11): Error: assertion might not hold
-OpaqueFunctions.dfy(261,11): Error: assertion might not hold
+OpaqueFunctions.dfy(246,12): Error: assertion might not hold
+OpaqueFunctions.dfy(261,12): Error: assertion might not hold
 OpaqueFunctions.dfy(326,6): Error: assertion might not hold
 OpaqueFunctions.dfy(328,6): Error: assertion might not hold
 OpaqueFunctions.dfy(330,6): Error: assertion might not hold

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

@@ -5,7 +5,7 @@ ResolutionErrors1.dfy(51,30): Error: Wrong number of type arguments (0 instead o
 ResolutionErrors1.dfy(66,20): Error: unresolved identifier: w
 ResolutionErrors1.dfy(85,8): Error: the type of this local variable is underspecified
 ResolutionErrors1.dfy(86,25): Error: the type of this variable is underspecified
-ResolutionErrors1.dfy(86,23): Error: type parameter 'T' (inferred to be '?') in the function call to 'P' could not be determined
+ResolutionErrors1.dfy(86,24): Error: type parameter 'T' (inferred to be '?') in the function call to 'P' could not be determined
 ResolutionErrors1.dfy(86,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly
 ResolutionErrors1.dfy(99,13): Error: a lemma is not allowed to use 'new'
 ResolutionErrors1.dfy(100,9): Error: a lemma is not allowed to use 'new'

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

@@ -4,14 +4,14 @@ ResolutionErrors6.dfy(71,11): Error: name of type (Cache) is used as a variable
 ResolutionErrors6.dfy(71,17): Error: incorrect type for selection into ? (got X)
 ResolutionErrors6.dfy(79,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning
 ResolutionErrors6.dfy(89,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning
-ResolutionErrors6.dfy(123,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
-ResolutionErrors6.dfy(124,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(123,14): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(124,14): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
 ResolutionErrors6.dfy(126,11): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization.
 ResolutionErrors6.dfy(147,4): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization.
-ResolutionErrors6.dfy(157,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
-ResolutionErrors6.dfy(158,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
-ResolutionErrors6.dfy(164,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
-ResolutionErrors6.dfy(165,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(157,16): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(158,23): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(164,16): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(165,23): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
 ResolutionErrors6.dfy(182,23): Error: type of left argument to * (int) must agree with the result type (bool)
 ResolutionErrors6.dfy(182,23): Error: type of * must be of a numeric type, bitvector type, or a set-like type (instead got bool)
 ResolutionErrors6.dfy(181,13): Error: not resolving module 'V' because there were errors in resolving its nested module 'W'
@@ -45,7 +45,7 @@ ResolutionErrors6.dfy(343,18): Error: map update requires the value to have the
 ResolutionErrors6.dfy(368,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 363 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization)
 ResolutionErrors6.dfy(371,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 363 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization)
 ResolutionErrors6.dfy(372,5): Error: type parameter (G) passed to method P must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 363 as 'Z(00)', which says it can only be instantiated with a nonempty type)
-ResolutionErrors6.dfy(381,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 376 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization)
-ResolutionErrors6.dfy(384,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization)
-ResolutionErrors6.dfy(385,9): Error: type parameter (G) passed to function FP must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(00)', which says it can only be instantiated with a nonempty type)
+ResolutionErrors6.dfy(381,11): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 376 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization)
+ResolutionErrors6.dfy(384,11): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization)
+ResolutionErrors6.dfy(385,11): Error: type parameter (G) passed to function FP must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(00)', which says it can only be instantiated with a nonempty type)
 46 resolution/type errors detected in ResolutionErrors6.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors6.dfy.refresh.expect

@@ -4,14 +4,14 @@ ResolutionErrors6.dfy(44,50): Error: the argument of a fresh expression must den
 ResolutionErrors6.dfy(71,11): Error: name of type (Cache) is used as a variable
 ResolutionErrors6.dfy(79,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning
 ResolutionErrors6.dfy(89,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning
-ResolutionErrors6.dfy(123,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
-ResolutionErrors6.dfy(124,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(123,14): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(124,14): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
 ResolutionErrors6.dfy(126,11): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization.
 ResolutionErrors6.dfy(147,4): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization.
-ResolutionErrors6.dfy(157,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
-ResolutionErrors6.dfy(158,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
-ResolutionErrors6.dfy(164,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
-ResolutionErrors6.dfy(165,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(157,16): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(158,23): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(164,16): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
+ResolutionErrors6.dfy(165,23): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
 ResolutionErrors6.dfy(182,23): Error: type of right argument to * (bool) must agree with the result type (int)
 ResolutionErrors6.dfy(181,13): Error: not resolving module 'V' because there were errors in resolving its nested module 'W'
 ResolutionErrors6.dfy(191,21): Error: type of right argument to * (bool) must agree with the result type (int)
@@ -43,7 +43,7 @@ ResolutionErrors6.dfy(343,18): Error: map update requires the value to have the
 ResolutionErrors6.dfy(368,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 363 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization)
 ResolutionErrors6.dfy(371,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 363 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization)
 ResolutionErrors6.dfy(372,5): Error: type parameter (G) passed to method P must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 363 as 'Z(00)', which says it can only be instantiated with a nonempty type)
-ResolutionErrors6.dfy(381,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 376 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization)
-ResolutionErrors6.dfy(384,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization)
-ResolutionErrors6.dfy(385,9): Error: type parameter (G) passed to function FP must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(00)', which says it can only be instantiated with a nonempty type)
+ResolutionErrors6.dfy(381,11): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 376 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization)
+ResolutionErrors6.dfy(384,11): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization)
+ResolutionErrors6.dfy(385,11): Error: type parameter (G) passed to function FP must be nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 376 as 'Z(00)', which says it can only be instantiated with a nonempty type)
 44 resolution/type errors detected in ResolutionErrors6.dfy