diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index 720a3981d3c..9fe42bddd18 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -94,12 +94,12 @@ INCLUDES= -I ..
 
 LIBS =
 
-CLEANFILES = goto-instrument$(EXEEXT)
+CLEANFILES = goto-instrument$(EXEEXT) goto-instrument$(LIBEXT)
 
 include ../config.inc
 include ../common
 
-all: goto-instrument$(EXEEXT)
+all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT)
 
 ifneq ($(LIB_GLPK),)
   LIBS += $(LIB_GLPK)
@@ -111,6 +111,9 @@ endif
 goto-instrument$(EXEEXT): $(OBJ)
 	$(LINKBIN)
 
+goto-instrument$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+
 .PHONY: goto-instrument-mac-signed
 
 goto-instrument-mac-signed: goto-instrument$(EXEEXT)
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
index 166c1f8c894..21316d73a38 100644
--- a/unit/CMakeLists.txt
+++ b/unit/CMakeLists.txt
@@ -36,7 +36,16 @@ target_include_directories(unit
     ${CBMC_SOURCE_DIR}
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
-target_link_libraries(unit testing-utils ansi-c solvers java_bytecode)
+target_link_libraries(
+        unit
+        testing-utils
+        ansi-c
+        solvers
+        java_bytecode
+        goto-programs
+        goto-instrument-lib
+)
+
 add_test(
     NAME unit
     COMMAND $<TARGET_FILE:unit>
diff --git a/unit/Makefile b/unit/Makefile
index 16f985fa47a..100bd0a1edd 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -67,6 +67,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               ../src/util/util$(LIBEXT) \
               ../src/big-int/big-int$(LIBEXT) \
               ../src/goto-programs/goto-programs$(LIBEXT) \
+              ../src/goto-instrument/goto-instrument$(LIBEXT) \
               ../src/pointer-analysis/pointer-analysis$(LIBEXT) \
               ../src/langapi/langapi$(LIBEXT) \
               ../src/assembler/assembler$(LIBEXT) \
diff --git a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
index 128c19b2e5b..5f61d323142 100644
--- a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
+++ b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
@@ -8,13 +8,13 @@
 
 #include <testing-utils/catch.hpp>
 #include <testing-utils/load_java_class.h>
-#include <testing-utils/require_goto_statements.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <util/config.h>
-
-#include <util/std_expr.h>
+#include <goto-instrument/cover.h>
+#include <util/options.h>
+#include <iostream>
 
 void check_function_call(
   const equal_exprt &eq_expr,
@@ -115,6 +115,55 @@ SCENARIO(
       }
 
       REQUIRE(found_function);
+
+      WHEN("basic blocks are instrumented")
+      {
+        optionst options;
+        options.set_option("cover", "location");
+        REQUIRE_FALSE(
+          instrument_cover_goals(
+            options, new_table, new_goto_functions, null_output));
+
+        auto function = new_goto_functions.function_map.find(function_name);
+        REQUIRE(function != new_goto_functions.function_map.end());
+
+        const goto_programt &goto_program = function->second.body;
+        auto it = goto_program.instructions.begin();
+        REQUIRE(it != goto_program.instructions.end());
+
+        // Skip the first instruction which is a declaration with no location
+        ++it;
+
+        THEN("Each instruction with a new bytecode index begins with ASSERT"
+               " and coverage assertions are at the beginning of the block")
+        {
+          irep_idt current_index;
+
+          while(it->type != goto_program_instruction_typet::END_FUNCTION)
+          {
+            const source_locationt &loc = it->source_location;
+            REQUIRE(loc != source_locationt::nil());
+            REQUIRE(!loc.get_java_bytecode_index().empty());
+            const auto new_index = loc.get_java_bytecode_index();
+
+            if(new_index != current_index)
+            {
+              current_index = new_index;
+              // instruction with a new bytecode index begins with ASSERT
+              REQUIRE(it->type == goto_program_instruction_typet::ASSERT);
+              // the assertion corresponds to a line coverage goal
+              REQUIRE(!loc.get_basic_block_covered_lines().empty());
+            }
+            else
+            {
+              // there is no line coverage goal in the middle of a block
+              REQUIRE(loc.get_basic_block_covered_lines().empty());
+            }
+
+            ++it;
+          }
+        }
+      }
     }
   }
 }