`goto-instrument` invariant violation with generated harness with fn pointer when contract with same signature exists

[archigup]

I get an invariant violation error from goto-instrument which involves a generated harness, an enforced contract for a function with a fn pointer arg that calls that fn ptr, and a contract with the same signature as the function pointer.

The CBMC version is commit 062962c (not actually 6.7.1 in output below).

Code to reproduce is below.

If foo does not call fn, the error does not occur. If unused_contract is removed, the error does not occur.

#include <stddef.h>

void unused_contract(void *ctx) __CPROVER_ensures(1);

void foo(void (*fn)(void *ctx)) __CPROVER_ensures(1) {
   fn(NULL);
}

$ goto-cc -c test.c -o test.goto
$ goto-harness test.goto test.goto --harness-function-name main --harness-type call-function --function foo
$ goto-cc -o test.goto test.goto
$ goto-instrument test.goto test.goto --dfcc main --enforce-contract foo
Reading GOTO program from 'test.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'main'
Wrapping 'foo' with contract 'foo' in CHECK mode
Instrumenting 'type_constructor_ptr_'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 0 targets
Removing unused functions
Updating init function
Setting entry point to main
--- begin invariant violation report ---
Invariant check failed
File: /build/source/src/util/namespace.h:49 function: lookup
Condition: !not_found
Reason: we are assuming that a name exists in the namespace when this function is called - identifier unused_contract::ctx was not found
Backtrace:
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xe78073]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xe79189]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x5642cd]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xc6db4e]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xc6f277]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xa4a552]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xa46724]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xa492c0]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0xa49362]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x56c714]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x56fa14]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x56299a]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x558a44]
/nix/store/q4wq65gl3r8fy746v9bbwgx4gzn0r2kl-glibc-2.40-66/lib/libc.so.6(+0x2a4d8) [0x7c3c1682a4d8]
/nix/store/q4wq65gl3r8fy746v9bbwgx4gzn0r2kl-glibc-2.40-66/lib/libc.so.6(__libc_start_main+0x8b) [0x7c3c1682a59b]
/nix/store/i0bvi6vyhah9p2m71cb43msls1di3jg5-cbmc-6.7.1/bin/goto-instrument() [0x563955]


--- end invariant violation report ---
aborted
6$ 

[remi-delmas-3000]

It could be due to aggressive removal of unused functions between passes