diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index c677bb5a3b1..792ba50d430 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1308,7 +1308,6 @@ __CPROVER_HIDE:; // __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool(); // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak; - // record fresh object in the object set #ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp index 45c960abd0e..a5fbfea3fa7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp @@ -17,6 +17,7 @@ Date: Jan 2025 #include #include #include + #include "dfcc_cfg_info.h" #include "dfcc_library.h"