diff --git a/regression/cbmc-cover/location12/test.desc b/regression/cbmc-cover/location12/test.desc
index bac822b042c7..6cc5084011fa 100644
--- a/regression/cbmc-cover/location12/test.desc
+++ b/regression/cbmc-cover/location12/test.desc
@@ -7,7 +7,8 @@ main.c
 ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: SATISFIED$
 ^\[foo.coverage.2\] file main.c line 4 function foo block 2.*: FAILED$
-^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: SATISFIED$
-^\*\* 4 of 5 covered \(80.0%\)
+^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: FAILED$
+^\[foo.coverage.4\] file main.c line 5 function foo block 4.*: SATISFIED$
+^\*\* 4 of 6 covered \(66.7%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc
index b48161384c3d..90cf7a9f26d1 100644
--- a/regression/cbmc-cover/location15/test.desc
+++ b/regression/cbmc-cover/location15/test.desc
@@ -6,7 +6,8 @@ main.c
 ^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$
 ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
 ^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$
-^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 14 function main block 4.*: FAILED$
+^\[main.coverage.5\] file main.c line 16 function main block 5.*: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$
 ^\*\* 3 of \d+ covered
 --
diff --git a/regression/cbmc-cover/location16/test.desc b/regression/cbmc-cover/location16/test.desc
index 74d7080448c9..40e65248f262 100644
--- a/regression/cbmc-cover/location16/test.desc
+++ b/regression/cbmc-cover/location16/test.desc
@@ -9,7 +9,8 @@ main.c
 ^\[func.coverage.2\] file main.c line 6 function func block 2.*: FAILED$
 ^\[func.coverage.3\] file main.c line 8 function func block 3.*: FAILED$
 ^\[func.coverage.4\] file main.c line 12 function func block 4.*: FAILED$
-^\[func.coverage.5\] file main.c line 15 function func block 5.*: SATISFIED$
-^\*\* 4 of 7 covered \(57.1%\)
+^\[func.coverage.5\] file main.c line 14 function func block 5.*: FAILED$
+^\[func.coverage.6\] file main.c line 15 function func block 6.*: SATISFIED$
+^\*\* 4 of 8 covered \(50.0%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location2/test.desc b/regression/cbmc-cover/location2/test.desc
index 747ff0c58009..817de5431b91 100644
--- a/regression/cbmc-cover/location2/test.desc
+++ b/regression/cbmc-cover/location2/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 9 function main block 1 \(lines main.c:main:9,10\): SATISFIED$
-^\[main.coverage.2\] file main.c line 11 function main block 2 \(lines main.c:main:11\): SATISFIED$
-^\*\* 2 of 2 covered \(100.0%\)
+^\[main.coverage.3\] file main.c line 11 function main block 3 \(lines main.c:main:11\): SATISFIED$
+^\*\* 3 of 3 covered \(100.0%\)
 --
 ^warning: ignoring
 main.c::5
diff --git a/regression/cbmc-cover/simple_assert/test.desc b/regression/cbmc-cover/simple_assert/test.desc
index d3fac6c4c466..dfdc0dee6f96 100644
--- a/regression/cbmc-cover/simple_assert/test.desc
+++ b/regression/cbmc-cover/simple_assert/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.coverage\.1\] .* function main block 1.*: SATISFIED$
-(1 of 1|3 of 3) covered \(100\.0%\)$
+(1 of 1|2 of 2|3 of 3) covered \(100\.0%\)$
 --
 ^warning: ignoring
 ^CONVERSION ERROR$
diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc
index 9f7882b842f8..efa75799614a 100644
--- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc
+++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc
@@ -1,9 +1,10 @@
 CORE paths-lifo-expected-failure new-smt-backend
 test.c
 --cover location --pointer-check --malloc-may-fail --malloc-fail-null
-\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED
-\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED
-\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED
+\[main\.coverage\.5\] file test\.c line \d+ function main block 5 \(lines test\.c:main:17,18\): SATISFIED
+\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:15\): FAILED
+\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:12,14\): SATISFIED
+\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12\): SATISFIED
 \[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp
index 81ff18b6b119..c290a1c3ce93 100644
--- a/src/goto-instrument/cover_basic_blocks.cpp
+++ b/src/goto-instrument/cover_basic_blocks.cpp
@@ -29,15 +29,34 @@ optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
   return {};
 }
 
+static bool
+same_source_line(const source_locationt &a, const source_locationt &b)
+{
+  return a.get_file() == b.get_file() && a.get_line() == b.get_line();
+}
+
 cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
 {
   bool next_is_target = true;
+  const goto_programt::instructiont *preceding_assume = nullptr;
   std::size_t current_block = 0;
 
   forall_goto_program_instructions(it, goto_program)
   {
+    // For the purposes of coverage blocks, multiple consecutive assume
+    // instructions with the same source location are considered to be part of
+    // the same block. Assumptions should terminate a block, as subsequent
+    // instructions may be unreachable. However check instrumentation passes
+    // may insert multiple assertions in the same program location. Therefore
+    // these are combined for reasons of readability of the coverage output.
+    bool end_of_assume_group =
+      preceding_assume &&
+      !(it->is_assume() &&
+        same_source_line(
+          preceding_assume->source_location(), it->source_location()));
+
     // Is it a potential beginning of a block?
-    if(next_is_target || it->is_target())
+    if(next_is_target || it->is_target() || end_of_assume_group)
     {
       if(auto block_number = continuation_of_block(it, block_map))
       {
@@ -72,13 +91,8 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
       block_info.source_location = it->source_location();
     }
 
-    next_is_target =
-#if 0
-      // Disabled for being too messy
-      it->is_goto() || it->is_function_call() || it->is_assume();
-#else
-      it->is_goto() || it->is_function_call();
-#endif
+    next_is_target = it->is_goto() || it->is_function_call();
+    preceding_assume = it->is_assume() ? &*it : nullptr;
   }
 }