CONTRACTS: make ptr_pred_ctx_reset_call call reset instead of init

regression/contracts-dfcc/test_is_fresh_enforce_requires_fail_separation/main.c

@@ -0,0 +1,14 @@
+// clang-format off
+int *foo(int *p)
+  __CPROVER_requires(__CPROVER_is_fresh(p, sizeof(int)))
+  __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)))
+// clang-format on
+{
+  return p;
+}
+
+int main()
+{
+  int *p;
+  foo(p);
+}

regression/contracts-dfcc/test_is_fresh_enforce_requires_fail_separation/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that __CPROVER_is_fresh separation checks fail when the
+return value aliases with a parameter that was required to be fresh.

src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

@@ -903,7 +903,7 @@ const code_function_callt dfcc_libraryt::ptr_pred_ctx_reset_call(
   const source_locationt &source_location)
 {
   code_function_callt call(
-    dfcc_fun_symbol[dfcc_funt::PTR_PRED_CTX_INIT].symbol_expr(),
+    dfcc_fun_symbol[dfcc_funt::PTR_PRED_CTX_RESET].symbol_expr(),
     {ptr_pred_ctx_ptr});
   call.add_source_location() = source_location;
   return call;