don't use is fresh under negation

Remi Delmas · Remi Delmas · commit 5372a0cb6a02 · 2025-01-25T16:20:28.000-05:00
diff --git 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
 {

Original file line number	Diff line number	Diff line change
`@@ -21,7 +21,6 @@ int foo(int *x)`
`21`	`21`	`ptr_ok(x))`
`22`	`22`	`__CPROVER_ensures(`
`23`	`23`	`!ptr_ok(x) &&`
`24`		`- !__CPROVER_is_fresh(x, sizeof(int)) &&`
`25`	`24`	`return_ok(__CPROVER_return_value, x))`
`26`	`25`	`// clang-format on`
`27`	`26`	`{`