Updating 30 tests

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect

@@ -13,13 +13,13 @@ revealFunctions.dfy(121,2): Info: hidden functions: Outer
 revealFunctions.dfy(131,10): Info: hidden functions: HideInFunction
 revealFunctions.dfy(134,2): Info: hidden functions: P
 revealFunctions.dfy(138,2): Info: hidden functions: P
-revealFunctions.dfy(15,4): Error: assertion might not hold
-revealFunctions.dfy(22,4): Error: assertion might not hold
-revealFunctions.dfy(49,4): Error: assertion might not hold
-revealFunctions.dfy(117,2): Error: assertion might not hold
-revealFunctions.dfy(118,2): Error: assertion might not hold
-revealFunctions.dfy(121,2): Error: assertion might not hold
-revealFunctions.dfy(134,2): Error: assertion might not hold
-revealFunctions.dfy(138,2): Error: assertion might not hold
+revealFunctions.dfy(15,4): Error: assertion could not be proved
+revealFunctions.dfy(22,4): Error: assertion could not be proved
+revealFunctions.dfy(49,4): Error: assertion could not be proved
+revealFunctions.dfy(117,2): Error: assertion could not be proved
+revealFunctions.dfy(118,2): Error: assertion could not be proved
+revealFunctions.dfy(121,2): Error: assertion could not be proved
+revealFunctions.dfy(134,2): Error: assertion could not be proved
+revealFunctions.dfy(138,2): Error: assertion could not be proved
 
 Dafny program verifier finished with 25 verified, 8 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/calls/CallBy.dfy.expect

@@ -1,8 +1,8 @@
-CallBy.dfy(26,2): Error: assertion might not hold
-CallBy.dfy(32,2): Error: assertion might not hold
-CallBy.dfy(39,2): Error: assertion might not hold
-CallBy.dfy(50,2): Error: assertion might not hold
-CallBy.dfy(56,2): Error: assertion might not hold
-CallBy.dfy(66,2): Error: assertion might not hold
+CallBy.dfy(26,2): Error: assertion could not be proved
+CallBy.dfy(32,2): Error: assertion could not be proved
+CallBy.dfy(39,2): Error: assertion could not be proved
+CallBy.dfy(50,2): Error: assertion could not be proved
+CallBy.dfy(56,2): Error: assertion could not be proved
+CallBy.dfy(66,2): Error: assertion could not be proved
 
 Dafny program verifier finished with 4 verified, 6 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/statement/opaqueBlock.dfy.expect

@@ -1,6 +1,6 @@
-opaqueBlock.dfy(15,2): Error: assertion might not hold
-opaqueBlock.dfy(28,2): Error: assertion might not hold
-opaqueBlock.dfy(42,2): Error: assertion might not hold
+opaqueBlock.dfy(15,2): Error: assertion could not be proved
+opaqueBlock.dfy(28,2): Error: assertion could not be proved
+opaqueBlock.dfy(42,2): Error: assertion could not be proved
 opaqueBlock.dfy(49,14): Error: possible division by zero
 opaqueBlock.dfy(54,17): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here
 opaqueBlock.dfy(71,21): Error: assignment might update an object not in the enclosing context's modifies clause
@@ -11,6 +11,6 @@ opaqueBlock.dfy(127,12): Error: variable 'y', which is subject to definite-assig
 opaqueBlock.dfy(130,17): Error: variable 'z', which is subject to definite-assignment rules, might be uninitialized here
 opaqueBlock.dfy(142,12): Error: ensures might not hold
 opaqueBlock.dfy(206,6): Error: assignment might update an object not in the enclosing context's modifies clause
-opaqueBlock.dfy(218,2): Error: assertion might not hold
+opaqueBlock.dfy(218,2): Error: assertion could not be proved
 
 Dafny program verifier finished with 3 verified, 14 errors

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

@@ -3,11 +3,11 @@ AsIsAgain.dfy(62,15): Error: value of expression (of type 'object') is not known
 AsIsAgain.dfy(64,15): Error: value of expression (of type 'object') is not known to be an instance of type 'B<W, int>'
 AsIsAgain.dfy(66,25): Error: value of expression (of type 'object') is not known to be an instance of type 'B<int, int>'
 AsIsAgain.dfy(68,15): Error: value of expression (of type 'object') is not known to be an instance of type 'A<W>'
-AsIsAgain.dfy(119,4): Error: assertion might not hold
-AsIsAgain.dfy(123,4): Error: assertion might not hold
-AsIsAgain.dfy(128,4): Error: assertion might not hold
-AsIsAgain.dfy(139,4): Error: assertion might not hold
-AsIsAgain.dfy(143,4): Error: assertion might not hold
-AsIsAgain.dfy(148,4): Error: assertion might not hold
+AsIsAgain.dfy(119,4): Error: assertion could not be proved
+AsIsAgain.dfy(123,4): Error: assertion could not be proved
+AsIsAgain.dfy(128,4): Error: assertion could not be proved
+AsIsAgain.dfy(139,4): Error: assertion could not be proved
+AsIsAgain.dfy(143,4): Error: assertion could not be proved
+AsIsAgain.dfy(148,4): Error: assertion could not be proved
 
 Dafny program verifier finished with 7 verified, 11 errors

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

@@ -1,12 +1,12 @@
 BigOrdinals.dfy(18,11): Error: a negative integer cannot be converted to an ORDINAL
 BigOrdinals.dfy(20,11): Error: value to be converted might be bigger than every natural number
-BigOrdinals.dfy(35,4): Error: assertion might not hold
-BigOrdinals.dfy(53,4): Error: assertion might not hold
+BigOrdinals.dfy(35,4): Error: assertion could not be proved
+BigOrdinals.dfy(53,4): Error: assertion could not be proved
 BigOrdinals.dfy(64,15): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
 BigOrdinals.dfy(66,15): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
 BigOrdinals.dfy(68,15): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
 BigOrdinals.dfy(73,15): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
-BigOrdinals.dfy(88,4): Error: assertion might not hold
+BigOrdinals.dfy(88,4): Error: assertion could not be proved
 BigOrdinals.dfy(113,9): Error: value does not satisfy the subset constraints of 'ConstrainedOrdinal'
 BigOrdinals.dfy(120,9): Error: value does not satisfy the subset constraints of 'ConstrainedOrdinal'
 

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

@@ -457,39 +457,39 @@ BitvectorsMore.dfy(21,13): Error: possible division by zero
 BitvectorsMore.dfy(25,13): Error: possible division by zero
 BitvectorsMore.dfy(30,15): Error: possible division by zero
 BitvectorsMore.dfy(32,15): Error: possible division by zero
-BitvectorsMore.dfy(104,37): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(104,37): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(105,35): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(105,38): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(105,38): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(107,34): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(107,37): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(107,37): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(108,34): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(115,42): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(115,42): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(116,39): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(116,42): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(116,42): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(124,28): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(124,31): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(124,31): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(125,28): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(125,31): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(125,31): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(135,24): Error: shift amount must not exceed the width of the result (32)
-BitvectorsMore.dfy(135,27): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv6
+BitvectorsMore.dfy(135,27): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv6
 BitvectorsMore.dfy(136,24): Error: shift amount must not exceed the width of the result (32)
-BitvectorsMore.dfy(136,27): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv6
+BitvectorsMore.dfy(136,27): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv6
 BitvectorsMore.dfy(137,24): Error: shift amount must not exceed the width of the result (32)
-BitvectorsMore.dfy(137,27): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv6
-BitvectorsMore.dfy(146,35): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv3
-BitvectorsMore.dfy(147,35): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv3
-BitvectorsMore.dfy(148,35): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv3
+BitvectorsMore.dfy(137,27): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv6
+BitvectorsMore.dfy(146,35): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv3
+BitvectorsMore.dfy(147,35): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv3
+BitvectorsMore.dfy(148,35): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv3
 BitvectorsMore.dfy(157,26): Error: shift amount must not exceed the width of the result (2)
-BitvectorsMore.dfy(157,29): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv2
+BitvectorsMore.dfy(157,29): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv2
 BitvectorsMore.dfy(158,26): Error: shift amount must not exceed the width of the result (2)
-BitvectorsMore.dfy(158,29): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv2
+BitvectorsMore.dfy(158,29): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv2
 BitvectorsMore.dfy(159,26): Error: shift amount must not exceed the width of the result (2)
-BitvectorsMore.dfy(159,29): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv2
+BitvectorsMore.dfy(159,29): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv2
 BitvectorsMore.dfy(160,26): Error: shift amount must not exceed the width of the result (2)
-BitvectorsMore.dfy(168,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(169,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(170,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(171,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
+BitvectorsMore.dfy(168,33): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv0
+BitvectorsMore.dfy(169,33): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv0
+BitvectorsMore.dfy(170,33): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv0
+BitvectorsMore.dfy(171,33): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv0
 BitvectorsMore.dfy(193,36): Error: rotate amount must not exceed the width of the result (5)
 BitvectorsMore.dfy(194,37): Error: rotate amount must not exceed the width of the result (5)
 

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

@@ -517,39 +517,39 @@ BitvectorsMore.dfy(21,13): Error: possible division by zero
 BitvectorsMore.dfy(25,13): Error: possible division by zero
 BitvectorsMore.dfy(30,15): Error: possible division by zero
 BitvectorsMore.dfy(32,15): Error: possible division by zero
-BitvectorsMore.dfy(104,37): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(104,37): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(105,35): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(105,38): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(105,38): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(107,34): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(107,37): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(107,37): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(108,34): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(115,42): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(115,42): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(116,39): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(116,42): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(116,42): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(124,28): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(124,31): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(124,31): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(125,28): Error: shift amount must not exceed the width of the result (67)
-BitvectorsMore.dfy(125,31): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv7
+BitvectorsMore.dfy(125,31): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv7
 BitvectorsMore.dfy(135,24): Error: shift amount must not exceed the width of the result (32)
-BitvectorsMore.dfy(135,27): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv6
+BitvectorsMore.dfy(135,27): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv6
 BitvectorsMore.dfy(136,24): Error: shift amount must not exceed the width of the result (32)
-BitvectorsMore.dfy(136,27): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv6
+BitvectorsMore.dfy(136,27): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv6
 BitvectorsMore.dfy(137,24): Error: shift amount must not exceed the width of the result (32)
-BitvectorsMore.dfy(137,27): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv6
-BitvectorsMore.dfy(146,35): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv3
-BitvectorsMore.dfy(147,35): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv3
-BitvectorsMore.dfy(148,35): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv3
+BitvectorsMore.dfy(137,27): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv6
+BitvectorsMore.dfy(146,35): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv3
+BitvectorsMore.dfy(147,35): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv3
+BitvectorsMore.dfy(148,35): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv3
 BitvectorsMore.dfy(157,26): Error: shift amount must not exceed the width of the result (2)
-BitvectorsMore.dfy(157,29): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv2
+BitvectorsMore.dfy(157,29): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv2
 BitvectorsMore.dfy(158,26): Error: shift amount must not exceed the width of the result (2)
-BitvectorsMore.dfy(158,29): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv2
+BitvectorsMore.dfy(158,29): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv2
 BitvectorsMore.dfy(159,26): Error: shift amount must not exceed the width of the result (2)
-BitvectorsMore.dfy(159,29): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv2
+BitvectorsMore.dfy(159,29): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv2
 BitvectorsMore.dfy(160,26): Error: shift amount must not exceed the width of the result (2)
-BitvectorsMore.dfy(168,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(169,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(170,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
-BitvectorsMore.dfy(171,33): Error: when converting shift amount to a bit vector, the value to be converted might not fit in bv0
+BitvectorsMore.dfy(168,33): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv0
+BitvectorsMore.dfy(169,33): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv0
+BitvectorsMore.dfy(170,33): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv0
+BitvectorsMore.dfy(171,33): Error: when converting shift amount to a bit vector, the value to be converted could not be proved to fit in bv0
 BitvectorsMore.dfy(193,36): Error: rotate amount must not exceed the width of the result (5)
 BitvectorsMore.dfy(194,37): Error: rotate amount must not exceed the width of the result (5)
 

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

@@ -1,6 +1,6 @@
-Char.dfy(48,8): Error: assertion might not hold
-Char.dfy(52,8): Error: assertion might not hold
-Char.dfy(63,6): Error: assertion might not hold
+Char.dfy(48,8): Error: assertion could not be proved
+Char.dfy(52,8): Error: assertion could not be proved
+Char.dfy(63,6): Error: assertion could not be proved
 Char.dfy(81,7): Error: char subtraction might underflow
 Char.dfy(81,13): Error: char addition might overflow
 Char.dfy(89,7): Error: char subtraction might underflow