diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index 4fce3f7494b6..8e0e23e0334c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -48,6 +48,9 @@ pub enum PropertyClass {
     ///
     /// 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.
     ///
@@ -150,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 7d63315e1e13..a88d12e794a0 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -82,6 +82,45 @@ impl GotocHook for Cover {
     }
 }
 
+/// 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, "KaniContractCover")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        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 caller_loc = gcx.codegen_caller_span_stable(span);
+
+        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 Assume;
 impl GotocHook for Assume {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
@@ -594,6 +633,7 @@ pub fn fn_hooks() -> GotocHooks {
         hooks: vec![
             Rc::new(Panic),
             Rc::new(Assume),
+            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 a34f6815e3dd..17e29a04297f 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -95,6 +95,7 @@ pub struct PropertyId {
 }
 
 impl Property {
+    const CONTRACT_COVER_PROPERTY_CLASS: &'static str = "contract_cover";
     const COVER_PROPERTY_CLASS: &'static str = "cover";
     const COVERAGE_PROPERTY_CLASS: &'static str = "code_coverage";
 
@@ -102,6 +103,11 @@ impl Property {
         self.property_id.class.clone()
     }
 
+    /// 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
     pub fn is_code_coverage_property(&self) -> bool {
         self.property_id.class == Self::COVERAGE_PROPERTY_CLASS
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index 5c10d08badb6..7334ef780080 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -512,8 +512,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);
-    let results_after_code_coverage = update_results_of_code_covererage_checks(updated_properties);
-    update_results_of_cover_checks(results_after_code_coverage)
+    let results_after_code_coverage = update_results_of_code_coverage_checks(updated_properties);
+    update_results_of_cover_checks(results_after_code_coverage, has_failed_unwinding_asserts)
 }
 
 /// Determines if there is property with status `FAILURE` and the given description
@@ -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 {
@@ -647,7 +647,17 @@ fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Ve
 /// Note that if the cover property was unreachable, its status at this point
 /// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since
 /// `update_properties_with_reach_status` is called beforehand
-fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property> {
+///
+/// Although regular cover properties do not fail verification, contract cover properties do.
+/// If the assert(!cond) is unreachable or successful, then fail.
+/// Also fail if the status is undetermined and there are failed unwinding asserts; if we didn't unwind enough,
+/// we know that the postcondition is unreachable.
+/// If the status is undetermined for another reason (e.g., unsupported constructs), leave the result as undetermined.
+/// If the status is failure (as expected), succeed.
+fn update_results_of_cover_checks(
+    mut properties: Vec<Property>,
+    has_failed_unwinding_asserts: bool,
+) -> Vec<Property> {
     for prop in properties.iter_mut() {
         if prop.is_cover_property() {
             if prop.status == CheckStatus::Success {
@@ -655,6 +665,15 @@ 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_contract_cover_property() {
+            if prop.status == CheckStatus::Unreachable
+                || prop.status == CheckStatus::Success
+                || (prop.status == CheckStatus::Undetermined && has_failed_unwinding_asserts)
+            {
+                prop.status = CheckStatus::Failure;
+            } else if prop.status == CheckStatus::Failure {
+                prop.status = CheckStatus::Success;
+            }
         }
     }
     properties
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 4919473bf0f1..e45a24d4f016 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -199,7 +199,7 @@ macro_rules! kani_intrinsics {
         #[inline(never)]
         #[doc(hidden)]
         pub fn any_modifies<T>() -> T {
-            // This function should not be reacheable.
+            // This function should not be reachable.
             // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
             // otherwise, this might not be properly instantiate. We mark this as unreachable to make
             // sure Kani doesn't report any false positives.
@@ -291,7 +291,7 @@ macro_rules! kani_intrinsics {
         /// function, both cause Kani to produce a warning since we don't support caller location.
         /// (see https://github.com/model-checking/kani/issues/2010).
         ///
-        /// This function is dead, since its caller is always  handled via a hook anyway,
+        /// This function is dead, since its caller is always handled via a hook anyway,
         /// so we just need to put a body that rustc does not complain about.
         /// An infinite loop works out nicely.
         fn kani_intrinsic<T>() -> T {
@@ -346,6 +346,14 @@ macro_rules! kani_intrinsics {
                 }
             }
 
+            /// This function is only used for function contract instrumentation.
+            /// 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 = "KaniContractCover"]
+            #[doc(hidden)]
+            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.
             #[inline(never)]
@@ -383,7 +391,7 @@ macro_rules! kani_intrinsics {
             #[inline(never)]
             #[doc(hidden)]
             pub unsafe fn write_any<T: ?Sized>(_pointer: *mut T) {
-                // This function should not be reacheable.
+                // This function should not be reachable.
                 // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
                 // otherwise, this might not be properly instantiate. We mark this as unreachable to make
                 // sure Kani doesn't report any false positives.
diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs
index 863cf882f063..7804825a2550 100644
--- a/library/kani_macros/src/sysroot/contracts/check.rs
+++ b/library/kani_macros/src/sysroot/contracts/check.rs
@@ -25,6 +25,7 @@ impl<'a> ContractConditionsHandler<'a> {
             ContractConditionsData::Requires { attr } => {
                 quote!({
                     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/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index 41be536ffb6d..d0d9bfc96ed6 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
 //!
@@ -169,6 +173,7 @@
 //!                                    || -> u32
 //!                                        {
 //!                                            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");
@@ -211,6 +221,7 @@
 //!                 || -> u32
 //!                     {
 //!                         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");
@@ -311,6 +327,7 @@
 //!                                    ||
 //!                                        {
 //!                                            kani::assume(*ptr < 100);
+//!                                            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");
@@ -367,6 +396,7 @@
 //!                 ||
 //!                     {
 //!                         kani::assume(*ptr < 100);
+//!                         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 _,);
@@ -376,9 +406,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");
diff --git a/tests/expected/function-contract/cover_contract/never_type_fixme.expected b/tests/expected/function-contract/cover_contract/never_type_fixme.expected
new file mode 100644
index 000000000000..53e2ce503bf7
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/never_type_fixme.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/undetermined_postcondition.expected b/tests/expected/function-contract/cover_contract/undetermined_postcondition.expected
new file mode 100644
index 000000000000..6d7541ff1b23
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/undetermined_postcondition.expected
@@ -0,0 +1,9 @@
+
+contract_cover.2\
+	 - Status: UNDETERMINED\
+	 - Description: "The contract's postcondition is reachable."
+
+unsupported_construct.1\
+	 - Status: FAILURE
+
+VERIFICATION:- FAILED
\ No newline at end of file
diff --git a/tests/expected/function-contract/cover_contract/undetermined_postcondition.rs b/tests/expected/function-contract/cover_contract/undetermined_postcondition.rs
new file mode 100644
index 000000000000..e3d27a36ac56
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/undetermined_postcondition.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test `cover_contract` functionality, which fails verification for a unsatisfiable precondition
+// or unreachable postcondition.
+// See https://github.com/model-checking/kani/issues/2793
+
+// Undetermined whether we can reach the postcondition because we encounter an unsupported construct.
+
+#[kani::proof_for_contract(unsupp)]
+fn undetermined_example() {
+    let mut x = 0;
+    unsupp(&mut x);
+    assert!(x == 0);
+}
+
+#[kani::requires(true)]
+#[kani::ensures(|res| *res == *x)]
+fn unsupp(x: &mut u8) -> u8 {
+    unsafe {
+        std::arch::asm!("nop");
+    }
+    *x
+}
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..182a5e90b207
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/unreachable_postcondition.rs
@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test `cover_contract` functionality, which fails verification for a unsatisfiable precondition
+// or unreachable postcondition.
+// See https://github.com/model-checking/kani/issues/2793
+
+// Test that verification fails for an unreachable postcondition.
+
+// The precondition is satisfiable, but the postcondition is unreachable because the code panics.
+// Test that in the case where the postcondition check's property status is unreachable (because the function panics)
+// we change the status to failure.
+#[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);
+}
+
+// Unreachable postcondition because the function never returns.
+// Test that in the case where the postcondition check's property status is undetermined because of unwinding failures,
+// we change the status to failure.
+#[kani::ensures(|result: &u32| *result == 7)]
+fn never_return() -> u32 {
+    loop {}
+    7
+}
+
+#[kani::proof_for_contract(never_return)]
+#[kani::unwind(5)]
+fn prove_never_return() {
+    never_return();
+}
diff --git a/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.expected b/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.expected
new file mode 100644
index 000000000000..fa9a2a1d2e8a
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/unsatisfiable_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/unsatisfiable_precondition.rs b/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.rs
new file mode 100644
index 000000000000..80b7ac3b0e5c
--- /dev/null
+++ b/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.rs
@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test `cover_contract` functionality, which fails verification for an unsatisfiable precondition
+// or unreachable postcondition.
+// See https://github.com/model-checking/kani/issues/2793
+
+// Test that verification fails for unsatisfiable preconditions.
+
+// Unsatisfiable precondition; separate requires clauses.
+// The postcondition is unreachable because of the unsatisfiable precondition.
+#[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);
+}
+
+// Unsatisfiable precondition; single requires clause
+// The postcondition is unreachable because of the unsatisfiable precondition.
+#[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/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected
index 4014a0723029..094dc6b7993e 100644
--- a/tests/expected/function-contract/valid_ptr.expected
+++ b/tests/expected/function-contract/valid_ptr.expected
@@ -1,5 +1,8 @@
 Checking harness pre_condition::harness_invalid_ptr...
-VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+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...
 VERIFICATION:- SUCCESSFUL
@@ -7,4 +10,8 @@ VERIFICATION:- SUCCESSFUL
 Checking harness pre_condition::harness_head_ptr...
 VERIFICATION:- SUCCESSFUL
 
-Complete - 3 successfully verified harnesses, 0 failures, 3 total
+Checking harness post_condition::harness...
+assertion.1\
+	 - Status: FAILURE\
+	 - Description: "|result| kani::mem::can_dereference((*result).0)"
+VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs
index 2047a46caf4f..af49b5cd053b 100644
--- a/tests/expected/function-contract/valid_ptr.rs
+++ b/tests/expected/function-contract/valid_ptr.rs
@@ -35,12 +35,9 @@ mod pre_condition {
     }
 }
 
-/// TODO: Enable once we fix: <https://github.com/model-checking/kani/issues/2997>
-#[cfg(not_supported)]
 mod post_condition {
-
     /// This contract should fail since we are creating a dangling pointer.
-    #[kani::ensures(kani::mem::can_dereference(result.0))]
+    #[kani::ensures(|result| kani::mem::can_dereference((*result).0))]
     unsafe fn new_invalid_ptr() -> PtrWrapper<char> {
         let var = 'c';
         PtrWrapper(&var as *const _)
