From 5372a0cb6a02ca1bdd1a14d68dca710c4e315229 Mon Sep 17 00:00:00 2001
From: Remi Delmas <delmasrd@amazon.com>
Date: Sat, 25 Jan 2025 16:20:28 -0500
Subject: [PATCH] don't use is fresh under negation

---
 regression/contracts-dfcc/test_scalar_memory_enforce/main.c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/regression/contracts-dfcc/test_scalar_memory_enforce/main.c b/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
index b22c93fe00f..ff6bbd8a739 100644
--- a/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
+++ b/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
@@ -21,7 +21,6 @@ int foo(int *x)
     ptr_ok(x))
   __CPROVER_ensures(
     !ptr_ok(x) &&
-    !__CPROVER_is_fresh(x, sizeof(int)) &&
     return_ok(__CPROVER_return_value, x))
 // clang-format on
 {