diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index bcf452602930..27203c7218c6 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -29,7 +29,7 @@ use tracing::debug;
 /// Classifies the type of CBMC `assert`, as different assertions can have different semantics (e.g. cover)
 ///
 /// Each property class should justify its existence with a note about the special handling it recieves.
-#[derive(Debug, Clone, EnumString, AsRefStr)]
+#[derive(Debug, Clone, EnumString, AsRefStr, PartialEq)]
 #[strum(serialize_all = "snake_case")]
 pub enum PropertyClass {
     /// Overflow panics that can be generated by Intrisics.
@@ -45,6 +45,19 @@ pub enum PropertyClass {
     ///
     /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
     Cover,
+    /// The class of checks used for code coverage instrumentation. Only needed
+    /// when working on coverage-related features.
+    ///
+    /// Do not mistake with `Cover`, they are different:
+    ///  - `CodeCoverage` checks have a fixed condition (`false`) and description.
+    ///  - `CodeCoverage` checks are filtered out from verification results and
+    ///    postprocessed to build coverage reports.
+    ///  - `Cover` checks can be added by users (using the `kani::cover` macro),
+    ///    while `CodeCoverage` checks are not exposed to users (i.e., they are
+    ///    automatically added if running with the coverage option).
+    ///
+    /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
+    CodeCoverage,
     /// Ordinary (Rust) assertions and panics.
     ///
     /// SPECIAL BEHAVIOR: These assertion failures should be observable during normal execution of Rust code.
@@ -134,6 +147,21 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc)
     }
 
+    /// Generate a cover statement for code coverage reports.
+    pub fn codegen_coverage(&self, span: Span) -> Stmt {
+        let loc = self.codegen_caller_span(&Some(span));
+        // Should use Stmt::cover, but currently this doesn't work with CBMC
+        // unless it is run with '--cover cover' (see
+        // https://github.com/diffblue/cbmc/issues/6613). So for now use
+        // `assert(false)`.
+        self.codegen_assert(
+            Expr::bool_false(),
+            PropertyClass::CodeCoverage,
+            "code coverage for location",
+            loc,
+        )
+    }
+
     // The above represent the basic operations we can perform w.r.t. assert/assume/cover
     // Below are various helper functions for constructing the above more easily.
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
index b015be5b401c..bc6738e8ead0 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
@@ -16,25 +16,55 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!(?bb, "Codegen basicblock");
         self.current_fn_mut().set_current_bb(bb);
         let label: String = self.current_fn().find_label(&bb);
+        let check_coverage = self.queries.check_coverage;
         // the first statement should be labelled. if there is no statements, then the
         // terminator should be labelled.
         match bbd.statements.len() {
             0 => {
                 let term = bbd.terminator();
                 let tcode = self.codegen_terminator(term);
-                self.current_fn_mut().push_onto_block(tcode.with_label(label));
+                // When checking coverage, the `coverage` check should be
+                // labelled instead.
+                if check_coverage {
+                    let span = term.source_info.span;
+                    let cover = self.codegen_coverage(span);
+                    self.current_fn_mut().push_onto_block(cover.with_label(label));
+                    self.current_fn_mut().push_onto_block(tcode);
+                } else {
+                    self.current_fn_mut().push_onto_block(tcode.with_label(label));
+                }
             }
             _ => {
                 let stmt = &bbd.statements[0];
                 let scode = self.codegen_statement(stmt);
-                self.current_fn_mut().push_onto_block(scode.with_label(label));
+                // When checking coverage, the `coverage` check should be
+                // labelled instead.
+                if check_coverage {
+                    let span = stmt.source_info.span;
+                    let cover = self.codegen_coverage(span);
+                    self.current_fn_mut().push_onto_block(cover.with_label(label));
+                    self.current_fn_mut().push_onto_block(scode);
+                } else {
+                    self.current_fn_mut().push_onto_block(scode.with_label(label));
+                }
 
                 for s in &bbd.statements[1..] {
+                    if check_coverage {
+                        let span = s.source_info.span;
+                        let cover = self.codegen_coverage(span);
+                        self.current_fn_mut().push_onto_block(cover);
+                    }
                     let stmt = self.codegen_statement(s);
                     self.current_fn_mut().push_onto_block(stmt);
                 }
-                let term = self.codegen_terminator(bbd.terminator());
-                self.current_fn_mut().push_onto_block(term);
+                let term = bbd.terminator();
+                if check_coverage {
+                    let span = term.source_info.span;
+                    let cover = self.codegen_coverage(span);
+                    self.current_fn_mut().push_onto_block(cover);
+                }
+                let tcode = self.codegen_terminator(term);
+                self.current_fn_mut().push_onto_block(tcode);
             }
         }
         self.current_fn_mut().reset_current_bb();
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 4bd5566f9d7c..af06c456a7b6 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -188,7 +188,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let a = fargs.remove(0);
                 let b = fargs.remove(0);
                 let div_does_not_overflow = self.div_does_not_overflow(a.clone(), b.clone());
-                let div_overflow_check = self.codegen_assert(
+                let div_overflow_check = self.codegen_assert_assume(
                     div_does_not_overflow,
                     PropertyClass::ArithmeticOverflow,
                     format!("attempt to compute {} which would overflow", intrinsic).as_str(),
diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
index 2a5e4c188578..ef766c562941 100644
--- a/kani-compiler/src/kani_compiler.rs
+++ b/kani-compiler/src/kani_compiler.rs
@@ -349,6 +349,7 @@ impl Callbacks for KaniCompiler {
             let queries = &mut (*self.queries.lock().unwrap());
             queries.emit_vtable_restrictions = matches.get_flag(parser::RESTRICT_FN_PTRS);
             queries.check_assertion_reachability = matches.get_flag(parser::ASSERTION_REACH_CHECKS);
+            queries.check_coverage = matches.get_flag(parser::COVERAGE_CHECKS);
             queries.output_pretty_json = matches.get_flag(parser::PRETTY_OUTPUT_FILES);
             queries.ignore_global_asm = matches.get_flag(parser::IGNORE_GLOBAL_ASM);
             queries.write_json_symtab =
@@ -364,6 +365,7 @@ impl Callbacks for KaniCompiler {
             {
                 queries.stubbing_enabled = true;
             }
+
             debug!(?queries, "config end");
         }
     }
diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs
index b8446bb7a023..44573bf124d8 100644
--- a/kani-compiler/src/kani_queries/mod.rs
+++ b/kani-compiler/src/kani_queries/mod.rs
@@ -28,6 +28,7 @@ pub enum ReachabilityType {
 #[derive(Debug, Default, Clone)]
 pub struct QueryDb {
     pub check_assertion_reachability: bool,
+    pub check_coverage: bool,
     pub emit_vtable_restrictions: bool,
     pub output_pretty_json: bool,
     pub ignore_global_asm: bool,
diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs
index 2ff81a90bc7c..a947fdc61eaa 100644
--- a/kani-compiler/src/parser.rs
+++ b/kani-compiler/src/parser.rs
@@ -28,6 +28,9 @@ pub const RESTRICT_FN_PTRS: &str = "restrict-vtable-fn-ptrs";
 /// Option name used to enable assertion reachability checks.
 pub const ASSERTION_REACH_CHECKS: &str = "assertion-reach-checks";
 
+/// Option name used to enable coverage checks.
+pub const COVERAGE_CHECKS: &str = "coverage-checks";
+
 /// Option name used to use json pretty-print for output files.
 pub const PRETTY_OUTPUT_FILES: &str = "pretty-json-files";
 
@@ -98,6 +101,12 @@ pub fn parser() -> Command {
                 .help("Check the reachability of every assertion.")
                 .action(ArgAction::SetTrue),
         )
+        .arg(
+            Arg::new(COVERAGE_CHECKS)
+                .long(COVERAGE_CHECKS)
+                .help("Check the reachability of every statement.")
+                .action(ArgAction::SetTrue),
+        )
         .arg(
             Arg::new(REACHABILITY)
                 .long(REACHABILITY)
diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs
index 746482c6985e..a4325ca610fa 100644
--- a/kani-driver/src/args/common.rs
+++ b/kani-driver/src/args/common.rs
@@ -44,6 +44,8 @@ pub enum UnstableFeatures {
     ConcretePlayback,
     /// Enable Kani's unstable async library.
     AsyncLib,
+    /// Enable line coverage instrumentation/reports
+    LineCoverage,
 }
 
 impl ValidateArgs for CommonArgs {
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 31cae95e2a61..626f2d81be93 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -300,6 +300,10 @@ pub struct VerificationArgs {
     )]
     pub enable_stubbing: bool,
 
+    /// Enable Kani coverage output alongside verification result
+    #[arg(long, hide_short_help = true)]
+    pub coverage: bool,
+
     /// Arguments to pass down to Cargo
     #[command(flatten)]
     pub cargo: CargoCommonArgs,
@@ -640,6 +644,16 @@ impl ValidateArgs for VerificationArgs {
             }
         }
 
+        if self.coverage
+            && !self.common_args.unstable_features.contains(&UnstableFeatures::LineCoverage)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `--coverage` argument is unstable and requires `-Z \
+            line-coverage` to be used.",
+            ));
+        }
+
         Ok(())
     }
 }
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index daddfdf62f1c..96770d562e79 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -13,7 +13,7 @@ use crate::args::{OutputFormat, VerificationArgs};
 use crate::cbmc_output_parser::{
     extract_results, process_cbmc_output, CheckStatus, ParserItem, Property, VerificationOutput,
 };
-use crate::cbmc_property_renderer::{format_result, kani_cbmc_output_filter};
+use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter};
 use crate::session::KaniSession;
 
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
@@ -303,14 +303,23 @@ impl VerificationResult {
         }
     }
 
-    pub fn render(&self, output_format: &OutputFormat, should_panic: bool) -> String {
+    pub fn render(
+        &self,
+        output_format: &OutputFormat,
+        should_panic: bool,
+        coverage_mode: bool,
+    ) -> String {
         match &self.results {
             Ok(results) => {
                 let status = self.status;
                 let failed_properties = self.failed_properties;
                 let show_checks = matches!(output_format, OutputFormat::Regular);
-                let mut result =
-                    format_result(results, status, should_panic, failed_properties, show_checks);
+
+                let mut result = if coverage_mode {
+                    format_coverage(results, status, should_panic, failed_properties, show_checks)
+                } else {
+                    format_result(results, status, should_panic, failed_properties, show_checks)
+                };
                 writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
                 result
             }
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index caf3dd7339a3..1522071fdefd 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -96,6 +96,10 @@ impl KaniSession {
             flags.push("--enable-stubbing".into());
         }
 
+        if self.args.coverage {
+            flags.push("--coverage-checks".into());
+        }
+
         flags.extend(
             self.args
                 .common_args
diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
index 70e13b7dda06..8bdd45034190 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -96,11 +96,17 @@ pub struct PropertyId {
 
 impl Property {
     const COVER_PROPERTY_CLASS: &str = "cover";
+    const COVERAGE_PROPERTY_CLASS: &str = "code_coverage";
 
     pub fn property_class(&self) -> String {
         self.property_id.class.clone()
     }
 
+    // Returns true if this is a code_coverage check
+    pub fn is_code_coverage_property(&self) -> bool {
+        self.property_id.class == Self::COVERAGE_PROPERTY_CLASS
+    }
+
     /// Returns true if this is a cover property
     pub fn is_cover_property(&self) -> bool {
         self.property_id.class == Self::COVER_PROPERTY_CLASS
@@ -322,11 +328,13 @@ impl std::fmt::Display for TraceData {
 #[serde(rename_all = "UPPERCASE")]
 pub enum CheckStatus {
     Failure,
-    Satisfied, // for cover properties only
+    Covered,   // for `code_coverage` properties only
+    Satisfied, // for `cover` properties only
     Success,
     Undetermined,
     Unreachable,
-    Unsatisfiable, // for cover properties only
+    Uncovered,     // for `code_coverage` properties only
+    Unsatisfiable, // for `cover` properties only
 }
 
 impl std::fmt::Display for CheckStatus {
@@ -334,6 +342,8 @@ impl std::fmt::Display for CheckStatus {
         let check_str = match self {
             CheckStatus::Satisfied => style("SATISFIED").green(),
             CheckStatus::Success => style("SUCCESS").green(),
+            CheckStatus::Covered => style("COVERED").green(),
+            CheckStatus::Uncovered => style("UNCOVERED").red(),
             CheckStatus::Failure => style("FAILURE").red(),
             CheckStatus::Unreachable => style("UNREACHABLE").yellow(),
             CheckStatus::Undetermined => style("UNDETERMINED").yellow(),
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index 8da67dae7ab1..be788c5d1c0c 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -8,7 +8,8 @@ use console::style;
 use once_cell::sync::Lazy;
 use regex::Regex;
 use rustc_demangle::demangle;
-use std::collections::HashMap;
+use std::collections::{BTreeMap, HashMap};
+use strum_macros::{AsRefStr, Display};
 
 type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>;
 
@@ -149,6 +150,15 @@ static CBMC_ALT_DESCRIPTIONS: Lazy<CbmcAltDescriptions> = Lazy::new(|| {
     map
 });
 
+#[derive(PartialEq, Eq, AsRefStr, Clone, Copy, Display)]
+#[strum(serialize_all = "UPPERCASE")]
+// The status of coverage reported by Kani
+enum CoverageStatus {
+    Full,
+    Partial,
+    None,
+}
+
 const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani";
 const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop";
 const UNWINDING_ASSERT_REC_DESC: &str = "recursion unwinding assertion";
@@ -421,6 +431,72 @@ pub fn format_result(
     result_str
 }
 
+/// Separate checks into coverage and non-coverage based on property class and format them separately for --coverage. We report both verification and processed coverage
+/// results
+pub fn format_coverage(
+    properties: &[Property],
+    status: VerificationStatus,
+    should_panic: bool,
+    failed_properties: FailedProperties,
+    show_checks: bool,
+) -> String {
+    let (coverage_checks, non_coverage_checks): (Vec<Property>, Vec<Property>) =
+        properties.iter().cloned().partition(|x| x.property_class() == "code_coverage");
+
+    let verification_output =
+        format_result(&non_coverage_checks, status, should_panic, failed_properties, show_checks);
+    let coverage_output = format_result_coverage(&coverage_checks);
+    let result = format!("{}\n{}", verification_output, coverage_output);
+
+    result
+}
+
+/// Generate coverage result from all coverage properties (i.e., checks with `code_coverage` property class).
+/// Loops through each of the checks with the `code_coverage` property class on a line and gives:
+///  - A status `FULL` if all checks pertaining to a line number are `COVERED`
+///  - A status `NONE` if all checks related to a line are `UNCOVERED`
+///  - Otherwise (i.e., if the line contains both) it reports `PARTIAL`.
+///
+/// Used when the user requests coverage information with `--coverage`.
+/// Output is tested through the `coverage-based` testing suite, not the regular
+/// `expected` suite.
+fn format_result_coverage(properties: &[Property]) -> String {
+    let mut formatted_output = String::new();
+    formatted_output.push_str("\nCoverage Results:\n");
+
+    let mut coverage_results: BTreeMap<String, BTreeMap<usize, CoverageStatus>> =
+        BTreeMap::default();
+    for prop in properties {
+        let src = prop.source_location.clone();
+        let file_entries = coverage_results.entry(src.file.unwrap()).or_default();
+        let check_status = if prop.status == CheckStatus::Covered {
+            CoverageStatus::Full
+        } else {
+            CoverageStatus::None
+        };
+
+        // Create Map<file, Map<line, status>>
+        file_entries
+            .entry(src.line.unwrap().parse().unwrap())
+            .and_modify(|line_status| {
+                if *line_status != check_status {
+                    *line_status = CoverageStatus::Partial
+                }
+            })
+            .or_insert(check_status);
+    }
+
+    // Create formatted string that is returned to the user as output
+    for (file, checks) in coverage_results.iter() {
+        for (line_number, coverage_status) in checks {
+            formatted_output.push_str(&format!("{}, {}, {}\n", file, line_number, coverage_status));
+        }
+        formatted_output.push('\n');
+    }
+
+    formatted_output
+}
+
 /// Attempts to build a message for a failed property with as much detailed
 /// information on the source location as possible.
 fn build_failure_message(description: String, trace: &Option<Vec<TraceItem>>) -> String {
@@ -512,7 +588,8 @@ pub fn postprocess_result(properties: Vec<Property>, extra_ptr_checks: bool) ->
 
     let updated_properties =
         update_properties_with_reach_status(properties_filtered, has_fundamental_failures);
-    update_results_of_cover_checks(updated_properties)
+    let results_after_code_coverage = update_results_of_code_covererage_checks(updated_properties);
+    update_results_of_cover_checks(results_after_code_coverage)
 }
 
 /// Determines if there is property with status `FAILURE` and the given description
@@ -613,6 +690,27 @@ fn update_properties_with_reach_status(
     properties
 }
 
+/// Update the results of `code_coverage` (NOT `cover`) properties.
+/// - `SUCCESS` -> `UNCOVERED`
+/// - `FAILURE` -> `COVERED`
+/// Note that these statuses are intermediate statuses that aren't reported to
+/// users but rather internally consumed and reported finally as `PARTIAL`, `FULL`
+/// or `NONE` based on aggregated line coverage results.
+fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Vec<Property> {
+    for prop in properties.iter_mut() {
+        if prop.is_code_coverage_property() {
+            prop.status = match prop.status {
+                CheckStatus::Success => CheckStatus::Uncovered,
+                CheckStatus::Failure => CheckStatus::Covered,
+                _ => unreachable!(
+                    "status for coverage checks should be either `SUCCESS` or `FAILURE` prior to postprocessing"
+                ),
+            };
+        }
+    }
+    properties
+}
+
 /// Update the results of cover properties.
 /// We encode cover(cond) as assert(!cond), so if the assertion
 /// fails, then the cover property is satisfied and vice versa.
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index fdafa8a5c18b..fa1aef3d763a 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -96,7 +96,11 @@ impl KaniSession {
             if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
                 println!(
                     "{}",
-                    result.render(&self.args.output_format, harness.attributes.should_panic)
+                    result.render(
+                        &self.args.output_format,
+                        harness.attributes.should_panic,
+                        self.args.coverage
+                    )
                 );
             }
             self.gen_and_add_concrete_playback(harness, &mut result)?;
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index fd04b579deb3..01afd6e2de59 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -38,6 +38,7 @@ cargo test -p kani_metadata
 # Declare testing suite information (suite and mode)
 TESTS=(
     "script-based-pre exec"
+    "coverage coverage-based"
     "kani kani"
     "expected expected"
     "ui expected"
diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected
new file mode 100644
index 000000000000..7a9fef1ca77c
--- /dev/null
+++ b/tests/coverage/reachable/assert-false/expected
@@ -0,0 +1,8 @@
+coverage/reachable/assert-false/main.rs, 6, FULL
+coverage/reachable/assert-false/main.rs, 7, FULL
+coverage/reachable/assert-false/main.rs, 11, FULL
+coverage/reachable/assert-false/main.rs, 12, FULL
+coverage/reachable/assert-false/main.rs, 15, FULL
+coverage/reachable/assert-false/main.rs, 16, FULL
+coverage/reachable/assert-false/main.rs, 17, PARTIAL
+coverage/reachable/assert-false/main.rs, 19, FULL
diff --git a/tests/coverage/reachable/assert-false/main.rs b/tests/coverage/reachable/assert-false/main.rs
new file mode 100644
index 000000000000..42563b1cd518
--- /dev/null
+++ b/tests/coverage/reachable/assert-false/main.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the assert is reported as `PARTIAL` for having both `COVERED` and `UNCOVERED` coverage checks
+fn any_bool() -> bool {
+    kani::any()
+}
+
+#[kani::proof]
+fn main() {
+    if any_bool() {
+        assert!(false);
+    }
+
+    if any_bool() {
+        let s = "Fail with custom runtime message";
+        assert!(false, "{}", s);
+    }
+}
diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected
new file mode 100644
index 000000000000..67ae085a3e83
--- /dev/null
+++ b/tests/coverage/reachable/assert/reachable_pass/expected
@@ -0,0 +1,4 @@
+coverage/reachable/assert/reachable_pass/test.rs, 6, FULL
+coverage/reachable/assert/reachable_pass/test.rs, 7, FULL
+coverage/reachable/assert/reachable_pass/test.rs, 8, FULL
+coverage/reachable/assert/reachable_pass/test.rs, 10, FULL
diff --git a/tests/coverage/reachable/assert/reachable_pass/test.rs b/tests/coverage/reachable/assert/reachable_pass/test.rs
new file mode 100644
index 000000000000..72acca2b764c
--- /dev/null
+++ b/tests/coverage/reachable/assert/reachable_pass/test.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn main() {
+    let x: u32 = kani::any_where(|val| *val == 5);
+    if x > 3 {
+        assert!(x > 4); // FULL: `x > 4` since `x = 5`
+    }
+}
diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected
new file mode 100644
index 000000000000..af2f30e51fe2
--- /dev/null
+++ b/tests/coverage/reachable/bounds/reachable_fail/expected
@@ -0,0 +1,4 @@
+coverage/reachable/bounds/reachable_fail/test.rs, 5, PARTIAL
+coverage/reachable/bounds/reachable_fail/test.rs, 6, NONE
+coverage/reachable/bounds/reachable_fail/test.rs, 10, FULL
+coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/reachable/bounds/reachable_fail/test.rs b/tests/coverage/reachable/bounds/reachable_fail/test.rs
new file mode 100644
index 000000000000..cebd78b2d5d9
--- /dev/null
+++ b/tests/coverage/reachable/bounds/reachable_fail/test.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn get(s: &[i16], index: usize) -> i16 {
+    s[index] // PARTIAL: `s[index]` is covered, but `index = 15` induces a failure
+} // NONE: `index = 15` caused failure earlier
+
+#[kani::proof]
+fn main() {
+    get(&[7, -83, 19], 15);
+} // NONE: `index = 15` caused failure earlier
diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected
new file mode 100644
index 000000000000..1ec1abefffd8
--- /dev/null
+++ b/tests/coverage/reachable/div-zero/reachable_fail/expected
@@ -0,0 +1,4 @@
+coverage/reachable/div-zero/reachable_fail/test.rs, 5, PARTIAL
+coverage/reachable/div-zero/reachable_fail/test.rs, 6, NONE
+coverage/reachable/div-zero/reachable_fail/test.rs, 10, FULL
+coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/reachable/div-zero/reachable_fail/test.rs b/tests/coverage/reachable/div-zero/reachable_fail/test.rs
new file mode 100644
index 000000000000..5f69005ee712
--- /dev/null
+++ b/tests/coverage/reachable/div-zero/reachable_fail/test.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn div(x: u16, y: u16) -> u16 {
+    x / y // PARTIAL: `y = 0` causes failure, but `x / y` is `COVERED`
+}
+
+#[kani::proof]
+fn main() {
+    div(678, 0);
+}
diff --git a/tests/coverage/reachable/div-zero/reachable_pass/expected b/tests/coverage/reachable/div-zero/reachable_pass/expected
new file mode 100644
index 000000000000..c7bfb5961c0b
--- /dev/null
+++ b/tests/coverage/reachable/div-zero/reachable_pass/expected
@@ -0,0 +1,4 @@
+coverage/reachable/div-zero/reachable_pass/test.rs, 5, PARTIAL
+coverage/reachable/div-zero/reachable_pass/test.rs, 6, FULL
+coverage/reachable/div-zero/reachable_pass/test.rs, 10, FULL
+coverage/reachable/div-zero/reachable_pass/test.rs, 11, FULL
diff --git a/tests/coverage/reachable/div-zero/reachable_pass/test.rs b/tests/coverage/reachable/div-zero/reachable_pass/test.rs
new file mode 100644
index 000000000000..766fb5a89d88
--- /dev/null
+++ b/tests/coverage/reachable/div-zero/reachable_pass/test.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn div(x: u16, y: u16) -> u16 {
+    if y != 0 { x / y } else { 0 } // PARTIAL: some cases are `COVERED`, others are not
+}
+
+#[kani::proof]
+fn main() {
+    div(11, 3);
+}
diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected
new file mode 100644
index 000000000000..f20826fb1a8e
--- /dev/null
+++ b/tests/coverage/reachable/overflow/reachable_fail/expected
@@ -0,0 +1,5 @@
+coverage/reachable/overflow/reachable_fail/test.rs, 8, PARTIAL
+coverage/reachable/overflow/reachable_fail/test.rs, 9, FULL
+coverage/reachable/overflow/reachable_fail/test.rs, 13, FULL
+coverage/reachable/overflow/reachable_fail/test.rs, 14, FULL
+coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE
diff --git a/tests/coverage/reachable/overflow/reachable_fail/test.rs b/tests/coverage/reachable/overflow/reachable_fail/test.rs
new file mode 100644
index 000000000000..d435612f2342
--- /dev/null
+++ b/tests/coverage/reachable/overflow/reachable_fail/test.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that Kani reports the correct coverage results in the case of an
+//! arithmetic overflow failure (caused by the second call to `cond_reduce`).
+
+fn cond_reduce(thresh: u32, x: u32) -> u32 {
+    if x > thresh { x - 50 } else { x } // PARTIAL: some cases are `COVERED`, others are not
+}
+
+#[kani::proof]
+fn main() {
+    cond_reduce(60, 70);
+    cond_reduce(40, 42);
+} // NONE: Caused by the arithmetic overflow failure from the second call to `cond_reduce`
diff --git a/tests/coverage/reachable/overflow/reachable_pass/expected b/tests/coverage/reachable/overflow/reachable_pass/expected
new file mode 100644
index 000000000000..5becf2cd23e7
--- /dev/null
+++ b/tests/coverage/reachable/overflow/reachable_pass/expected
@@ -0,0 +1,7 @@
+coverage/reachable/overflow/reachable_pass/test.rs, 8, FULL
+coverage/reachable/overflow/reachable_pass/test.rs, 9, FULL
+coverage/reachable/overflow/reachable_pass/test.rs, 13, FULL
+coverage/reachable/overflow/reachable_pass/test.rs, 14, FULL
+coverage/reachable/overflow/reachable_pass/test.rs, 15, FULL
+coverage/reachable/overflow/reachable_pass/test.rs, 16, FULL
+coverage/reachable/overflow/reachable_pass/test.rs, 17, FULL
diff --git a/tests/coverage/reachable/overflow/reachable_pass/test.rs b/tests/coverage/reachable/overflow/reachable_pass/test.rs
new file mode 100644
index 000000000000..0b05874efc84
--- /dev/null
+++ b/tests/coverage/reachable/overflow/reachable_pass/test.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that Kani reports the correct coverage results (`FULL` for all lines)
+//! in a case where arithmetic overflow failures are prevented.
+
+fn reduce(x: u32) -> u32 {
+    if x > 1000 { x - 1000 } else { x }
+}
+
+#[kani::proof]
+fn main() {
+    reduce(7);
+    reduce(33);
+    reduce(728);
+    reduce(1079);
+}
diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/expected b/tests/coverage/reachable/rem-zero/reachable_fail/expected
new file mode 100644
index 000000000000..f7fa6ed7efeb
--- /dev/null
+++ b/tests/coverage/reachable/rem-zero/reachable_fail/expected
@@ -0,0 +1,4 @@
+coverage/reachable/rem-zero/reachable_fail/test.rs, 5, PARTIAL
+coverage/reachable/rem-zero/reachable_fail/test.rs, 6, NONE
+coverage/reachable/rem-zero/reachable_fail/test.rs, 10, FULL
+coverage/reachable/rem-zero/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/test.rs b/tests/coverage/reachable/rem-zero/reachable_fail/test.rs
new file mode 100644
index 000000000000..400c7e02340b
--- /dev/null
+++ b/tests/coverage/reachable/rem-zero/reachable_fail/test.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn rem(x: u16, y: u16) -> u16 {
+    x % y // PARTIAL: `x % y` is covered but induces a division failure
+} // NONE: Caused by division failure earlier
+
+#[kani::proof]
+fn main() {
+    rem(678, 0);
+} // NONE: Caused by division failure earlier
diff --git a/tests/coverage/reachable/rem-zero/reachable_pass/expected b/tests/coverage/reachable/rem-zero/reachable_pass/expected
new file mode 100644
index 000000000000..f3d5934d785d
--- /dev/null
+++ b/tests/coverage/reachable/rem-zero/reachable_pass/expected
@@ -0,0 +1,4 @@
+coverage/reachable/rem-zero/reachable_pass/test.rs, 5, PARTIAL
+coverage/reachable/rem-zero/reachable_pass/test.rs, 6, FULL
+coverage/reachable/rem-zero/reachable_pass/test.rs, 10, FULL
+coverage/reachable/rem-zero/reachable_pass/test.rs, 11, FULL
diff --git a/tests/coverage/reachable/rem-zero/reachable_pass/test.rs b/tests/coverage/reachable/rem-zero/reachable_pass/test.rs
new file mode 100644
index 000000000000..41ed28f7b903
--- /dev/null
+++ b/tests/coverage/reachable/rem-zero/reachable_pass/test.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn rem(x: u16, y: u16) -> u16 {
+    if y != 0 { x % y } else { 0 }
+}
+
+#[kani::proof]
+fn main() {
+    rem(11, 3);
+}
diff --git a/tests/coverage/unreachable/abort/expected b/tests/coverage/unreachable/abort/expected
new file mode 100644
index 000000000000..473b0f5a8d4d
--- /dev/null
+++ b/tests/coverage/unreachable/abort/expected
@@ -0,0 +1,7 @@
+coverage/unreachable/abort/main.rs, 10, PARTIAL
+coverage/unreachable/abort/main.rs, 11, FULL
+coverage/unreachable/abort/main.rs, 13, FULL
+coverage/unreachable/abort/main.rs, 15, FULL
+coverage/unreachable/abort/main.rs, 17, NONE
+coverage/unreachable/abort/main.rs, 20, NONE
+coverage/unreachable/abort/main.rs, 21, NONE
diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs
new file mode 100644
index 000000000000..2941ec126f3c
--- /dev/null
+++ b/tests/coverage/unreachable/abort/main.rs
@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test that the abort() function is respected and nothing beyond it will execute.
+
+use std::process;
+
+#[kani::proof]
+fn main() {
+    for i in 0..4 {
+        if i == 1 {
+            // This comes first and it should be reachable.
+            process::abort();
+        }
+        if i == 2 {
+            // This should never happen.
+            process::exit(1);
+        }
+    }
+    assert!(false, "This is unreachable");
+}
diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected
new file mode 100644
index 000000000000..f5b5f8044769
--- /dev/null
+++ b/tests/coverage/unreachable/assert/expected
@@ -0,0 +1,7 @@
+coverage/unreachable/assert/test.rs, 6, FULL
+coverage/unreachable/assert/test.rs, 7, FULL
+coverage/unreachable/assert/test.rs, 9, FULL
+coverage/unreachable/assert/test.rs, 10, NONE
+coverage/unreachable/assert/test.rs, 12, NONE
+coverage/unreachable/assert/test.rs, 16, FULL
+coverage/unreachable/assert/test.rs, 18, FULL
diff --git a/tests/coverage/unreachable/assert/test.rs b/tests/coverage/unreachable/assert/test.rs
new file mode 100644
index 000000000000..e7bddead756a
--- /dev/null
+++ b/tests/coverage/unreachable/assert/test.rs
@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn foo() {
+    let x: i32 = kani::any();
+    if x > 5 {
+        // fails
+        assert!(x < 4);
+        if x < 3 {
+            // unreachable
+            assert!(x == 2);
+        }
+    } else {
+        // passes
+        assert!(x <= 5);
+    }
+}
diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected
new file mode 100644
index 000000000000..f4e7608b2c13
--- /dev/null
+++ b/tests/coverage/unreachable/assert_eq/expected
@@ -0,0 +1,5 @@
+coverage/unreachable/assert_eq/test.rs, 6, FULL
+coverage/unreachable/assert_eq/test.rs, 7, FULL
+coverage/unreachable/assert_eq/test.rs, 8, FULL
+coverage/unreachable/assert_eq/test.rs, 9, NONE
+coverage/unreachable/assert_eq/test.rs, 11, FULL
diff --git a/tests/coverage/unreachable/assert_eq/test.rs b/tests/coverage/unreachable/assert_eq/test.rs
new file mode 100644
index 000000000000..29623498e715
--- /dev/null
+++ b/tests/coverage/unreachable/assert_eq/test.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn main() {
+    let x: i32 = kani::any();
+    let y = if x > 10 { 15 } else { 33 };
+    if y > 50 {
+        assert_eq!(y, 55);
+    }
+}
diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected
new file mode 100644
index 000000000000..3b57defb4c36
--- /dev/null
+++ b/tests/coverage/unreachable/assert_ne/expected
@@ -0,0 +1,6 @@
+coverage/unreachable/assert_ne/test.rs, 6, FULL
+coverage/unreachable/assert_ne/test.rs, 7, FULL
+coverage/unreachable/assert_ne/test.rs, 8, FULL
+coverage/unreachable/assert_ne/test.rs, 10, FULL
+coverage/unreachable/assert_ne/test.rs, 11, NONE
+coverage/unreachable/assert_ne/test.rs, 14, FULL
diff --git a/tests/coverage/unreachable/assert_ne/test.rs b/tests/coverage/unreachable/assert_ne/test.rs
new file mode 100644
index 000000000000..44b0ca82383e
--- /dev/null
+++ b/tests/coverage/unreachable/assert_ne/test.rs
@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn main() {
+    let x: u32 = kani::any();
+    if x > 0 {
+        let y = x / 2;
+        // y is strictly less than x
+        if y == x {
+            assert_ne!(y, 1);
+        }
+    }
+}
diff --git a/tests/coverage/unreachable/assume_assert/expected b/tests/coverage/unreachable/assume_assert/expected
new file mode 100644
index 000000000000..8c1ae8a247d2
--- /dev/null
+++ b/tests/coverage/unreachable/assume_assert/expected
@@ -0,0 +1,4 @@
+coverage/unreachable/assume_assert/main.rs, 5, FULL
+coverage/unreachable/assume_assert/main.rs, 6, FULL
+coverage/unreachable/assume_assert/main.rs, 7, NONE
+coverage/unreachable/assume_assert/main.rs, 8, NONE
diff --git a/tests/coverage/unreachable/assume_assert/main.rs b/tests/coverage/unreachable/assume_assert/main.rs
new file mode 100644
index 000000000000..c4d5d65c6640
--- /dev/null
+++ b/tests/coverage/unreachable/assume_assert/main.rs
@@ -0,0 +1,8 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn check_assume_assert() {
+    let a: u8 = kani::any();
+    kani::assume(false);
+    assert!(a < 5);
+}
diff --git a/tests/coverage/unreachable/bounds/expected b/tests/coverage/unreachable/bounds/expected
new file mode 100644
index 000000000000..610372000a01
--- /dev/null
+++ b/tests/coverage/unreachable/bounds/expected
@@ -0,0 +1,4 @@
+coverage/unreachable/bounds/test.rs, 5, PARTIAL
+coverage/unreachable/bounds/test.rs, 6, FULL
+coverage/unreachable/bounds/test.rs, 11, FULL
+coverage/unreachable/bounds/test.rs, 12, FULL
diff --git a/tests/coverage/unreachable/bounds/test.rs b/tests/coverage/unreachable/bounds/test.rs
new file mode 100644
index 000000000000..c37c9d0dcad6
--- /dev/null
+++ b/tests/coverage/unreachable/bounds/test.rs
@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn get(s: &[i16], index: usize) -> i16 {
+    if index < s.len() { s[index] } else { -1 }
+}
+
+#[kani::proof]
+fn main() {
+    //get(&[7, -83, 19], 2);
+    get(&[5, 206, -46, 321, 8], 8);
+}
diff --git a/tests/coverage/unreachable/break/expected b/tests/coverage/unreachable/break/expected
new file mode 100644
index 000000000000..dcb013c50c3d
--- /dev/null
+++ b/tests/coverage/unreachable/break/expected
@@ -0,0 +1,9 @@
+coverage/unreachable/break/main.rs, 5, PARTIAL
+coverage/unreachable/break/main.rs, 6, FULL
+coverage/unreachable/break/main.rs, 7, FULL
+coverage/unreachable/break/main.rs, 11, NONE
+coverage/unreachable/break/main.rs, 12, PARTIAL
+coverage/unreachable/break/main.rs, 16, FULL
+coverage/unreachable/break/main.rs, 17, FULL
+coverage/unreachable/break/main.rs, 18, FULL
+coverage/unreachable/break/main.rs, 19, FULL
diff --git a/tests/coverage/unreachable/break/main.rs b/tests/coverage/unreachable/break/main.rs
new file mode 100644
index 000000000000..4e795bd2a6ea
--- /dev/null
+++ b/tests/coverage/unreachable/break/main.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn find_positive(nums: &[i32]) -> Option<i32> {
+    for &num in nums {
+        if num > 0 {
+            return Some(num);
+        }
+    }
+    // This part is unreachable if there is at least one positive number.
+    None
+}
+
+#[kani::proof]
+fn main() {
+    let numbers = [-3, -1, 0, 2, 4];
+    let result = find_positive(&numbers);
+    assert_eq!(result, Some(2));
+}
diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected
new file mode 100644
index 000000000000..214cbfa827bd
--- /dev/null
+++ b/tests/coverage/unreachable/check_id/expected
@@ -0,0 +1,16 @@
+coverage/unreachable/check_id/main.rs, 5, FULL
+coverage/unreachable/check_id/main.rs, 6, FULL
+coverage/unreachable/check_id/main.rs, 8, NONE
+coverage/unreachable/check_id/main.rs, 10, FULL
+coverage/unreachable/check_id/main.rs, 14, FULL
+coverage/unreachable/check_id/main.rs, 15, FULL
+coverage/unreachable/check_id/main.rs, 16, FULL
+coverage/unreachable/check_id/main.rs, 17, FULL
+coverage/unreachable/check_id/main.rs, 18, FULL
+coverage/unreachable/check_id/main.rs, 19, FULL
+coverage/unreachable/check_id/main.rs, 20, FULL
+coverage/unreachable/check_id/main.rs, 21, FULL
+coverage/unreachable/check_id/main.rs, 22, FULL
+coverage/unreachable/check_id/main.rs, 23, FULL
+coverage/unreachable/check_id/main.rs, 24, FULL
+coverage/unreachable/check_id/main.rs, 25, NONE
diff --git a/tests/coverage/unreachable/check_id/main.rs b/tests/coverage/unreachable/check_id/main.rs
new file mode 100644
index 000000000000..8273a9bcc679
--- /dev/null
+++ b/tests/coverage/unreachable/check_id/main.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn foo(x: i32) {
+    assert!(1 + 1 == 2);
+    if x < 9 {
+        // unreachable
+        assert!(2 + 2 == 4);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    assert!(1 + 1 == 2);
+    let x = if kani::any() { 33 } else { 57 };
+    foo(x);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 2);
+    assert!(3 + 3 == 5);
+}
diff --git a/tests/coverage/unreachable/compare/expected b/tests/coverage/unreachable/compare/expected
new file mode 100644
index 000000000000..6187e232cbe7
--- /dev/null
+++ b/tests/coverage/unreachable/compare/expected
@@ -0,0 +1,7 @@
+coverage/unreachable/compare/main.rs, 6, PARTIAL
+coverage/unreachable/compare/main.rs, 7, FULL
+coverage/unreachable/compare/main.rs, 11, FULL
+coverage/unreachable/compare/main.rs, 12, FULL
+coverage/unreachable/compare/main.rs, 13, FULL
+coverage/unreachable/compare/main.rs, 14, FULL
+coverage/unreachable/compare/main.rs, 16, FULL
diff --git a/tests/coverage/unreachable/compare/main.rs b/tests/coverage/unreachable/compare/main.rs
new file mode 100644
index 000000000000..a10fb84e29a8
--- /dev/null
+++ b/tests/coverage/unreachable/compare/main.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn compare(x: u16, y: u16) -> u16 {
+    // The line below should be reported as PARTIAL for having both REACHABLE and UNREACHABLE checks
+    if x >= y { 1 } else { 0 }
+}
+
+#[kani::proof]
+fn main() {
+    let x: u16 = kani::any();
+    let y: u16 = kani::any();
+    if x >= y {
+        compare(x, y);
+    }
+}
diff --git a/tests/coverage/unreachable/contradiction/expected b/tests/coverage/unreachable/contradiction/expected
new file mode 100644
index 000000000000..ca67a4938193
--- /dev/null
+++ b/tests/coverage/unreachable/contradiction/expected
@@ -0,0 +1,6 @@
+coverage/unreachable/contradiction/main.rs, 5, FULL
+coverage/unreachable/contradiction/main.rs, 6, FULL
+coverage/unreachable/contradiction/main.rs, 7, PARTIAL
+coverage/unreachable/contradiction/main.rs, 8, NONE
+coverage/unreachable/contradiction/main.rs, 11, FULL
+coverage/unreachable/contradiction/main.rs, 13, FULL
diff --git a/tests/coverage/unreachable/contradiction/main.rs b/tests/coverage/unreachable/contradiction/main.rs
new file mode 100644
index 000000000000..fe79107e8962
--- /dev/null
+++ b/tests/coverage/unreachable/contradiction/main.rs
@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn contradiction() {
+    let x: u8 = kani::any();
+    if x > 5 {
+        if x < 2 {
+            let y = x;
+        }
+    } else {
+        assert!(x < 10);
+    }
+}
diff --git a/tests/coverage/unreachable/debug-assert/expected b/tests/coverage/unreachable/debug-assert/expected
new file mode 100644
index 000000000000..25fdfed4c863
--- /dev/null
+++ b/tests/coverage/unreachable/debug-assert/expected
@@ -0,0 +1,4 @@
+coverage/unreachable/debug-assert/main.rs, 6, PARTIAL
+coverage/unreachable/debug-assert/main.rs, 7, PARTIAL
+coverage/unreachable/debug-assert/main.rs, 8, NONE
+coverage/unreachable/debug-assert/main.rs, 10, NONE
diff --git a/tests/coverage/unreachable/debug-assert/main.rs b/tests/coverage/unreachable/debug-assert/main.rs
new file mode 100644
index 000000000000..ab3ab41e47d0
--- /dev/null
+++ b/tests/coverage/unreachable/debug-assert/main.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn main() {
+    for i in 0..4 {
+        debug_assert!(i > 0, "This should fail and stop the execution");
+        assert!(i == 0, "This should be unreachable");
+    }
+}
diff --git a/tests/coverage/unreachable/divide/expected b/tests/coverage/unreachable/divide/expected
new file mode 100644
index 000000000000..63081358941a
--- /dev/null
+++ b/tests/coverage/unreachable/divide/expected
@@ -0,0 +1,7 @@
+coverage/unreachable/divide/main.rs, 6, FULL
+coverage/unreachable/divide/main.rs, 7, FULL
+coverage/unreachable/divide/main.rs, 9, NONE
+coverage/unreachable/divide/main.rs, 11, FULL
+coverage/unreachable/divide/main.rs, 15, FULL
+coverage/unreachable/divide/main.rs, 16, FULL
+coverage/unreachable/divide/main.rs, 17, FULL
diff --git a/tests/coverage/unreachable/divide/main.rs b/tests/coverage/unreachable/divide/main.rs
new file mode 100644
index 000000000000..ba6afab83135
--- /dev/null
+++ b/tests/coverage/unreachable/divide/main.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that checks for UNREACHABLE panics. The panic is reported as NONE for the assumption that the divisor is not zero.
+fn divide(a: i32, b: i32) -> i32 {
+    if b != 0 {
+        return a / b;
+    } else {
+        panic!("Division by zero");
+    }
+}
+
+#[kani::proof]
+fn main() {
+    let y: i32 = kani::any();
+    kani::assume(y != 0);
+    let result = divide(10, y);
+    assert_eq!(result, 5);
+}
diff --git a/tests/coverage/unreachable/early-return/expected b/tests/coverage/unreachable/early-return/expected
new file mode 100644
index 000000000000..466c1775408b
--- /dev/null
+++ b/tests/coverage/unreachable/early-return/expected
@@ -0,0 +1,10 @@
+coverage/unreachable/early-return/main.rs, 5, PARTIAL
+coverage/unreachable/early-return/main.rs, 6, FULL
+coverage/unreachable/early-return/main.rs, 7, FULL
+coverage/unreachable/early-return/main.rs, 10, NONE
+coverage/unreachable/early-return/main.rs, 11, PARTIAL
+coverage/unreachable/early-return/main.rs, 15, FULL
+coverage/unreachable/early-return/main.rs, 16, FULL
+coverage/unreachable/early-return/main.rs, 17, FULL
+coverage/unreachable/early-return/main.rs, 18, FULL
+coverage/unreachable/early-return/main.rs, 19, FULL
diff --git a/tests/coverage/unreachable/early-return/main.rs b/tests/coverage/unreachable/early-return/main.rs
new file mode 100644
index 000000000000..4e50c1f8a3b7
--- /dev/null
+++ b/tests/coverage/unreachable/early-return/main.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn find_index(nums: &[i32], target: i32) -> Option<usize> {
+    for (index, &num) in nums.iter().enumerate() {
+        if num == target {
+            return Some(index);
+        }
+    }
+    None
+}
+
+#[kani::proof]
+fn main() {
+    let numbers = [10, 20, 30, 40, 50];
+    let target = 30;
+    let result = find_index(&numbers, target);
+    assert_eq!(result, Some(2));
+}
diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected
new file mode 100644
index 000000000000..4460f23a80de
--- /dev/null
+++ b/tests/coverage/unreachable/if-statement/expected
@@ -0,0 +1,10 @@
+coverage/unreachable/if-statement/main.rs, 5, FULL
+coverage/unreachable/if-statement/main.rs, 7, PARTIAL
+coverage/unreachable/if-statement/main.rs, 8, NONE
+coverage/unreachable/if-statement/main.rs, 9, NONE
+coverage/unreachable/if-statement/main.rs, 11, NONE
+coverage/unreachable/if-statement/main.rs, 13, FULL
+coverage/unreachable/if-statement/main.rs, 17, FULL
+coverage/unreachable/if-statement/main.rs, 18, FULL
+coverage/unreachable/if-statement/main.rs, 19, FULL
+coverage/unreachable/if-statement/main.rs, 20, FULL
diff --git a/tests/coverage/unreachable/if-statement/main.rs b/tests/coverage/unreachable/if-statement/main.rs
new file mode 100644
index 000000000000..f497cd76808e
--- /dev/null
+++ b/tests/coverage/unreachable/if-statement/main.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn check_number(num: i32) -> &'static str {
+    if num > 0 {
+        // The line is partially covered because the if statement is UNREACHABLE while the else statement is reachable
+        if num % 2 == 0 { "Positive and Even" } else { "Positive and Odd" }
+    } else if num < 0 {
+        "Negative"
+    } else {
+        "Zero"
+    }
+}
+
+#[kani::proof]
+fn main() {
+    let number = 7;
+    let result = check_number(number);
+    assert_eq!(result, "Positive and Odd");
+}
diff --git a/tests/coverage/unreachable/multiple-harnesses/expected b/tests/coverage/unreachable/multiple-harnesses/expected
new file mode 100644
index 000000000000..17a52666c08d
--- /dev/null
+++ b/tests/coverage/unreachable/multiple-harnesses/expected
@@ -0,0 +1,39 @@
+Checking harness fully_covered...
+coverage/unreachable/multiple-harnesses/main.rs, 5, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 7, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 8, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 9, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 11, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 13, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 14, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 15, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 17, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 20, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 21, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 23, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 26, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 40, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 41, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 42, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 43, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 44, FULL
+
+Checking harness mostly_covered...
+coverage/unreachable/multiple-harnesses/main.rs, 5, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 7, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 8, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 9, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 11, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 13, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 14, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 15, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 17, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 20, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 21, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 23, NONE
+coverage/unreachable/multiple-harnesses/main.rs, 26, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 31, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 32, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 33, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 34, FULL
+coverage/unreachable/multiple-harnesses/main.rs, 35, FULL
diff --git a/tests/coverage/unreachable/multiple-harnesses/main.rs b/tests/coverage/unreachable/multiple-harnesses/main.rs
new file mode 100644
index 000000000000..9cf7dc4101e6
--- /dev/null
+++ b/tests/coverage/unreachable/multiple-harnesses/main.rs
@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn estimate_size(x: u32) -> u32 {
+    assert!(x < 4096);
+
+    if x < 256 {
+        if x < 128 {
+            return 1;
+        } else {
+            return 3;
+        }
+    } else if x < 1024 {
+        if x > 1022 {
+            return 4;
+        } else {
+            return 5;
+        }
+    } else {
+        if x < 2048 {
+            return 7;
+        } else {
+            return 9;
+        }
+    }
+}
+
+#[cfg(kani)]
+#[kani::proof]
+fn mostly_covered() {
+    let x: u32 = kani::any();
+    kani::assume(x < 2048);
+    let y = estimate_size(x);
+    assert!(y < 10);
+}
+
+#[cfg(kani)]
+#[kani::proof]
+fn fully_covered() {
+    let x: u32 = kani::any();
+    kani::assume(x < 4096);
+    let y = estimate_size(x);
+    assert!(y < 10);
+}
diff --git a/tests/coverage/unreachable/return/expected b/tests/coverage/unreachable/return/expected
new file mode 100644
index 000000000000..139f81840aab
--- /dev/null
+++ b/tests/coverage/unreachable/return/expected
@@ -0,0 +1,8 @@
+coverage/unreachable/return/main.rs, 5, FULL
+coverage/unreachable/return/main.rs, 6, FULL
+coverage/unreachable/return/main.rs, 9, NONE
+coverage/unreachable/return/main.rs, 10, PARTIAL
+coverage/unreachable/return/main.rs, 14, FULL
+coverage/unreachable/return/main.rs, 15, FULL
+coverage/unreachable/return/main.rs, 16, FULL
+coverage/unreachable/return/main.rs, 17, FULL
diff --git a/tests/coverage/unreachable/return/main.rs b/tests/coverage/unreachable/return/main.rs
new file mode 100644
index 000000000000..ccd76a5b4f8e
--- /dev/null
+++ b/tests/coverage/unreachable/return/main.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn greet(is_guest: bool) -> &'static str {
+    if is_guest {
+        return "Welcome, Guest!";
+    }
+    // This part is unreachable if is_guest is true.
+    "Hello, User!"
+}
+
+#[kani::proof]
+fn main() {
+    let is_guest = true;
+    let message = greet(is_guest);
+    assert_eq!(message, "Welcome, Guest!");
+}
diff --git a/tests/coverage/unreachable/tutorial_unreachable/expected b/tests/coverage/unreachable/tutorial_unreachable/expected
new file mode 100644
index 000000000000..cf45a502d295
--- /dev/null
+++ b/tests/coverage/unreachable/tutorial_unreachable/expected
@@ -0,0 +1,5 @@
+coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL
+coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL
+coverage/unreachable/tutorial_unreachable/main.rs, 8, FULL
+coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE
+coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL
diff --git a/tests/coverage/unreachable/tutorial_unreachable/main.rs b/tests/coverage/unreachable/tutorial_unreachable/main.rs
new file mode 100644
index 000000000000..c56e591446cf
--- /dev/null
+++ b/tests/coverage/unreachable/tutorial_unreachable/main.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn unreachable_example() {
+    let x = 5;
+    let y = x + 2;
+    if x > y {
+        assert!(x < 8);
+    }
+}
diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected
new file mode 100644
index 000000000000..8fa3ec8b870f
--- /dev/null
+++ b/tests/coverage/unreachable/variant/expected
@@ -0,0 +1,10 @@
+coverage/unreachable/variant/main.rs, 15, FULL
+coverage/unreachable/variant/main.rs, 16, NONE
+coverage/unreachable/variant/main.rs, 17, NONE
+coverage/unreachable/variant/main.rs, 18, FULL
+coverage/unreachable/variant/main.rs, 19, NONE
+coverage/unreachable/variant/main.rs, 21, NONE
+coverage/unreachable/variant/main.rs, 23, FULL
+coverage/unreachable/variant/main.rs, 27, FULL
+coverage/unreachable/variant/main.rs, 28, FULL
+coverage/unreachable/variant/main.rs, 29, FULL
diff --git a/tests/coverage/unreachable/variant/main.rs b/tests/coverage/unreachable/variant/main.rs
new file mode 100644
index 000000000000..ca53b8ccfd18
--- /dev/null
+++ b/tests/coverage/unreachable/variant/main.rs
@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks coverage results in an example with a `match` statement matching on
+//! all enum variants.
+
+enum Direction {
+    Up,
+    Down,
+    Left,
+    Right,
+}
+
+fn print_direction(dir: Direction) {
+    match dir {
+        Direction::Up => println!("Going up!"),
+        Direction::Down => println!("Going down!"),
+        Direction::Left => println!("Going left!"),
+        Direction::Right => println!("Going right!"),
+        // This part is unreachable since we cover all variants in the match.
+        _ => {}
+    }
+}
+
+#[kani::proof]
+fn main() {
+    let direction = Direction::Left;
+    print_direction(direction);
+}
diff --git a/tests/coverage/unreachable/vectors/expected b/tests/coverage/unreachable/vectors/expected
new file mode 100644
index 000000000000..e47941f17db2
--- /dev/null
+++ b/tests/coverage/unreachable/vectors/expected
@@ -0,0 +1,6 @@
+coverage/unreachable/vectors/main.rs, 8, FULL
+coverage/unreachable/vectors/main.rs, 11, FULL
+coverage/unreachable/vectors/main.rs, 13, PARTIAL
+coverage/unreachable/vectors/main.rs, 15, NONE
+coverage/unreachable/vectors/main.rs, 17, FULL
+coverage/unreachable/vectors/main.rs, 19, FULL
diff --git a/tests/coverage/unreachable/vectors/main.rs b/tests/coverage/unreachable/vectors/main.rs
new file mode 100644
index 000000000000..a44c4bb47c3d
--- /dev/null
+++ b/tests/coverage/unreachable/vectors/main.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks coverage results in an example with a guarded out-of-bounds access.
+
+#[kani::proof]
+fn main() {
+    let numbers = vec![1, 2, 3, 4, 5];
+
+    // Attempt to access the 10th element of the vector, which is out of bounds.
+    let tenth_element = numbers.get(9);
+
+    if let Some(value) = tenth_element {
+        // This part is unreachable since the vector has only 5 elements (indices 0 to 4).
+        println!("The 10th element is: {}", value);
+    } else {
+        println!("The 10th element is out of bounds!");
+    }
+}
diff --git a/tests/coverage/unreachable/while-loop-break/expected b/tests/coverage/unreachable/while-loop-break/expected
new file mode 100644
index 000000000000..a0e43c183846
--- /dev/null
+++ b/tests/coverage/unreachable/while-loop-break/expected
@@ -0,0 +1,11 @@
+coverage/unreachable/while-loop-break/main.rs, 8, FULL
+coverage/unreachable/while-loop-break/main.rs, 9, FULL
+coverage/unreachable/while-loop-break/main.rs, 10, FULL
+coverage/unreachable/while-loop-break/main.rs, 11, FULL
+coverage/unreachable/while-loop-break/main.rs, 13, FULL
+coverage/unreachable/while-loop-break/main.rs, 15, NONE
+coverage/unreachable/while-loop-break/main.rs, 16, PARTIAL
+coverage/unreachable/while-loop-break/main.rs, 20, FULL
+coverage/unreachable/while-loop-break/main.rs, 21, FULL
+coverage/unreachable/while-loop-break/main.rs, 22, FULL
+coverage/unreachable/while-loop-break/main.rs, 23, FULL
diff --git a/tests/coverage/unreachable/while-loop-break/main.rs b/tests/coverage/unreachable/while-loop-break/main.rs
new file mode 100644
index 000000000000..cb7c6276b147
--- /dev/null
+++ b/tests/coverage/unreachable/while-loop-break/main.rs
@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks coverage results in an example with a `while` loop that returns before
+//! running the last iteration.
+
+fn find_first_negative(nums: &[i32]) -> Option<i32> {
+    let mut index = 0;
+    while index < nums.len() {
+        if nums[index] < 0 {
+            return Some(nums[index]);
+        }
+        index += 1;
+    }
+    None
+}
+
+#[kani::proof]
+fn main() {
+    let numbers = [1, 2, -3, 4, -5];
+    let result = find_first_negative(&numbers);
+    assert_eq!(result, Some(-3));
+}
diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs
index f71bc535a11e..99ec78bef693 100644
--- a/tools/compiletest/src/common.rs
+++ b/tools/compiletest/src/common.rs
@@ -19,6 +19,7 @@ pub enum Mode {
     KaniFixme,
     CargoKani,
     CargoKaniTest, // `cargo kani --tests`. This is temporary and should be removed when s2n-quic moves --tests to `Cargo.toml`.
+    CoverageBased,
     Exec,
     Expected,
     Stub,
@@ -32,6 +33,7 @@ impl FromStr for Mode {
             "kani-fixme" => Ok(KaniFixme),
             "cargo-kani" => Ok(CargoKani),
             "cargo-kani-test" => Ok(CargoKaniTest),
+            "coverage-based" => Ok(CoverageBased),
             "exec" => Ok(Exec),
             "expected" => Ok(Expected),
             "stub-tests" => Ok(Stub),
@@ -47,6 +49,7 @@ impl fmt::Display for Mode {
             KaniFixme => "kani-fixme",
             CargoKani => "cargo-kani",
             CargoKaniTest => "cargo-kani-test",
+            CoverageBased => "coverage-based",
             Exec => "exec",
             Expected => "expected",
             Stub => "stub-tests",
diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs
index 0dd403ba1b2f..cdef1446763a 100644
--- a/tools/compiletest/src/main.rs
+++ b/tools/compiletest/src/main.rs
@@ -94,7 +94,7 @@ pub fn parse_config(args: Vec<String>) -> Config {
         .optflag("", "report-time",
                  "report the time of each test. Configuration is done via env variables, like \
                  rust unit tests.")
-        .optmulti("", "kani-flag", 
+        .optmulti("", "kani-flag",
                   "pass extra flags to Kani. Note that this may cause spurious failures if the \
                   passed flag conflicts with the test configuration. Only works for `kani`, \
                   `cargo-kani`, and `expected` modes."
diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
index 04647f7b6572..7fad336dffdc 100644
--- a/tools/compiletest/src/runtest.rs
+++ b/tools/compiletest/src/runtest.rs
@@ -7,7 +7,9 @@
 
 use crate::common::KaniFailStep;
 use crate::common::{output_base_dir, output_base_name};
-use crate::common::{CargoKani, CargoKaniTest, Exec, Expected, Kani, KaniFixme, Stub};
+use crate::common::{
+    CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub,
+};
 use crate::common::{Config, TestPaths};
 use crate::header::TestProps;
 use crate::read2::read2;
@@ -75,6 +77,7 @@ impl<'test> TestCx<'test> {
             KaniFixme => self.run_kani_test(),
             CargoKani => self.run_cargo_kani_test(false),
             CargoKaniTest => self.run_cargo_kani_test(true),
+            CoverageBased => self.run_expected_coverage_test(),
             Exec => self.run_exec_test(),
             Expected => self.run_expected_test(),
             Stub => self.run_stub_test(),
@@ -311,6 +314,22 @@ impl<'test> TestCx<'test> {
         self.compose_and_run(kani)
     }
 
+    /// Run coverage based output for kani on a single file
+    fn run_kani_with_coverage(&self) -> ProcRes {
+        let mut kani = Command::new("kani");
+        if !self.props.compile_flags.is_empty() {
+            kani.env("RUSTFLAGS", self.props.compile_flags.join(" "));
+        }
+        kani.arg(&self.testpaths.file).args(&self.props.kani_flags);
+        kani.arg("--coverage").args(&["-Z", "line-coverage"]);
+
+        if !self.props.cbmc_flags.is_empty() {
+            kani.arg("--cbmc-args").args(&self.props.cbmc_flags);
+        }
+
+        self.compose_and_run(kani)
+    }
+
     /// Runs an executable file and:
     ///  * Checks the expected output if an expected file is specified
     ///  * Checks the exit code (assumed to be 0 by default)
@@ -380,6 +399,13 @@ impl<'test> TestCx<'test> {
         self.verify_output(&proc_res, &expected_path);
     }
 
+    /// Runs Kani in coverage mode on the test file specified by `self.testpaths.file`.
+    fn run_expected_coverage_test(&self) {
+        let proc_res = self.run_kani_with_coverage();
+        let expected_path = self.testpaths.file.parent().unwrap().join("expected");
+        self.verify_output(&proc_res, &expected_path);
+    }
+
     /// Runs Kani with stub implementations of various data structures.
     /// Currently, it only runs tests for the Vec module with the (Kani)Vec
     /// abstraction. At a later stage, it should be possible to add command-line