fix tests

library/kani_macros/src/sysroot/contracts/helpers.rs

@@ -201,17 +201,20 @@ pub fn split_for_remembers(stmts: &[Stmt], closure_type: ClosureType) -> (&[Stmt
     let mut pos = 0;
 
     let check_str = match closure_type {
-        ClosureType::Check => "assume",
-        ClosureType::Replace => "assert",
+        ClosureType::Check => "kani::internal::assume_unless_vacuous",
+        ClosureType::Replace => "kani::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_two_idents =
-                    segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::<Vec<_>>();
-
-                if first_two_idents == vec!["kani", check_str] {
+                let first_three_idents = segments
+                    .iter()
+                    .take(3)
+                    .map(|sgmt| sgmt.ident.to_string())
+                    .collect::<Vec<_>>()
+                    .join("::");
+                if first_three_idents.contains(check_str) {
                     pos += 1;
                 }
             }

tests/expected/function-contract/valid_ptr.expected

@@ -1,10 +1,17 @@
 Checking harness pre_condition::harness_invalid_ptr...
-VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+assume_unless_vacuous\
+	 - Status: FAILURE
+VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
 
 Checking harness pre_condition::harness_stack_ptr...
 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...
+assume_unless_vacuous\
+	 - Status: FAILURE
+VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
+
+Complete - 2 successfully verified harnesses, 2 failures, 4 total

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 _)