diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected
index 0570f1e3f710..a5df4acee287 100644
--- a/tests/coverage/abort/expected
+++ b/tests/coverage/abort/expected
@@ -1,22 +1,21 @@
-/home/ubuntu/kani/tests/coverage/abort/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|     | //! Test that the abort() function is respected and nothing beyond it will execute.
-   5|     | 
-   6|     | use std::process;
-   7|     | 
-   8|     | #[kani::proof]
-   9|    2| fn main() {
-  10|    2|     for i in 0..4 {
-  11|     |         if i == 1 {
-  12|     |             // This comes first and it should be reachable.
-  13|    2|             process::abort();
-  14|    2|         }
-  15|    2|         if i == 2 {
-  16|     |             // This should never happen.
-  17|    0|             process::exit(1);
-  18|    2|         }
-  19|     |     }
-  20|    0|     ```assert!'''(false, ```"This is unreachable"''');
-  21|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Test that the abort() function is respected and nothing beyond it will execute.\
+   5|     | \
+   6|     | use std::process;\
+   7|     | \
+   8|     | #[kani::proof]\
+   9|    2| fn main() {\
+  10|    2|     for i in 0..4 {\
+  11|     |         if i == 1 {\
+  12|     |             // This comes first and it should be reachable.\
+  13|    2|             process::abort();\
+  14|    2|         }\
+  15|    2|         if i == 2 {\
+  16|     |             // This should never happen.\
+  17|    0|             process::exit(1);\
+  18|    2|         }\
+  19|     |     }\
+  20|    0|     ```assert!'''(false, ```"This is unreachable"''');\
+  21|     | }\
diff --git a/tests/coverage/assert/expected b/tests/coverage/assert/expected
index e066d470cd9b..8825a53c0d07 100644
--- a/tests/coverage/assert/expected
+++ b/tests/coverage/assert/expected
@@ -1,19 +1,18 @@
-/home/ubuntu/kani/tests/coverage/assert/test.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|     | #[kani::proof]
-   5|    2| fn foo() {
-   6|    2|     let x: i32 = kani::any();
-   7|    2|     if x > 5 {
-   8|     |         // fails
-   9|    2|         assert!(x < 4);
-  10|    2|         if x < 3 ```{'''
-  11|    0| ```            // unreachable'''
-  12|    0| ```            assert!(x == 2);'''
-  13|    0| ```        }'''
-  14|    2|     } else {
-  15|    2|         // passes
-  16|    2|         assert!(x <= 5);
-  17|    2|     }
-  18|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | #[kani::proof]\
+   5|    2| fn foo() {\
+   6|    2|     let x: i32 = kani::any();\
+   7|    2|     if x > 5 {\
+   8|     |         // fails\
+   9|    2|         assert!(x < 4);\
+  10|    2|         if x < 3 ```{'''\
+  11|    0| ```            // unreachable'''\
+  12|    0| ```            assert!(x == 2);'''\
+  13|    0| ```        }'''\
+  14|    2|     } else {\
+  15|    2|         // passes\
+  16|    2|         assert!(x <= 5);\
+  17|    2|     }\
+  18|     | }\
diff --git a/tests/coverage/assert_eq/expected b/tests/coverage/assert_eq/expected
index 7d5a91d46771..851d079661ec 100644
--- a/tests/coverage/assert_eq/expected
+++ b/tests/coverage/assert_eq/expected
@@ -1,12 +1,11 @@
-/home/ubuntu/kani/tests/coverage/assert_eq/test.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|     | #[kani::proof]
-   5|    2| fn main() {
-   6|    2|     let x: i32 = kani::any();
-   7|    2|     let y = if x > 10 { 15 } else { 33 };
-   8|    0|     if y > 50 ```{'''
-   9|    0| ```        assert_eq!(y, 55);'''
-  10|    2| ```    }'''
-  11|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | #[kani::proof]\
+   5|    2| fn main() {\
+   6|    2|     let x: i32 = kani::any();\
+   7|    2|     let y = if x > 10 { 15 } else { 33 };\
+   8|    0|     if y > 50 ```{'''\
+   9|    0| ```        assert_eq!(y, 55);'''\
+  10|    2| ```    }'''\
+  11|     | }\
diff --git a/tests/coverage/assert_ne/expected b/tests/coverage/assert_ne/expected
index d29a77afeb5f..ede0547016c4 100644
--- a/tests/coverage/assert_ne/expected
+++ b/tests/coverage/assert_ne/expected
@@ -1,15 +1,14 @@
-/home/ubuntu/kani/tests/coverage/assert_ne/test.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|     | #[kani::proof]
-   5|    2| fn main() {
-   6|    2|     let x: u32 = kani::any();
-   7|    2|     if x > 0 {
-   8|    2|         let y = x / 2;
-   9|    2|         // y is strictly less than x
-  10|    2|         if y == x ```{'''
-  11|    0| ```            assert_ne!(y, 1);'''
-  12|    2| ```        }'''
-  13|    2|     }
-  14|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | #[kani::proof]\
+   5|    2| fn main() {\
+   6|    2|     let x: u32 = kani::any();\
+   7|    2|     if x > 0 {\
+   8|    2|         let y = x / 2;\
+   9|    2|         // y is strictly less than x\
+  10|    2|         if y == x ```{'''\
+  11|    0| ```            assert_ne!(y, 1);'''\
+  12|    2| ```        }'''\
+  13|    2|     }\
+  14|     | }\
diff --git a/tests/coverage/break/expected b/tests/coverage/break/expected
index aca305b0f411..fbf1ddf75436 100644
--- a/tests/coverage/break/expected
+++ b/tests/coverage/break/expected
@@ -1,20 +1,19 @@
-/home/ubuntu/kani/tests/coverage/break/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|    2| fn find_positive(nums: &[i32]) -> Option<i32> {
-   5|    2|     for &num in nums {
-   6|     |         if num > 0 {
-   7|    2|             return Some(num);
-   8|    2|         }
-   9|     |     }
-  10|     |     // `None` is unreachable because there is at least one positive number.
-  11|    0|     None
-  12|     | }
-  13|     | 
-  14|     | #[kani::proof]
-  15|    2| fn main() {
-  16|    2|     let numbers = [-3, -1, 0, 2, 4];
-  17|    2|     let result = find_positive(&numbers);
-  18|    2|     assert_eq!(result, Some(2));
-  19|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    2| fn find_positive(nums: &[i32]) -> Option<i32> {\
+   5|    2|     for &num in nums {\
+   6|     |         if num > 0 {\
+   7|    2|             return Some(num);\
+   8|    2|         }\
+   9|     |     }\
+  10|     |     // `None` is unreachable because there is at least one positive number.\
+  11|    0|     None\
+  12|     | }\
+  13|     | \
+  14|     | #[kani::proof]\
+  15|    2| fn main() {\
+  16|    2|     let numbers = [-3, -1, 0, 2, 4];\
+  17|    2|     let result = find_positive(&numbers);\
+  18|    2|     assert_eq!(result, Some(2));\
+  19|     | }\
diff --git a/tests/coverage/compare/expected b/tests/coverage/compare/expected
index fc776f1cd4ea..bca5c3d98559 100644
--- a/tests/coverage/compare/expected
+++ b/tests/coverage/compare/expected
@@ -1,17 +1,16 @@
-/home/ubuntu/kani/tests/coverage/compare/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|    2| fn compare(x: u16, y: u16) -> u16 {
-   5|    2|     // The case where `x < y` isn't possible so its region is `UNCOVERED`
-   6|    2|     if x >= y { 1 } else { 0 }
-   7|     | }
-   8|     | 
-   9|     | #[kani::proof]
-  10|    2| fn main() {
-  11|    2|     let x: u16 = kani::any();
-  12|    2|     let y: u16 = kani::any();
-  13|    2|     if x >= y {
-  14|    2|         compare(x, y);
-  15|    2|     }
-  16|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    2| fn compare(x: u16, y: u16) -> u16 {\
+   5|    2|     // The case where `x < y` isn't possible so its region is `UNCOVERED`\
+   6|    2|     if x >= y { 1 } else { 0 }\
+   7|     | }\
+   8|     | \
+   9|     | #[kani::proof]\
+  10|    2| fn main() {\
+  11|    2|     let x: u16 = kani::any();\
+  12|    2|     let y: u16 = kani::any();\
+  13|    2|     if x >= y {\
+  14|    2|         compare(x, y);\
+  15|    2|     }\
+  16|     | }\
diff --git a/tests/coverage/contradiction/expected b/tests/coverage/contradiction/expected
index 5acc7f5c7d4d..ae214727543f 100644
--- a/tests/coverage/contradiction/expected
+++ b/tests/coverage/contradiction/expected
@@ -1,15 +1,14 @@
-/home/ubuntu/kani/tests/coverage/contradiction/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | #[kani::proof]
-   4|    2| fn contradiction() {
-   5|    2|     let x: u8 = kani::any();
-   6|    2|     let mut y: u8 = 0;
-   7|    2|     if x > 5 {
-   8|    2|         if x < 2 ```{'''
-   9|    0| ```            y = x;'''
-  10|    2| ```        }'''
-  11|    2|     } else {
-  12|    2|         assert!(x < 10);
-  13|    2|     }
-  14|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | #[kani::proof]\
+   4|    2| fn contradiction() {\
+   5|    2|     let x: u8 = kani::any();\
+   6|    2|     let mut y: u8 = 0;\
+   7|    2|     if x > 5 {\
+   8|    2|         if x < 2 ```{'''\
+   9|    0| ```            y = x;'''\
+  10|    2| ```        }'''\
+  11|    2|     } else {\
+  12|    2|         assert!(x < 10);\
+  13|    2|     }\
+  14|     | }\
diff --git a/tests/coverage/debug-assert/expected b/tests/coverage/debug-assert/expected
index 7ce531204090..b1b8bd6c7c95 100644
--- a/tests/coverage/debug-assert/expected
+++ b/tests/coverage/debug-assert/expected
@@ -1,16 +1,15 @@
-/home/ubuntu/kani/tests/coverage/debug-assert/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|     | //! This test checks that the regions after the `debug_assert` macro are
-   5|     | //! `UNCOVERED`. In fact, for this example, the region associated to `"This
-   6|     | //! should fail and stop the execution"` is also `UNCOVERED` because the macro
-   7|     | //! calls span two regions each.
-   8|     | 
-   9|     | #[kani::proof]
-  10|    2| fn main() {
-  11|    2|     for i in 0..4 {
-  12|    0|         debug_assert!(i > 0, ```"This should fail and stop the execution"''');
-  13|    0|         ```assert!(i == 0''', ```"This should be unreachable"''');
-  14|     |     }
-  15|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! This test checks that the regions after the `debug_assert` macro are\
+   5|     | //! `UNCOVERED`. In fact, for this example, the region associated to `"This\
+   6|     | //! should fail and stop the execution"` is also `UNCOVERED` because the macro\
+   7|     | //! calls span two regions each.\
+   8|     | \
+   9|     | #[kani::proof]\
+  10|    2| fn main() {\
+  11|    2|     for i in 0..4 {\
+  12|    0|         debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
+  13|    0|         ```assert!(i == 0''', ```"This should be unreachable"''');\
+  14|     |     }\
+  15|     | }\
diff --git a/tests/coverage/div-zero/expected b/tests/coverage/div-zero/expected
index a5a7f94c83fd..9074e6f36d26 100644
--- a/tests/coverage/div-zero/expected
+++ b/tests/coverage/div-zero/expected
@@ -1,12 +1,11 @@
-/home/ubuntu/kani/tests/coverage/div-zero/test.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|    2| fn div(x: u16, y: u16) -> u16 {
-   5|    2|     if y != 0 { x / y } else { 0 }
-   6|     | }
-   7|     | 
-   8|     | #[kani::proof]
-   9|    2| fn main() {
-  10|    2|     div(11, 3);
-  11|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    2| fn div(x: u16, y: u16) -> u16 {\
+   5|    2|     if y != 0 { x / y } else { 0 }\
+   6|     | }\
+   7|     | \
+   8|     | #[kani::proof]\
+   9|    2| fn main() {\
+  10|    2|     div(11, 3);\
+  11|     | }\
diff --git a/tests/coverage/early-return/expected b/tests/coverage/early-return/expected
index 9cb66a254204..7203570b106a 100644
--- a/tests/coverage/early-return/expected
+++ b/tests/coverage/early-return/expected
@@ -1,20 +1,19 @@
-/home/ubuntu/kani/tests/coverage/early-return/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|    2| fn find_index(nums: &[i32], target: i32) -> Option<usize> {
-   5|    2|     for (index, &num) in nums.iter().enumerate() {
-   6|     |         if num == target {
-   7|    2|             return Some(index);
-   8|    2|         }
-   9|     |     }
-  10|    0|     None
-  11|     | }
-  12|     | 
-  13|     | #[kani::proof]
-  14|    2| fn main() {
-  15|    2|     let numbers = [10, 20, 30, 40, 50];
-  16|    2|     let target = 30;
-  17|    2|     let result = find_index(&numbers, target);
-  18|    2|     assert_eq!(result, Some(2));
-  19|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    2| fn find_index(nums: &[i32], target: i32) -> Option<usize> {\
+   5|    2|     for (index, &num) in nums.iter().enumerate() {\
+   6|     |         if num == target {\
+   7|    2|             return Some(index);\
+   8|    2|         }\
+   9|     |     }\
+  10|    0|     None\
+  11|     | }\
+  12|     | \
+  13|     | #[kani::proof]\
+  14|    2| fn main() {\
+  15|    2|     let numbers = [10, 20, 30, 40, 50];\
+  16|    2|     let target = 30;\
+  17|    2|     let result = find_index(&numbers, target);\
+  18|    2|     assert_eq!(result, Some(2));\
+  19|     | }\
diff --git a/tests/coverage/if-statement-multi/expected b/tests/coverage/if-statement-multi/expected
index ee486c9b8975..35dbc31b2423 100644
--- a/tests/coverage/if-statement-multi/expected
+++ b/tests/coverage/if-statement-multi/expected
@@ -1,27 +1,26 @@
-/home/ubuntu/kani/tests/coverage/if-statement-multi/test.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | // kani-flags: --coverage -Zsource-coverage
-   4|     | 
-   5|     | //! Checks that we are covering all regions except
-   6|     | //!  * the `val == 42` condition
-   7|     | //!  * the `false` branch
-   8|     | //!
-   9|     | //! No coverage information is shown for `_other_function` because it's sliced
-  10|     | //! off: <https://github.com/model-checking/kani/issues/3445>
-  11|     | 
-  12|    0| ```fn _other_function() {'''
-  13|    0| ```    println!("Hello, world!");'''
-  14|    0| ```}'''
-  15|     | 
-  16|    2| fn test_cov(val: u32) -> bool {
-  17|    2|     if val < 3 || ```val == 42''' { true } else { ```false''' }
-  18|     | }
-  19|     | 
-  20|     | #[cfg_attr(kani, kani::proof)]
-  21|    2| fn main() {
-  22|    2|     let test1 = test_cov(1);
-  23|    2|     let test2 = test_cov(2);
-  24|    2|     assert!(test1);
-  25|    2|     assert!(test2);
-  26|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | // kani-flags: --coverage -Zsource-coverage\
+   4|     | \
+   5|     | //! Checks that we are covering all regions except\
+   6|     | //!  * the `val == 42` condition\
+   7|     | //!  * the `false` branch\
+   8|     | //!\
+   9|     | //! No coverage information is shown for `_other_function` because it's sliced\
+  10|     | //! off: <https://github.com/model-checking/kani/issues/3445>\
+  11|     | \
+  12|    0| ```fn _other_function() {'''\
+  13|    0| ```    println!("Hello, world!");'''\
+  14|    0| ```}'''\
+  15|     | \
+  16|    2| fn test_cov(val: u32) -> bool {\
+  17|    2|     if val < 3 || ```val == 42''' { true } else { ```false''' }\
+  18|     | }\
+  19|     | \
+  20|     | #[cfg_attr(kani, kani::proof)]\
+  21|    2| fn main() {\
+  22|    2|     let test1 = test_cov(1);\
+  23|    2|     let test2 = test_cov(2);\
+  24|    2|     assert!(test1);\
+  25|    2|     assert!(test2);\
+  26|     | }\
diff --git a/tests/coverage/if-statement/expected b/tests/coverage/if-statement/expected
index fd1dd049975d..ba8de00e08fb 100644
--- a/tests/coverage/if-statement/expected
+++ b/tests/coverage/if-statement/expected
@@ -1,21 +1,20 @@
-/home/ubuntu/kani/tests/coverage/if-statement/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|    2| fn check_number(num: i32) -> &'static str {
-   5|    2|     if num > 0 {
-   6|     |         // The next line is partially covered
-   7|    2|         if num % 2 == 0 { ```"Positive and Even"''' } else { "Positive and Odd" }
-   8|    0|     } else if ```num < 0''' {
-   9|    0|         "Negative"
-  10|     |     } else {
-  11|    0|         "Zero"
-  12|     |     }
-  13|     | }
-  14|     | 
-  15|     | #[kani::proof]
-  16|    2| fn main() {
-  17|    2|     let number = 7;
-  18|    2|     let result = check_number(number);
-  19|    2|     assert_eq!(result, "Positive and Odd");
-  20|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    2| fn check_number(num: i32) -> &'static str {\
+   5|    2|     if num > 0 {\
+   6|     |         // The next line is partially covered\
+   7|    2|         if num % 2 == 0 { ```"Positive and Even"''' } else { "Positive and Odd" }\
+   8|    0|     } else if ```num < 0''' {\
+   9|    0|         "Negative"\
+  10|     |     } else {\
+  11|    0|         "Zero"\
+  12|     |     }\
+  13|     | }\
+  14|     | \
+  15|     | #[kani::proof]\
+  16|    2| fn main() {\
+  17|    2|     let number = 7;\
+  18|    2|     let result = check_number(number);\
+  19|    2|     assert_eq!(result, "Positive and Odd");\
+  20|     | }\
diff --git a/tests/coverage/multiple-harnesses/expected b/tests/coverage/multiple-harnesses/expected
index 58176fc4dca3..432ba426ddd5 100644
--- a/tests/coverage/multiple-harnesses/expected
+++ b/tests/coverage/multiple-harnesses/expected
@@ -1,45 +1,44 @@
-/home/ubuntu/kani/tests/coverage/multiple-harnesses/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|    3| fn estimate_size(x: u32) -> u32 {
-   5|    3|     assert!(x < 4096);
-   6|    3| 
-   7|    3|     if x < 256 {
-   8|    3|         if x < 128 {
-   9|    3|             return 1;
-  10|     |         } else {
-  11|    3|             return 3;
-  12|     |         }
-  13|    3|     } else if x < 1024 {
-  14|    3|         if x > 1022 {
-  15|    3|             return 4;
-  16|     |         } else {
-  17|    3|             return 5;
-  18|     |         }
-  19|     |     } else {
-  20|    3|         if x < 2048 {
-  21|    3|             return 7;
-  22|     |         } else {
-  23|    2|             return 9;
-  24|     |         }
-  25|     |     }
-  26|     | }
-  27|     | 
-  28|     | #[cfg(kani)]
-  29|     | #[kani::proof]
-  30|    2| fn mostly_covered() {
-  31|    2|     let x: u32 = kani::any();
-  32|    2|     kani::assume(x < 2048);
-  33|    2|     let y = estimate_size(x);
-  34|    2|     assert!(y < 10);
-  35|     | }
-  36|     | 
-  37|     | #[cfg(kani)]
-  38|     | #[kani::proof]
-  39|    2| fn fully_covered() {
-  40|    2|     let x: u32 = kani::any();
-  41|    2|     kani::assume(x < 4096);
-  42|    2|     let y = estimate_size(x);
-  43|    2|     assert!(y < 10);
-  44|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    3| fn estimate_size(x: u32) -> u32 {\
+   5|    3|     assert!(x < 4096);\
+   6|    3| \
+   7|    3|     if x < 256 {\
+   8|    3|         if x < 128 {\
+   9|    3|             return 1;\
+  10|     |         } else {\
+  11|    3|             return 3;\
+  12|     |         }\
+  13|    3|     } else if x < 1024 {\
+  14|    3|         if x > 1022 {\
+  15|    3|             return 4;\
+  16|     |         } else {\
+  17|    3|             return 5;\
+  18|     |         }\
+  19|     |     } else {\
+  20|    3|         if x < 2048 {\
+  21|    3|             return 7;\
+  22|     |         } else {\
+  23|    2|             return 9;\
+  24|     |         }\
+  25|     |     }\
+  26|     | }\
+  27|     | \
+  28|     | #[cfg(kani)]\
+  29|     | #[kani::proof]\
+  30|    2| fn mostly_covered() {\
+  31|    2|     let x: u32 = kani::any();\
+  32|    2|     kani::assume(x < 2048);\
+  33|    2|     let y = estimate_size(x);\
+  34|    2|     assert!(y < 10);\
+  35|     | }\
+  36|     | \
+  37|     | #[cfg(kani)]\
+  38|     | #[kani::proof]\
+  39|    2| fn fully_covered() {\
+  40|    2|     let x: u32 = kani::any();\
+  41|    2|     kani::assume(x < 4096);\
+  42|    2|     let y = estimate_size(x);\
+  43|    2|     assert!(y < 10);\
+  44|     | }\
diff --git a/tests/coverage/overflow-failure/expected b/tests/coverage/overflow-failure/expected
index cc07742f3070..e717f072a897 100644
--- a/tests/coverage/overflow-failure/expected
+++ b/tests/coverage/overflow-failure/expected
@@ -1,16 +1,15 @@
-/home/ubuntu/kani/tests/coverage/overflow-failure/test.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|     | //! Checks that Kani reports the correct coverage results in the case of an
-   5|     | //! arithmetic overflow failure (caused by the second call to `cond_reduce`).
-   6|     | 
-   7|    2| fn cond_reduce(thresh: u32, x: u32) -> u32 {
-   8|    2|     if x > thresh { x - 50 } else { x }
-   9|     | }
-  10|     | 
-  11|     | #[kani::proof]
-  12|    2| fn main() {
-  13|    2|     cond_reduce(60, 70);
-  14|    2|     cond_reduce(40, 42);
-  15|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Checks that Kani reports the correct coverage results in the case of an\
+   5|     | //! arithmetic overflow failure (caused by the second call to `cond_reduce`).\
+   6|     | \
+   7|    2| fn cond_reduce(thresh: u32, x: u32) -> u32 {\
+   8|    2|     if x > thresh { x - 50 } else { x }\
+   9|     | }\
+  10|     | \
+  11|     | #[kani::proof]\
+  12|    2| fn main() {\
+  13|    2|     cond_reduce(60, 70);\
+  14|    2|     cond_reduce(40, 42);\
+  15|     | }\
diff --git a/tests/coverage/overflow-full-coverage/expected b/tests/coverage/overflow-full-coverage/expected
index 7f666b5571f7..e25b5740eacd 100644
--- a/tests/coverage/overflow-full-coverage/expected
+++ b/tests/coverage/overflow-full-coverage/expected
@@ -1,18 +1,17 @@
-/home/ubuntu/kani/tests/coverage/overflow-full-coverage/test.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|     | //! Checks that Kani reports all regions as `COVERED` as expected in this case
-   5|     | //! where arithmetic overflow failures are prevented.
-   6|     | 
-   7|    2| fn reduce(x: u32) -> u32 {
-   8|    2|     if x > 1000 { x - 1000 } else { x }
-   9|     | }
-  10|     | 
-  11|     | #[kani::proof]
-  12|    2| fn main() {
-  13|    2|     reduce(7);
-  14|    2|     reduce(33);
-  15|    2|     reduce(728);
-  16|    2|     reduce(1079);
-  17|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Checks that Kani reports all regions as `COVERED` as expected in this case\
+   5|     | //! where arithmetic overflow failures are prevented.\
+   6|     | \
+   7|    2| fn reduce(x: u32) -> u32 {\
+   8|    2|     if x > 1000 { x - 1000 } else { x }\
+   9|     | }\
+  10|     | \
+  11|     | #[kani::proof]\
+  12|    2| fn main() {\
+  13|    2|     reduce(7);\
+  14|    2|     reduce(33);\
+  15|    2|     reduce(728);\
+  16|    2|     reduce(1079);\
+  17|     | }\
diff --git a/tests/coverage/while-loop-break/expected b/tests/coverage/while-loop-break/expected
index 574875ac558b..d6bf62ff23d0 100644
--- a/tests/coverage/while-loop-break/expected
+++ b/tests/coverage/while-loop-break/expected
@@ -1,24 +1,23 @@
-/home/ubuntu/kani/tests/coverage/while-loop-break/main.rs
-   1|     | // Copyright Kani Contributors
-   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT
-   3|     | 
-   4|     | //! Checks coverage results in an example with a `while` loop that returns before
-   5|     | //! running the last iteration.
-   6|     | 
-   7|    2| fn find_first_negative(nums: &[i32]) -> Option<i32> {
-   8|    2|     let mut index = 0;
-   9|    2|     while index < nums.len() {
-  10|    2|         if nums[index] < 0 {
-  11|    2|             return Some(nums[index]);
-  12|    2|         }
-  13|    2|         index += 1;
-  14|     |     }
-  15|    0|     None
-  16|     | }
-  17|     | 
-  18|     | #[kani::proof]
-  19|    2| fn main() {
-  20|    2|     let numbers = [1, 2, -3, 4, -5];
-  21|    2|     let result = find_first_negative(&numbers);
-  22|    2|     assert_eq!(result, Some(-3));
-  23|     | }
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Checks coverage results in an example with a `while` loop that returns before\
+   5|     | //! running the last iteration.\
+   6|     | \
+   7|    2| fn find_first_negative(nums: &[i32]) -> Option<i32> {\
+   8|    2|     let mut index = 0;\
+   9|    2|     while index < nums.len() {\
+  10|    2|         if nums[index] < 0 {\
+  11|    2|             return Some(nums[index]);\
+  12|    2|         }\
+  13|    2|         index += 1;\
+  14|     |     }\
+  15|    0|     None\
+  16|     | }\
+  17|     | \
+  18|     | #[kani::proof]\
+  19|    2| fn main() {\
+  20|    2|     let numbers = [1, 2, -3, 4, -5];\
+  21|    2|     let result = find_first_negative(&numbers);\
+  22|    2|     assert_eq!(result, Some(-3));\
+  23|     | }\