From ed261e349614b4a85b26eb83324b89dd0e9567a1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 22 Jan 2025 11:31:41 +0000
Subject: [PATCH] Enable valid_ptr post_condition harnesses

With #2997 resolved this is expected to work.
---
 tests/expected/function-contract/valid_ptr.rs | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs
index 2047a46caf4f..abfa037dcc48 100644
--- a/tests/expected/function-contract/valid_ptr.rs
+++ b/tests/expected/function-contract/valid_ptr.rs
@@ -3,8 +3,6 @@
 // kani-flags: -Zfunction-contracts -Zmem-predicates
 
 //! Test that it is sound to use memory predicates inside a contract pre-condition.
-//! We cannot validate post-condition yet. This can be done once we fix:
-//! <https://github.com/model-checking/kani/issues/2997>
 
 mod pre_condition {
     /// This contract should succeed only if the input is a valid pointer.
@@ -35,8 +33,6 @@ 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.