Regenerate the tests

AeneasVerif · Jan 8, 2025 · a7746fe · a7746fe
1 parent 7487a67
commit a7746fe
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out
@@ -1,5 +1,5 @@
 [[92mInfo[39m ] Imported: tests/llbc/loops_borrow_check_fail.llbc
 [[91mError[39m] Can not apply a projection to the ⊥ value
 Source: 'tests/src/loops-borrow-check-fail.rs', lines 8:10-8:13
-[[91mError[39m] Can not apply a projection to the ⊥ value
-Source: 'tests/src/loops-borrow-check-fail.rs', lines 19:12-19:17
+[[91mError[39m] Unexpected
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 18:4-20:5
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
@@ -14,4 +14,4 @@ Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 886, characters 2-177
 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1018, characters 2-36
 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1652, characters 5-42
-Called from Dune__exe__Main in file "Main.ml", line 493, characters 11-63
+Called from Dune__exe__Main in file "Main.ml", line 564, characters 11-63