diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index dd6909483694..10df35d34d62 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -247,6 +247,24 @@ pub mod rustc_smir {
         region_from_coverage(tcx, bcb, instance)
     }
 
+    pub fn merge_source_region(source_regions: Vec<SourceRegion>) -> SourceRegion {
+        let start_line = source_regions.iter().map(|sr| sr.start_line).min().unwrap();
+        let start_col = source_regions
+            .iter()
+            .filter(|sr| sr.start_line == start_line)
+            .map(|sr| sr.start_col)
+            .min()
+            .unwrap();
+        let end_line = source_regions.iter().map(|sr| sr.end_line).max().unwrap();
+        let end_col = source_regions
+            .iter()
+            .filter(|sr| sr.end_line == end_line)
+            .map(|sr| sr.end_col)
+            .max()
+            .unwrap();
+        SourceRegion { start_line, start_col, end_line, end_col }
+    }
+
     /// Retrieves the `SourceRegion` associated with a `BasicCoverageBlock` object.
     ///
     /// Note: This function could be in the internal `rustc` impl for `Coverage`.
@@ -258,22 +276,25 @@ pub mod rustc_smir {
         // We need to pull the coverage info from the internal MIR instance.
         let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
         let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
-
+        let filename = rustc_internal::stable(body.span).get_filename();
         // Some functions, like `std` ones, may not have coverage info attached
         // to them because they have been compiled without coverage flags.
         if let Some(cov_info) = &body.function_coverage_info {
             // Iterate over the coverage mappings and match with the coverage term.
+            let mut source_regions: Vec<SourceRegion> = Vec::new();
             for mapping in &cov_info.mappings {
                 let Code { bcb } = mapping.kind else { unreachable!() };
                 let source_map = tcx.sess.source_map();
                 let file = source_map.lookup_source_file(mapping.span.lo());
-                if bcb == coverage {
-                    return Some((
-                        make_source_region(source_map, &file, mapping.span).unwrap(),
-                        rustc_internal::stable(mapping.span).get_filename(),
-                    ));
+                if bcb == coverage
+                    && let Some(source_region) = make_source_region(source_map, &file, mapping.span)
+                {
+                    source_regions.push(source_region);
                 }
             }
+            if !source_regions.is_empty() {
+                return Some((merge_source_region(source_regions), filename));
+            }
         }
         None
     }
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 0fb26468fadc..f1eb90721eb6 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-05-06"
+channel = "nightly-2025-05-07"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected
index 0334841a880e..ae63575af3bc 100644
--- a/tests/coverage/abort/expected
+++ b/tests/coverage/abort/expected
@@ -8,7 +8,7 @@
    8|     | #[kani::proof]\
    9|    1| fn main() {\
   10|    1|     for i in 0..4 {\
-  11|     |         if i == 1 {\
+  11|    1|         if i == 1 {\
   12|     |             // This comes first and it should be reachable.\
   13|    1|             process::abort();\
   14|    1|         }\
diff --git a/tests/coverage/assert_eq/expected b/tests/coverage/assert_eq/expected
index 0cc1e01fbca9..8665bb8bcbeb 100644
--- a/tests/coverage/assert_eq/expected
+++ b/tests/coverage/assert_eq/expected
@@ -5,7 +5,7 @@
    5|    1| fn main() {\
    6|    1|     let x: i32 = kani::any();\
    7|    1|     let y = if x > 10 { 15 } else { 33 };\
-   8|    0|     if y > 50 ```{'''\
+   8|    1|     if y > 50 ```{'''\
    9|    0| ```        assert_eq!(y, 55);'''\
   10|    1| ```    }'''\
   11|     | }\
diff --git a/tests/coverage/break/expected b/tests/coverage/break/expected
index e1570030f6ae..25d192336b7c 100644
--- a/tests/coverage/break/expected
+++ b/tests/coverage/break/expected
@@ -3,7 +3,7 @@
    3|     | \
    4|    1| fn find_positive(nums: &[i32]) -> Option<i32> {\
    5|    1|     for &num in nums {\
-   6|     |         if num > 0 {\
+   6|    1|         if num > 0 {\
    7|    1|             return Some(num);\
    8|    1|         } \
    9|     |     }\
diff --git a/tests/coverage/debug-assert/expected b/tests/coverage/debug-assert/expected
index 82ad7c992ca3..d36fc11843d0 100644
--- a/tests/coverage/debug-assert/expected
+++ b/tests/coverage/debug-assert/expected
@@ -9,7 +9,7 @@
    9|     | #[kani::proof]\
   10|    1| fn main() {\
   11|    1|     for i in 0..4 {\
-  12|    0|         debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
+  12|    1|         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/early-return/expected b/tests/coverage/early-return/expected
index efdd71ee91f0..4df1f1922603 100644
--- a/tests/coverage/early-return/expected
+++ b/tests/coverage/early-return/expected
@@ -3,7 +3,7 @@
    3|     | \
    4|    1| fn find_index(nums: &[i32], target: i32) -> Option<usize> {\
    5|    1|     for (index, &num) in nums.iter().enumerate() {\
-   6|     |         if num == target {\
+   6|    1|         if num == target {\
    7|    1|             return Some(index);\
    8|    1|         } \
    9|     |     }\