Updated all .rs.check files

dafny-lang · MikaelMayer · Jun 22, 2024 · May 2, 2024 · May 31, 2024 · Jun 1, 2024
commit a9084e55c890ff989e1ac36642c46e0ed7439f4a
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BuiltIns.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BuiltIns.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `(bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool): Default` is not satisfied
+// CHECK-L: error[E0277]: the trait bound `dyn Fn() -> DafnyInt: Default` is not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BuiltIns_Unsupported.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BuiltIns_Unsupported.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `(bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool, bool): Default` is not satisfied
+// CHECK-L: error[E0277]: the trait bound `dyn for<'a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p, 'q> Fn(&'a bool, &'b bool, &'c bool, &'d bool, &'e bool, &'f bool, &'g bool, &'h bool, &'i bool, &'j bool, &'k bool, &'l bool, &'m bool, &'n bool, &'o bool, &'p bool, &'q bool) -> DafnyInt: Default` is not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/TailRecursion.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/TailRecursion.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0786]: found invalid metadata files for crate `alloc` which `std` depends on
+// CHECK: .*<i>Type\ name\ for\ ORDINAL\ \(Microsoft_dDafny_dBigOrdinalType\)</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/TypeDescriptors.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/TypeDescriptors.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0786]: found invalid metadata files for crate `core`
+// CHECK: .*<i>Type\ name\ for\ ORDINAL\ \(Microsoft_dDafny_dBigOrdinalType\)</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/UnicodeStrings.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/UnicodeStrings.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0786]: found invalid metadata files for crate `core` which `std` depends on
+// CHECK: .*<i>Unsupported:\ Cannot\ emit\ literal\ expression\ 0\ outside\ of\ expression\ context:\ Microsoft_dDafny_dCompilers_dBuilderSyntaxTree'1\[Microsoft_dDafny_dCompilers_dStatementContainer]</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Uninitialized.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Uninitialized.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: Unhandled exception: System.OutOfMemoryException: Exception of type 'System.OutOfMemoryException' was thrown.
+// CHECK: .*<i>QuantifierExpr</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Variance.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Variance.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0786]: found invalid metadata files for crate `object` which `std` depends on
+// CHECK: .*<i>Traits</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Constant.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Constant.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Traits</i>.*
+// CHECK-L: Unhandled exception: System.InvalidOperationException: Operation is not valid due to the current state of the object.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Unsupported:\ <i>Cannot\ assign\ null\ value\ to\ variable</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesCompile.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesCompile.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: could not compile `once_cell` (lib)
+// CHECK-L: error[E0072]: recursive type `List` has infinite size
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/FlyingRobots.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/FlyingRobots.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `Rc<Bot>: DafnyType` is not satisfied
+// CHECK-L: error[E0277]: the trait bound `Bot: Clone` is not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/NatList.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/NatList.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0786]: found invalid metadata files for crate `core`
+// CHECK: .*<i>Type\ variance\ Co\ not\ supported</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression7.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression7.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0786]: found invalid metadata files for crate `core`
+// CHECK-L: error[E0072]: recursive type `List` has infinite size
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression9.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression9.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `dyn for<'a> Fn(&'a DafnyInt) -> DafnyChar: Default` is not satisfied
+// CHECK-L: Unhandled exception: System.IO.IOException: The process cannot access the file 'C:\vscode\settings.json' because it is being used by another process.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/UnionFind.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/UnionFind.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0369]: binary operation `<` cannot be applied to type `&nat`
+// CHECK-L: error[E0072]: recursive types `Contents` and `Element` have infinite size
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0786]: found invalid metadata files for crate `core`
+// CHECK: .*<i>Traits</i>.*
diff --git a/...ntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1Expressions.dfy.rs.check b/...ntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1Expressions.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: could not compile `paste` (lib)
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/FIFO.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/FIFO.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/LIFO.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/LIFO.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine2.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine2.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: missing angle brackets in associated item path
+// CHECK-L: error[E0369]: cannot add `DafnyInt` to `nat`
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine3.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine3.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ghost/Comp.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ghost/Comp.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1029.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1029.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: missing angle brackets in associated item path
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1185.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1185.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0277]: the trait bound `_T0: Hash` is not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Unsupported:\ Cannot\ emit\ literal\ expression\ 0\ outside\ of\ expression\ context:\ Microsoft_dDafny_dCompilers_dBuilderSyntaxTree'1\[Microsoft_dDafny_dCompilers_dStatementContainer]</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514b.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514b.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Unsupported:\ Cannot\ emit\ literal\ expression\ 0\ outside\ of\ expression\ context:\ Microsoft_dDafny_dCompilers_dBuilderSyntaxTree'1\[Microsoft_dDafny_dCompilers_dStatementContainer]</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514c.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514c.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Unsupported:\ Cannot\ emit\ literal\ expression\ 0\ outside\ of\ expression\ context:\ Microsoft_dDafny_dCompilers_dBuilderSyntaxTree'1\[Microsoft_dDafny_dCompilers_dStatementContainer]</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1553.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1553.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `_R: DafnyType` is not satisfied
+// CHECK-L: error[E0277]: the trait bound `_R: Default` is not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1604.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1604.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: Unhandled exception: System.InvalidOperationException: Unknown buildable type: NULL
+// CHECK: .*<i>Unsupported:\ <i>Cannot\ assign\ null\ value\ to\ variable</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1607.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1607.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `&bool: DafnyPrint` is not satisfied
+// CHECK-L: error[E0599]: the method `as_ref` exists for reference `&D`, but its trait bounds were not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1714.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1714.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: Unhandled exception: System.InvalidOperationException: Unknown buildable type: NULL
+// CHECK: .*<i>Traits</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1852.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1852.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1903.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1903.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1909.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1909.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: missing angle brackets in associated item path
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2173.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2173.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0308]: mismatched types
+// CHECK-L: error[E0072]: recursive type `T` has infinite size
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2510.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2510.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Type\ variance\ Co\ not\ supported</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2581.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2581.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0369]: binary operation `==` cannot be applied to type `Sequence<_T>`
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-261.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-261.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Coercion\ from\ \(::dafny_runtime::DafnyInt,\ ::dafny_runtime::DafnyInt\)\ to\ \(super::_System::nat,\ super::_System::na\.\.\..*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-262.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-262.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: missing angle brackets in associated item path
+// CHECK-L: error[E0369]: cannot add `DafnyInt` to `nat`
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2708.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2708.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2726a.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2726a.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2792.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2792.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Cannot\ assign\ null\ value\ to\ variable</i>.*
+// CHECK: .*<i>Static\ functions\ with\ type\ arguments</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3734.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3734.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0433]: failed to resolve: use of undeclared crate or module `num`
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3868.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3868.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Type\ variance\ Co\ not\ supported</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3883.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3883.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Traits</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4141.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4141.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Type parameter Equality support Required not supported for type parameters</i>.*
+// CHECK: .*<i>Coercion\ from\ ::\.\.\..*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-443.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-443.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446a.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446a.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0599]: no associated item named `_allocated` found for struct `A` in the current scope
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446b.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446b.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-452.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-452.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-452c.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-452c.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5065.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5065.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0308]: mismatched types
+// CHECK-L: error[E0107]: method takes 0 generic arguments but 1 generic argument was supplied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5092.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5092.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: missing angle brackets in associated item path
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-686.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-686.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: missing angle brackets in associated item path
+// CHECK-L: error[E0599]: the method `as_ref` exists for reference `&Color`, but its trait bounds were not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697b.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697b.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Unsupported:\ <i>Cannot\ assign\ null\ value\ to\ variable</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697f.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697f.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error: missing angle brackets in associated item path
+// CHECK-L: error[E0277]: the trait bound `EvenCell: num_traits::sign::Signed` is not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697k.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697k.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Cannot\ assign\ null\ value\ to\ variable</i>.*
+// CHECK: .*<i>Traits</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-701.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-701.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Traits</i>.*
+// CHECK-L: Unhandled exception: System.InvalidOperationException: Operation is not valid due to the current state of the object.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-731.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-731.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Traits</i>.*
+// CHECK-L: Unhandled exception: System.InvalidOperationException: Operation is not valid due to the current state of the object.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-731b.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-731b.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Traits</i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-817a.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-817a.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0599]: no method named `borrow_mut` found for struct `DafnyInt` in the current scope
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-864rr.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-864rr.dfy.rs.check
diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-a.dfy.rs.check b/...e/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-a.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `Rc<Tree>: DafnyType` is not satisfied
+// CHECK-L: error[E0308]: mismatched types
diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-b.dfy.rs.check b/...e/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-b.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `Rc<Tree>: DafnyType` is not satisfied
+// CHECK-L: error[E0308]: mismatched types
diff --git a/...e/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-c.dfy.rs.check b/...e/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-c.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: the trait bound `Rc<Tree>: DafnyType` is not satisfied
+// CHECK-L: error[E0308]: mismatched types
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3871.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3871.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0070]: invalid left-hand side of assignment
+// CHECK-L: error[E0277]: the trait bound `RefCell<Vec<DafnyInt>>: Hash` is not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4483.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4483.dfy.rs.check
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Compilation.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Compilation.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0277]: the trait bound `dyn for<'a> Fn(&'a DafnyInt) -> DafnyInt: Default` is not satisfied
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Fold.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Fold.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK-L: error[E0072]: recursive type `List` has infinite size
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Renaming.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Renaming.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0782]: trait objects must include the `dyn` keyword
+// CHECK-L: error[E0631]: type mismatch in closure arguments
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/TreeMapSimple.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/TreeMapSimple.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Coercion\ from\ ::std::rc::Rc<dyn\ ::std::ops::Fn\(&super::_module::Tree<_A>\)\ ->\ super::_module::Tree<_B>>\ to\ ::std::rc::Rc<dyn\ ::std::ops::Fn\(&_A\)\ ->\ _B></i>.*
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/OrPatterns.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/OrPatterns.dfy.rs.check
@@ -1 +1 @@
-// CHECK-L: error[E0277]: can't compare `&DafnyInt` with `DafnyInt`
+// CHECK-L: error[E0072]: recursive type `List` has infinite size
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/PatternMatching.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/PatternMatching.dfy.rs.check
@@ -1 +1 @@
-// CHECK: .*<i>Coercion</i>.*
+// CHECK: .*<i>Coercion\ from\ super::_module::List<::dafny_runtime::DafnyInt>\ to\ super::_module::List<super::_System::nat></i>.*