Invariant violation in get_string_constant on an SV-COMP benchmark

[lou1306]

CBMC version: 6.4.1
Operating system: macOS 14.7.3
Exact command line resulting in the issue: cbmc --unwind 1 if_etherip-unreach-call.i
What behaviour did you expect: cbmc generates GOTO program, then performs BMC
What happened instead: Invariant violation is reported during GOTO program generation

Details: I am running CBMC on some programs from the SV-COMP benchmarks suite (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/).

When I run it on sv-benchmarks/c/openbsd-6.2/if_etherip-unreach-call.i (attached here: if_etherip-unreach-call.i.txt), it fails almost immediately with an invariant violation report that can be found below.

I have looked around, but no other issue seems to mention this specific problem with get_string_constant.

CBMC version 6.4.1 (cbmc-6.4.1) 64-bit arm64 macos
Type-checking if_etherip-unreach-call
Generating GOTO Program
--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20241128-12508-57225x/src/ansi-c/goto-conversion/goto_convert.cpp:2109 function: get_string_constant
Condition: expected string constant
Reason: !res
Backtrace:
0   cbmc                                0x00000001013daa30 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 124
1   cbmc                                0x00000001013dada4 _Z13get_backtracev + 44
2   cbmc                                0x0000000100f47c50 _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 60
3   cbmc                                0x0000000101125090 _Z24report_invariant_failureIJRK16source_locationtNSt3__112basic_stringIcNS3_11char_traitsIcEENS3_9allocatorIcEEEEEEvRKS9_SB_iS9_S9_DpOT_ + 88
4   cbmc                                0x0000000101122364 _ZN13goto_convertt19get_string_constantERK5exprt + 184
5   cbmc                                0x00000001010fe700 _ZN13goto_convertt23do_function_call_symbolERK5exprtRK12symbol_exprtRKNSt3__16vectorIS0_NS6_9allocatorIS0_EEEER13goto_programtRK8dstringt + 5584
6   cbmc                                0x0000000101129458 _ZN13goto_convertt16do_function_callERK5exprtS2_RKNSt3__16vectorIS0_NS3_9allocatorIS0_EEEER13goto_programtRK8dstringt + 912
7   cbmc                                0x000000010112e594 _ZN13goto_convertt20remove_function_callER31side_effect_expr_function_calltRK8dstringtb + 1140
8   cbmc                                0x0000000101116394 _ZN13goto_convertt10clean_exprER5exprtRK8dstringtb + 4520
9   cbmc                                0x000000010111c6fc _ZN13goto_convertt18convert_expressionERK16code_expressiontR13goto_programtRK8dstringt + 604
10  cbmc                                0x0000000101119f80 _ZN13goto_convertt7convertERK5codetR13goto_programtRK8dstringt + 236
11  cbmc                                0x000000010111bdb4 _ZN13goto_convertt13convert_blockERK11code_blocktR13goto_programtRK8dstringt + 124
12  cbmc                                0x0000000101119f04 _ZN13goto_convertt7convertERK5codetR13goto_programtRK8dstringt + 112
13  cbmc                                0x0000000101119b90 _ZN13goto_convertt16goto_convert_recERK5codetR13goto_programtRK8dstringt + 48
14  cbmc                                0x000000010112a6d8 _ZN23goto_convert_functionst16convert_functionERK8dstringtR14goto_functiont + 1192
15  cbmc                                0x000000010112a1d8 _ZN23goto_convert_functionst12goto_convertER15goto_functionst + 316
16  cbmc                                0x000000010112b15c _Z12goto_convertR18symbol_table_basetR15goto_functionstR16message_handlert + 108
17  cbmc                                0x0000000101176dfc _Z21initialize_goto_modelRKNSt3__16vectorINS_12basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEENS4_IS6_EEEER16message_handlertRK8optionst + 548
18  cbmc                                0x0000000100f1ef84
 _ZN19cbmc_parse_optionst16get_goto_programER11goto_modeltRK8optionstRK8cmdlinetR19ui_message_handlert + 124
19  cbmc                                0x0000000100f1de00 _ZN19cbmc_parse_optionst4doitEv + 928
20  cbmc                                0x00000001013ff64c _ZN19parse_options_baset4mainEv + 180
21  cbmc                                0x0000000100f13e1c main + 48
22  dyld                                0x0000000196013154 start + 2476

Diagnostics:
<< EXTRA DIAGNOSTICS >>
source location: file /Users/lucad/git/sv-benchmarks/c/openbsd-6.2/if_etherip-unreach-call.i line 151 function openbsd_assert
symbol
  * type: pointer
      * #source_location:
        * file: /Users/lucad/git/sv-benchmarks/c/openbsd-6.2/if_etherip-unreach-call.i
        * line: 150
        * function: openbsd_assert
        * working_directory: /Users/lucad/git/sv-benchmarks/c/openbsd-6.2
      * width: 64
      0: signedbv
          * width: 8
          * #constant: 1
          * #c_type: char
  * #source_location:
    * file: /Users/lucad/git/sv-benchmarks/c/openbsd-6.2/if_etherip-unreach-call.i
    * line: 151
    * function: openbsd_assert
    * working_directory: /Users/lucad/git/sv-benchmarks/c/openbsd-6.2
  * identifier: openbsd_assert::cond
  * #lvalue: 1
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---