Invariant violation in local_bitvector_analysist when --export-file-local-symbols is used

[remi-delmas-3000]

// file a.c
static void foo(int)
{
  __CPROVER_assert(0, "reachable");
}

// file main.c
void __CPROVER_file_local_a_c_foo(int);
int main() 
{
 __CPROVER_file_local_a_c_foo(0);
  return 0;
}

❯ goto-cc --export-file-local-symbols a.c main.c -o main.out
❯ cbmc main.out
CBMC version 5.95.1 (cbmc-5.95.1-dirty) 64-bit x86_64 macos
Reading GOTO program from file main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
--- begin invariant violation report ---
Invariant check failed
File: /Users/delmasrd/projects/cbmc/src/util/namespace.h:51 function: lookup
Condition: !not_found
Reason: we are assuming that a name exists in the namespace when this function is called - identifier  was not found
Backtrace:
0   cbmc                                0x000000010df08794 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 68
1   cbmc                                0x000000010df08ccf _Z13get_backtracev + 63
2   cbmc                                0x000000010d40abde _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 46
3   cbmc                                0x000000010d40ab73 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 51
4   cbmc                                0x000000010d40e8ce _ZNK15namespace_baset6lookupERK8dstringt + 222
5   cbmc                                0x000000010d7e87c0 _ZN25local_bitvector_analysist10is_trackedERK8dstringt + 128
6   cbmc                                0x000000010d7e9edf _ZN25local_bitvector_analysist5buildEv + 319
7   cbmc                                0x000000010d91e7fc _ZN25local_bitvector_analysistC2ERK14goto_functiontRK10namespacet + 156
8   cbmc                                0x000000010d91e725 _ZN25local_bitvector_analysistC1ERK14goto_functiontRK10namespacet + 37
9   cbmc                                0x000000010d90ac70 _Z16util_make_uniqueI25local_bitvector_analysistJR14goto_functiontRK10namespacetEENSt3__110unique_ptrIT_NS6_14default_deleteIS8_EEEEDpOT0_ + 64
10  cbmc                                0x000000010d908e5c _ZN13goto_check_ct10goto_checkERK8dstringtR14goto_functiont + 220
11  cbmc                                0x000000010d90c19a _Z12goto_check_cRK10namespacetRK8optionstR15goto_functionstR16message_handlert + 282
12  cbmc                                0x000000010d90c262 _Z12goto_check_cRK8optionstR11goto_modeltR16message_handlert + 66
13  cbmc                                0x000000010da18675 _Z20process_goto_programR11goto_modeltRK8optionstR8messaget + 1157
14  cbmc                                0x000000010d42c0b9 _ZN19cbmc_parse_optionst20process_goto_programER11goto_modeltRK8optionstR8messaget + 345
15  cbmc                                0x000000010d42aacd _ZN19cbmc_parse_optionst16get_goto_programER11goto_modeltRK8optionstRK8cmdlinetR19ui_message_handlert + 397
16  cbmc                                0x000000010d4289d9 _ZN19cbmc_parse_optionst4doitEv + 2921
17  cbmc                                0x000000010df5ca91 _ZN19parse_options_baset4mainEv + 1665
18  cbmc                                0x000000010d408ecf main + 63
19  dyld                                0x00007ff80b92b366 start + 1942


--- end invariant violation report ---
[1]    73412 abort      cbmc main.out

The invariant violation does not occur if a.c is compiled separately with --export-file-local-symbols and then linked.

❯ goto-cc --export-file-local-symbols a.c -o a.out
❯ goto-cc a.out main.c -o main.out
❯ cbmc main.out
CBMC version 5.95.1 (cbmc-5.95.1-dirty) 64-bit x86_64 macos
Reading GOTO program from file main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00303751s
size of program expression: 24 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 3.9559e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000312894s
Running propositional reduction
Post-processing
Runtime Post-process: 2.4725e-05s
Solving with MiniSAT 2.2.1 with simplifier
0 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000116481s
Runtime decision procedure: 0.000537371s

** Results:
a.c function foo
[foo.assertion.1] line 3 reachable: FAILURE

** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

CBMC version: 5.95.1
Operating system: macos
Exact command line resulting in the issue: see above
What behaviour did you expect: failed assertion
What happened instead: invariant violation