diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs
index 4eb1a0720f22..c7363a09d109 100644
--- a/cprover_bindings/src/irep/goto_binary_serde.rs
+++ b/cprover_bindings/src/irep/goto_binary_serde.rs
@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! GOTO binary serializer.
 
+use tracing::debug;
+
 use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
 use crate::{InternString, InternedString};
 use std::collections::HashMap;
@@ -23,6 +25,8 @@ pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::Sym
     let mut writer = BufWriter::new(out_file);
     let mut serializer = GotoBinarySerializer::new(&mut writer);
     let irep_symbol_table = &source.to_irep();
+    debug!("SYMTAB: {irep_symbol_table:?}");
+    // debug!("SYMTAB: {source:?}");
     serializer.write_file(irep_symbol_table);
 }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index e7b7ee5a376a..2233751b104a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -93,13 +93,18 @@ impl<'tcx> GotocCtx<'tcx> {
                     "assumption failed",
                     location,
                 )
-            }
+            },
+            StatementKind::Coverage(opaque) => {
+            debug!(?opaque, "StatementKind::Coverage Opaque");
+            self.codegen_coverage(stmt.span)
+            // let coverage_stmt = self.codegen_coverage(stmt.span);
+            // Stmt::block(vec![coverage_stmt], location)
+            },
             StatementKind::PlaceMention(_) => todo!(),
             StatementKind::FakeRead(..)
             | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType { .. }
             | StatementKind::Nop
-            | StatementKind::Coverage { .. }
             | StatementKind::ConstEvalCounter => Stmt::skip(location),
         }
         .with_location(location)
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 9b6e0598daa5..f1b3591868ac 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -116,6 +116,10 @@ impl KaniSession {
         // We only use panic abort strategy for verification since we cannot handle unwind logic.
         flags.extend_from_slice(
             &[
+                "-C",
+                "instrument-coverage",
+                "-Z",
+                "no-profiler-runtime",
                 "-C",
                 "panic=abort",
                 "-C",