diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index b969fecd3a61..8e0e23e0334c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -44,15 +44,13 @@ pub enum PropertyClass {
     ///
     /// SPECIAL BEHAVIOR: None? Possibly confusing to customers that a Rust assume is a Kani assert.
     Assume,
-    /// Same as `Assume`, but fails if the assumption would empty the search space.
-    /// E.g, imagine a previous assertion (x > 0) already exists. An assume(x < 0) would empty the search space
-    /// because there is no value of `x` for which both assertions are satisfiable.
-    /// We use this internally for contract instrumentation to ensure that preconditions do not empty the search space.
-    AssumeUnlessVacuous,
     /// See [GotocCtx::codegen_cover] below. Generally just an `assert(false)` that's not an error.
     ///
     /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
     Cover,
+    /// Same codegen as `Cover`, but failure will cause verification failure.
+    /// Used internally for contract instrumentation; see the contracts module in kani_macros for details.
+    ContractCover,
     /// The class of checks used for code coverage instrumentation. Only needed
     /// when working on coverage-related features.
     ///
@@ -155,6 +153,12 @@ impl GotocCtx<'_> {
         self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc)
     }
 
+    /// Generate a cover statement for a contract at the current location
+    pub fn codegen_contract_cover(&self, cond: Expr, msg: &str, span: SpanStable) -> Stmt {
+        let loc = self.codegen_caller_span_stable(span);
+        self.codegen_assert(cond.not(), PropertyClass::ContractCover, msg, loc)
+    }
+
     /// Generate a cover statement for code coverage reports.
     pub fn codegen_coverage(
         &self,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 2c19dc913dc8..4dd450bfab95 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -82,10 +82,14 @@ impl GotocHook for Cover {
     }
 }
 
-struct Assume;
-impl GotocHook for Assume {
+/// A hook for Kani's `contract_cover` function.
+/// This is only used internally for contract instrumentation.
+/// We use it to check that a contract's preconditions are satisfiable and that its postconditions are reachable.
+/// Unlike the standard `cover`, failing this check does cause verification failure.
+struct ContractCover;
+impl GotocHook for ContractCover {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance.def, "KaniAssume")
+        matches_function(tcx, instance.def, "KaniContractCover")
     }
 
     fn handle(
@@ -97,19 +101,30 @@ impl GotocHook for Assume {
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        assert_eq!(fargs.len(), 1);
+        assert_eq!(fargs.len(), 2);
         let cond = fargs.remove(0).cast_to(Type::bool());
+        let msg = fargs.remove(0);
+        let msg = gcx.extract_const_message(&msg).unwrap();
         let target = target.unwrap();
-        let loc = gcx.codegen_span_stable(span);
+        let caller_loc = gcx.codegen_caller_span_stable(span);
 
-        Stmt::block(vec![gcx.codegen_assume(cond, loc), Stmt::goto(bb_label(target), loc)], loc)
+        let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span);
+
+        Stmt::block(
+            vec![
+                reach_stmt,
+                gcx.codegen_contract_cover(cond, &msg, span),
+                Stmt::goto(bb_label(target), caller_loc),
+            ],
+            caller_loc,
+        )
     }
 }
 
-struct AssumeUnlessVacuous;
-impl GotocHook for AssumeUnlessVacuous {
+struct Assume;
+impl GotocHook for Assume {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance.def, "KaniAssumeUnlessVacuous")
+        matches_function(tcx, instance.def, "KaniAssume")
     }
 
     fn handle(
@@ -121,21 +136,12 @@ impl GotocHook for AssumeUnlessVacuous {
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        assert_eq!(fargs.len(), 2);
+        assert_eq!(fargs.len(), 1);
         let cond = fargs.remove(0).cast_to(Type::bool());
-        let msg = fargs.remove(0);
-        let msg = gcx.extract_const_message(&msg).unwrap();
         let target = target.unwrap();
         let loc = gcx.codegen_span_stable(span);
 
-        Stmt::block(
-            vec![
-                gcx.codegen_assume(cond, loc),
-                Stmt::assert_false(PropertyClass::AssumeUnlessVacuous.as_str(), &msg, loc),
-                Stmt::goto(bb_label(target), loc),
-            ],
-            loc,
-        )
+        Stmt::block(vec![gcx.codegen_assume(cond, loc), Stmt::goto(bb_label(target), loc)], loc)
     }
 }
 
@@ -617,7 +623,7 @@ pub fn fn_hooks() -> GotocHooks {
         hooks: vec![
             Rc::new(Panic),
             Rc::new(Assume),
-            Rc::new(AssumeUnlessVacuous),
+            Rc::new(ContractCover),
             Rc::new(Assert),
             Rc::new(Check),
             Rc::new(Cover),
diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
index 33d26961f6d9..1e4a10a6a34e 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -95,7 +95,7 @@ pub struct PropertyId {
 }
 
 impl Property {
-    const ASSUME_UNLESS_VACUOUS_PROPERTY_CLASS: &'static str = "assume_unless_vacuous";
+    const CONTRACT_COVER_PROPERTY_CLASS: &'static str = "contract_cover";
     const COVER_PROPERTY_CLASS: &'static str = "cover";
     const COVERAGE_PROPERTY_CLASS: &'static str = "code_coverage";
 
@@ -103,9 +103,9 @@ impl Property {
         self.property_id.class.clone()
     }
 
-    /// Returns true if this is an assume_unless_vacuous property
-    pub fn is_assume_unless_vacuous_property(&self) -> bool {
-        self.property_id.class == Self::ASSUME_UNLESS_VACUOUS_PROPERTY_CLASS
+    /// Returns true if this is an contract_cover property
+    pub fn is_contract_cover_property(&self) -> bool {
+        self.property_id.class == Self::CONTRACT_COVER_PROPERTY_CLASS
     }
 
     // Returns true if this is a code_coverage check
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index 142fb56e52b6..bdc16f72c595 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -512,7 +512,7 @@ pub fn postprocess_result(properties: Vec<Property>, extra_ptr_checks: bool) ->
 
     let updated_properties =
         update_properties_with_reach_status(properties_filtered, has_fundamental_failures);
-    let results_after_code_coverage = update_results_of_code_covererage_checks(updated_properties);
+    let results_after_code_coverage = update_results_of_code_coverage_checks(updated_properties);
     update_results_of_cover_checks(results_after_code_coverage)
 }
 
@@ -623,7 +623,7 @@ fn update_properties_with_reach_status(
 /// 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> {
+fn update_results_of_code_coverage_checks(mut properties: Vec<Property>) -> Vec<Property> {
     for prop in properties.iter_mut() {
         if prop.is_code_coverage_property() {
             prop.status = match prop.status {
@@ -648,10 +648,8 @@ fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Ve
 /// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since
 /// `update_properties_with_reach_status` is called beforehand
 ///
-/// We encode assume_unless_vacuous(cond) as assume(cond); assert(false).
-/// `is_assume_unless_vacuous_property` corresponds to the assert(false).
-/// If this assertion fails as expected, the assume did not empty the search space,
-/// so succeed; otherwise, fail.
+/// Although regular cover properties do not fail verification, contract cover properties do.
+/// If the assert(!cond) fails as expected, succeed; otherwise, fail.
 fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property> {
     for prop in properties.iter_mut() {
         if prop.is_cover_property() {
@@ -660,8 +658,11 @@ fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property
             } else if prop.status == CheckStatus::Failure {
                 prop.status = CheckStatus::Satisfied;
             }
-        } else if prop.is_assume_unless_vacuous_property() {
-            if prop.status == CheckStatus::Success {
+        } else if prop.is_contract_cover_property() {
+            if prop.status == CheckStatus::Unreachable
+                || prop.status == CheckStatus::Success
+                || prop.status == CheckStatus::Undetermined
+            {
                 prop.status = CheckStatus::Failure;
             } else if prop.status == CheckStatus::Failure {
                 prop.status = CheckStatus::Success;
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index c5a6ae4aca29..e45a24d4f016 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -347,24 +347,12 @@ macro_rules! kani_intrinsics {
             }
 
             /// This function is only used for function contract instrumentation.
-            /// It is the same as assume(), but it adds an extra assert(false) afterward.
-            /// The CBMC output parser uses this assertion as a reachability check;
-            /// if the assertion is unreachable or succeeds, then we know that the assumption emptied the search space.
+            /// It is the same as cover(), but if the cover statement is unreachable, it fails the contract harness.
+            /// See the contracts module in kani_macros for details.
             #[inline(never)]
-            #[rustc_diagnostic_item = "KaniAssumeUnlessVacuous"]
-            #[cfg(not(feature = "concrete_playback"))]
+            #[rustc_diagnostic_item = "KaniContractCover"]
             #[doc(hidden)]
-            pub fn assume_unless_vacuous(cond: bool, msg: &'static str) {
-                let _ = cond;
-            }
-
-            #[inline(never)]
-            #[rustc_diagnostic_item = "KaniAssumeUnlessVacuous"]
-            #[cfg(feature = "concrete_playback")]
-            #[doc(hidden)]
-            pub fn assume_unless_vacuous(cond: bool, msg: &'static str) {
-                assert!(cond, "{}", msg);
-            }
+            pub const fn contract_cover(_cond: bool, _msg: &'static str) {}
 
             /// A way to break the ownerhip rules. Only used by contracts where we can
             /// guarantee it is done safely.
diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs
index 800f95504d3f..7804825a2550 100644
--- a/library/kani_macros/src/sysroot/contracts/check.rs
+++ b/library/kani_macros/src/sysroot/contracts/check.rs
@@ -24,7 +24,8 @@ impl<'a> ContractConditionsHandler<'a> {
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
                 quote!({
-                    kani::internal::assume_unless_vacuous(#attr, "The contract's precondition (i.e., the conjunction of the #[requires(...)] clauses' bodies) is satisfiable.");
+                    kani::assume(#attr);
+                    kani::internal::contract_cover(#attr, "The contract's precondition is satisfiable.");
                     #(#body_stmts)*
                 })
             }
@@ -46,6 +47,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#assumes)*
                     #remembers
                     #(#rest_of_body)*
+                    kani::internal::contract_cover(#ensures_clause, "The contract's postcondition is reachable.");
                     #exec_postconditions
                     #return_expr
                 })
diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs
index 1fde077be171..49d101dad32a 100644
--- a/library/kani_macros/src/sysroot/contracts/helpers.rs
+++ b/library/kani_macros/src/sysroot/contracts/helpers.rs
@@ -201,20 +201,17 @@ pub fn split_for_remembers(stmts: &[Stmt], closure_type: ClosureType) -> (&[Stmt
     let mut pos = 0;
 
     let check_str = match closure_type {
-        ClosureType::Check => "kani::internal::assume_unless_vacuous",
-        ClosureType::Replace => "kani::assert",
+        ClosureType::Check => "assume",
+        ClosureType::Replace => "assert",
     };
 
     for stmt in stmts {
         if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt {
             if let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref() {
-                let first_three_idents = segments
-                    .iter()
-                    .take(3)
-                    .map(|sgmt| sgmt.ident.to_string())
-                    .collect::<Vec<_>>()
-                    .join("::");
-                if first_three_idents.contains(check_str) {
+                let first_two_idents =
+                    segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::<Vec<_>>();
+
+                if first_two_idents == vec!["kani", check_str] {
                     pos += 1;
                 }
             }
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index c90128c170e9..a8046d8a7521 100644
--- a/library/kani_macros/src/sysroot/contracts/mod.rs
+++ b/library/kani_macros/src/sysroot/contracts/mod.rs
@@ -58,6 +58,10 @@
 //! added before the body and postconditions after as well as injected before
 //! every `return` (see [`PostconditionInjector`]). All arguments are captured
 //! by the closure.
+//! We also inject contract_cover checks after the precondition and before the postcondition.
+//! The precondition cover checks ensure that the precondition is satisfiable; i.e.,
+//! that the precondition does not empty the search space and produce a vacuous proof.
+//! The postcondition cover checks ensure that the postcondition is reachable.
 //!
 //! ## Replace Function
 //!
@@ -168,7 +172,8 @@
 //!                                let mut __kani_check_div =
 //!                                    || -> u32
 //!                                        {
-//!                                            kani::internal::assume_unless_vacuous(divisor != 0);
+//!                                            kani::assume(divisor != 0);
+//!                                            kani::internal::contract_cover(divisor != 0, "The contract's precondition is satisfiable.");
 //!                                            let _wrapper_arg = ();
 //!                                            #[kanitool::is_contract_generated(wrapper)]
 //!                                            #[allow(dead_code, unused_variables, unused_mut)]
@@ -176,6 +181,11 @@
 //!                                                |_wrapper_arg| -> u32 { dividend / divisor };
 //!                                            let result_kani_internal: u32 =
 //!                                                __kani_modifies_div(_wrapper_arg);
+//!                                            kani::internal::contract_cover(
+//!                                                 kani::internal::apply_closure(|result: &u32|
+//!                                                     *result <= dividend,
+//!                                                     &result_kani_internal),
+//!                                                 "The contract's postcondition is reachable.");
 //!                                            kani::assert(kani::internal::apply_closure(|result: &u32|
 //!                                                        *result <= dividend, &result_kani_internal),
 //!                                                "|result : &u32| *result <= dividend");
@@ -210,7 +220,8 @@
 //!             let mut __kani_check_div =
 //!                 || -> u32
 //!                     {
-//!                         kani::internal::assume_unless_vacuous(divisor != 0);
+//!                         kani::assume(divisor != 0);
+//!                         kani::internal::contract_cover(divisor != 0, "The contract's precondition is satisfiable.");
 //!                         let _wrapper_arg = ();
 //!                         #[kanitool::is_contract_generated(wrapper)]
 //!                         #[allow(dead_code, unused_variables, unused_mut)]
@@ -218,6 +229,11 @@
 //!                             |_wrapper_arg| -> u32 { dividend / divisor };
 //!                         let result_kani_internal: u32 =
 //!                             __kani_modifies_div(_wrapper_arg);
+//!                         kani::internal::contract_cover(
+//!                             kani::internal::apply_closure(|result: &u32|
+//!                                 *result <= dividend,
+//!                                 &result_kani_internal),
+//!                             "The contract's postcondition is reachable.");
 //!                         kani::assert(kani::internal::apply_closure(|result: &u32|
 //!                                     *result <= dividend, &result_kani_internal),
 //!                             "|result : &u32| *result <= dividend");
@@ -310,7 +326,8 @@
 //!                                let mut __kani_check_modify =
 //!                                    ||
 //!                                        {
-//!                                            kani::internal::assume_unless_vacuous(divisor != 0);
+//!                                            kani::assume(divisor != 0);
+//!                                            kani::internal::contract_cover(*ptr < 100, "The contract's precondition is satisfiable.");
 //!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                                            let _wrapper_arg = (ptr as *const _,);
@@ -320,9 +337,21 @@
 //!                                                |_wrapper_arg| { *ptr += 1; };
 //!                                            let result_kani_internal: () =
 //!                                                __kani_modifies_modify(_wrapper_arg);
+//!                                            kani::internal::contract_cover(
+//!                                                kani::internal::apply_closure(|result|
+//!                                                    (remember_kani_internal_2e780b148d45b5c8) == * ptr,
+//!                                                    &result_kani_internal
+//!                                                ),
+//!                                            "The contract's postcondition is reachable.");
 //!                                            kani::assert(kani::internal::apply_closure(|result|
 //!                                                        (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                                    &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
+//!                                            kani::internal::contract_cover(
+//!                                                kani::internal::apply_closure(|result|
+//!                                                    (remember_kani_internal_2e780b148d45b5c8) == * ptr,
+//!                                                    &result_kani_internal
+//!                                                ),
+//!                                            "The contract's postcondition is reachable.");
 //!                                            kani::assert(kani::internal::apply_closure(|result|
 //!                                                        (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                                    &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
@@ -375,9 +404,19 @@
 //!                             |_wrapper_arg| { *ptr += 1; };
 //!                         let result_kani_internal: () =
 //!                             __kani_modifies_modify(_wrapper_arg);
+//!                         kani::internal::contract_cover(
+//!                            kani::internal::apply_closure(|result|
+//!                              (remember_kani_internal_2e780b148d45b5c8) == * ptr,
+//!                              &result_kani_internal
+//!                         ),
 //!                         kani::assert(kani::internal::apply_closure(|result|
 //!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                 &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
+//!                         kani::internal::contract_cover(
+//!                            kani::internal::apply_closure(|result|
+//!                              (remember_kani_internal_2e780b148d45b5c8) == * ptr,
+//!                              &result_kani_internal
+//!                         ),
 //!                         kani::assert(kani::internal::apply_closure(|result|
 //!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                 &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
@@ -549,5 +588,7 @@ fn contract_main(
         Err(e) => return e.into_compile_error().into(),
     };
 
-    handler.dispatch_on(function_state).into()
+    let res = handler.dispatch_on(function_state).into();
+    println!("{}", &res);
+    res
 }
diff --git a/tests/expected/function-contract/cover_contract/never_type.expected b/tests/expected/function-contract/cover_contract/never_type.expected
new file mode 100644
index 000000000000..53e2ce503bf7
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/never_type.expected
@@ -0,0 +1,9 @@
+contract_cover.2\
+	 - Status: FAILURE\
+	 - Description: "The contract's postcondition is reachable."
+
+unwind.0\
+    - Status: FAILURE\
+    - Description: "unwinding assertion loop 0"
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/cover_contract/never_type_fixme.rs b/tests/expected/function-contract/cover_contract/never_type_fixme.rs
new file mode 100644
index 000000000000..d14f3173ab3a
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/never_type_fixme.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Unreachable postcondition because the function never returns.
+// Kani should fail verification because the postcondition is unreachable,
+// but currently doesn't generate the postcondition check at all
+// (although verification still fails because of the unwinding error).
+// We may need special never type detection for this case.
+
+#![feature(never_type)]
+
+#[kani::requires(true)]
+#[kani::ensures(|result: &!| true)]
+fn never_return() -> ! {
+    let x = 7;
+    loop {}
+}
+
+// Unreachable postcondition because the function never returns
+#[kani::proof_for_contract(never_return)]
+#[kani::unwind(5)]
+fn prove_never_return() {
+    never_return();
+}
diff --git a/tests/expected/function-contract/cover_contract/unreachable_postcondition.expected b/tests/expected/function-contract/cover_contract/unreachable_postcondition.expected
new file mode 100644
index 000000000000..fd4ed7de24d3
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/unreachable_postcondition.expected
@@ -0,0 +1,24 @@
+
+contract_cover.1\
+	 - Status: FAILURE\
+	 - Description: "The contract's postcondition is reachable."
+
+unwind.0\
+	 - Status: FAILURE\
+	 - Description: "unwinding assertion loop 0"
+
+VERIFICATION:- FAILED
+
+assertion.1\
+	 - Status: FAILURE\
+	 - Description: "panic"
+
+contract_cover.1\
+	 - Status: SUCCESS\
+	 - Description: "The contract's precondition is satisfiable."
+
+contract_cover.2\
+	 - Status: FAILURE\
+	 - Description: "The contract's postcondition is reachable."
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/cover_contract/unreachable_postcondition.rs b/tests/expected/function-contract/cover_contract/unreachable_postcondition.rs
new file mode 100644
index 000000000000..982a04f4c63c
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/unreachable_postcondition.rs
@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test `conver_contract` functionality, which fails verification for a vacuous precondition
+// or unreachable postcondition.
+// See https://github.com/model-checking/kani/issues/2793
+
+// Unreachable postcondition.
+// The precondition is satisfiable, but the postcondition is unreachable because the code panics.
+#[kani::requires(a > 5)]
+#[kani::ensures(|result: &u32| *result == a)]
+fn unreachable_postcondition(a: u32) -> u32 {
+    panic!("panic")
+}
+
+#[kani::proof_for_contract(unreachable_postcondition)]
+fn prove_unreachable_postcondition() {
+    let x: u32 = kani::any();
+    unreachable_postcondition(x);
+}
+
+#[kani::ensures(|result: &u32| *result == 7)]
+fn never_return() -> u32 {
+    loop {}
+    7
+}
+
+// Unreachable postcondition because the function never returns
+#[kani::proof_for_contract(never_return)]
+#[kani::unwind(5)]
+fn prove_never_return() {
+    never_return();
+}
diff --git a/tests/expected/function-contract/cover_contract/vacuous_precondition.expected b/tests/expected/function-contract/cover_contract/vacuous_precondition.expected
new file mode 100644
index 000000000000..fa9a2a1d2e8a
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/vacuous_precondition.expected
@@ -0,0 +1,23 @@
+contract_cover.1\
+	 - Status: FAILURE\
+	 - Description: "The contract's precondition is satisfiable."
+
+contract_cover.2\
+	 - Status: FAILURE\
+	 - Description: "The contract's postcondition is reachable."
+
+VERIFICATION:- FAILED
+
+contract_cover.1\
+	 - Status: SUCCESS\
+	 - Description: "The contract's precondition is satisfiable."
+
+contract_cover.2\
+	 - Status: FAILURE\
+	 - Description: "The contract's precondition is satisfiable."
+
+contract_cover.3\
+	 - Status: FAILURE\
+	 - Description: "The contract's postcondition is reachable."
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/cover_contract/vacuous_precondition.rs b/tests/expected/function-contract/cover_contract/vacuous_precondition.rs
new file mode 100644
index 000000000000..27f239a3f08c
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/vacuous_precondition.rs
@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test `conver_contract` functionality, which fails verification for a vacuous precondition
+// or unreachable postcondition.
+// See https://github.com/model-checking/kani/issues/2793
+
+// Vacuous precondition; separate requires clauses
+#[kani::requires(a > 5)]
+#[kani::requires(a < 4)]
+#[kani::ensures(|result: &u32| *result == a)]
+fn separate_requires(a: u32) -> u32 {
+    panic!("This code is never tested")
+}
+
+#[kani::proof_for_contract(separate_requires)]
+fn prove_separate_requires() {
+    let x: u32 = kani::any();
+    separate_requires(x);
+}
+
+// Vacuous precondition; single requires clause
+#[kani::requires(a > 5 && a < 4)]
+#[kani::ensures(|result: &u32| *result == a)]
+fn conjoined_requires(a: u32) -> u32 {
+    panic!("This code is never tested")
+}
+
+#[kani::proof_for_contract(conjoined_requires)]
+fn prove_conjoined_requires() {
+    let x: u32 = kani::any();
+    conjoined_requires(x);
+}
diff --git a/tests/expected/function-contract/vacuous_requires_fail.expected b/tests/expected/function-contract/vacuous_requires_fail.expected
deleted file mode 100644
index 6bea81e7987b..000000000000
--- a/tests/expected/function-contract/vacuous_requires_fail.expected
+++ /dev/null
@@ -1,5 +0,0 @@
-Failed Checks: The contract's precondition (i.e., the conjunction of the #[requires(...)] clauses' bodies) is satisfiable.
-
-VERIFICATION:- FAILED
-
-Verification failed for - prove_buggy
\ No newline at end of file
diff --git a/tests/expected/function-contract/vacuous_requires_fail.rs b/tests/expected/function-contract/vacuous_requires_fail.rs
deleted file mode 100644
index 9ffaf65fed76..000000000000
--- a/tests/expected/function-contract/vacuous_requires_fail.rs
+++ /dev/null
@@ -1,17 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
-
-// See https://github.com/model-checking/kani/issues/2793
-#[kani::requires(a > 5)]
-#[kani::requires(a < 4)]
-#[kani::ensures(|result| *result == a)]
-fn buggy(a: u32) -> u32 {
-    panic!("This code is never tested")
-}
-
-#[kani::proof_for_contract(buggy)]
-fn prove_buggy() {
-    let x: u32 = kani::any();
-    buggy(x);
-}
diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected
index 41ec2098c806..094dc6b7993e 100644
--- a/tests/expected/function-contract/valid_ptr.expected
+++ b/tests/expected/function-contract/valid_ptr.expected
@@ -1,6 +1,7 @@
 Checking harness pre_condition::harness_invalid_ptr...
-assume_unless_vacuous\
-	 - Status: FAILURE
+contract_cover.1\
+	 - Status: FAILURE\
+	 - Description: "The contract's precondition is satisfiable."
 VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
 
 Checking harness pre_condition::harness_stack_ptr...
@@ -10,8 +11,7 @@ Checking harness pre_condition::harness_head_ptr...
 VERIFICATION:- SUCCESSFUL
 
 Checking harness post_condition::harness...
-assume_unless_vacuous\
-	 - Status: FAILURE
-VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
-
-Complete - 2 successfully verified harnesses, 2 failures, 4 total
+assertion.1\
+	 - Status: FAILURE\
+	 - Description: "|result| kani::mem::can_dereference((*result).0)"
+VERIFICATION:- FAILED