CBMC aborted abnormally in field_sensitivityt::get_fields

[ligurio]

/home/sergeyb/sources/cache/cbmc/build/bin/cbmc(+0x147305) [0x55555569b305]

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
constant
  * type: c_enum_tag
      * identifier: tag-bps_tree_test_max_sizes
  * #source_location: 
    * file: /home/sergeyb/sources/MRG/tarantool/src/lib/salad/bps_tree.h
    * line: 5834
    * function: bps_tree_test_insert
  * value: 10
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---

Program received signal SIGABRT, Aborted.

CBMC version: 6.3.1 (cbmc-6.3.1-6-gbcda5a9316)
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: /home/sergeyb/sources/cache/cbmc/build/bin/cbmc --bounds-check --memory-leak-check --memory-cleanup-check --pointer-check --signed-overflow-check --unsigned-overflow-check --nan-check --float-overflow-check --unwind 1 --verbosity 10 proofs/bps_tree_iterator.proof
What behaviour did you expect: model checking finished successfully
What happened instead: SIGABORT

Backtrace:

#0  __pthread_kill_implementation (no_tid=0, signo=6, threadid=140737352644416) at ./nptl/pthread_kill.c:44
#1  __pthread_kill_internal (signo=6, threadid=140737352644416) at ./nptl/pthread_kill.c:78
#2  __GI___pthread_kill (threadid=140737352644416, signo=signo@entry=6) at ./nptl/pthread_kill.c:89
#3  0x00007ffff7842476 in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#4  0x00007ffff78287f3 in __GI_abort () at ./stdlib/abort.c:79
#5  0x00005555556c66cc in invariant_violated_structured<invariant_with_diagnostics_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > (
    file="/home/sergeyb/sources/cache/cbmc/src/util/arith_tools.h", function="numeric_cast_v", line=line@entry=151, 
    condition="expression should be convertible to target integral type") at /home/sergeyb/sources/cache/cbmc/src/util/invariant.h:260
#6  0x00005555557150d9 in report_invariant_failure<irep_pretty_diagnosticst> (condition="maybe", 
    reason="expression should be convertible to target integral type", line=151, function="numeric_cast_v", 
    file="/home/sergeyb/sources/cache/cbmc/src/util/arith_tools.h") at /home/sergeyb/sources/cache/cbmc/src/util/invariant.h:379
#7  numeric_cast_v<BigInt> (arg=...) at /home/sergeyb/sources/cache/cbmc/src/util/arith_tools.h:151
#8  0x00005555559e7415 in field_sensitivityt::get_fields (this=this@entry=0x555558123f98, ns=..., state=..., ssa_expr=..., 
    disjoined_fields_only=disjoined_fields_only@entry=false) at /home/sergeyb/sources/cache/cbmc/src/util/std_expr.h:3049
#9  0x0000555555939814 in goto_symex_statet::declare (this=this@entry=0x555558123e40, ssa=..., ns=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/goto_symex_state.cpp:872
#10 0x00005555559ad977 in goto_symext::symex_decl (this=0x55555c7d8ff0, state=..., expr=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_decl.cpp:39
#11 0x00005555559ce488 in goto_symext::execute_next_instruction(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&)
    (this=0x55555c7d8ff0, get_goto_function=..., state=...) at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_main.cpp:690
#12 0x00005555559d0588 in goto_symext::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&) (
    this=this@entry=0x55555c7d8ff0, get_goto_function=..., state=...) at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_main.cpp:597
#13 0x00005555557fcbc8 in symex_bmct::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&) (
    this=0x55555c7d8ff0, get_goto_function=..., state=...) at /home/sergeyb/sources/cache/cbmc/src/goto-checker/symex_bmc.cpp:75
#14 0x00005555559d06e8 in goto_symext::symex_threaded_step(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&) (
    this=0x55555c7d8ff0, state=..., get_goto_function=...) at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_main.cpp:302
#15 0x00005555559d0857 in goto_symext::symex_with_state(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&) (
    this=0x55555c7d8ff0, state=..., get_goto_function=...) at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_main.cpp:368
#16 0x00005555559cfe7b in goto_symext::symex_from_entry_point_of(std::function<goto_functiont const& (dstringt const&)> const&, shadow_memory_field_definitionst const&) (this=this@entry=0x55555c7d8ff0, get_goto_function=..., fields=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_main.cpp:472
#17 0x00005555557dfb81 in multi_path_symex_only_checkert::generate_equation (this=0x55555c7d8960)
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/multi_path_symex_only_checker.cpp:82
#18 0x00005555557de39f in multi_path_symex_checkert::operator() (this=this@entry=0x55555c7d8960, properties=std::map with 17719 elements = {...})
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/multi_path_symex_checker.cpp:55
#19 0x00005555556a6438 in all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator() (this=0x55555c7d8770)
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/all_properties_verifier_with_trace_storage.h:45
#20 0x00005555556a29e3 in cbmc_parse_optionst::doit (this=0x7fffffffd7a0) at /home/sergeyb/sources/cache/cbmc/src/cbmc/cbmc_parse_options.cpp:776
#21 0x000055555569996f in parse_options_baset::main (this=this@entry=0x7fffffffd7a0)
    at /home/sergeyb/sources/cache/cbmc/src/util/parse_options.cpp:97
#22 0x0000555555687709 in main (argc=<optimized out>, argv=<optimized out>) at /home/sergeyb/sources/cache/cbmc/src/cbmc/cbmc_main.cpp:48

(I'll provide source code a bit later.)

[tautschnig]

It seems that this involves the source code from https://github.com/tarantool/tarantool/blob/master/src/lib/salad/bps_tree.h and, specifically, an array the size of which is given by an enum value. This ought to work fine as long as the underlying type that is used to represent the enum values is a signed or unsigned integral type, which I believe to be the case here. So, yes, please do provide either the source code or a goto binary to permit debugging. Thank you!

[ligurio]

Reduced test source (still require salad) with GOTO binary in attached archive gh-8479.zip