Invariant check failed: map_entry.literal_map.size() == width

[ligurio]

--- begin invariant violation report ---                                 
Invariant check failed                                                                                                                             
File: /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv_map.cpp:68 function: get_literals                                             
Condition: map_entry.literal_map.size() == width                                                                                                   
Reason: number of literals in the literal map shall equal the bitvector width                                                                      
Backtrace:      <see below backtrace>

CBMC version: 6.3.1 (cbmc-6.3.1-6-gbcda5a9316)
Operating system: Ubuntu 22.04 amd64
Exact command line resulting in the issue: cbmc --verbosity 10 --bounds-check --memory-leak-check --memory-cleanup-check --pointer-check --signed-overflow-check --unsigned-overflow-check --nan-check --float-overflow-check --unwind 5 --object-bits 10 --trace proofs/vy_cache.proof
What behaviour did you expect: verification finished without crashes
What happened instead: crash

#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  0x000055555569bedb in invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&> (file="/home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv_map.cpp", function="get_literals", line=line@entry=68, 
    condition="map_entry.literal_map.size() == width") at /home/sergeyb/sources/cache/cbmc/src/util/invariant.h:260
#6  0x0000555555d5fbc6 in invariant_violated_string (reason="number of literals in the literal map shall equal the bitvector width", 
    condition="map_entry.literal_map.size() == width", line=68, function="get_literals", 
    file="/home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv_map.cpp") at /home/sergeyb/sources/cache/cbmc/src/util/invariant.h:282
#7  boolbv_mapt::get_literals (this=this@entry=0x55555728eef0, identifier=..., type=..., width=width@entry=0)
    at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv_map.cpp:68
#8  0x0000555555d57e09 in boolbvt::convert_index (this=this@entry=0x55555728e870, expr=...)
    at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv_index.cpp:74
#9  0x0000555555c858be in bv_pointerst::convert_pointer_type (this=0x55555728e870, expr=...)
    at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/bv_pointers.cpp:419
#10 0x0000555555c87624 in bv_pointerst::convert_bitvector (this=0x55555728e870, expr=...)
    at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/bv_pointers.cpp:624
#11 0x0000555555d39542 in boolbvt::convert_bv (this=0x55555728e870, expr=..., expected_width=std::optional<unsigned long> [no contained value])
    at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv.cpp:59
#12 0x0000555555d353f4 in boolbvt::boolbv_set_equality_to_true (expr=..., this=0x55555728e870)
    at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv.cpp:505
#13 boolbvt::boolbv_set_equality_to_true (this=0x55555728e870, expr=...) at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv.cpp:490
#14 0x0000555555d354ce in boolbvt::set_to (this=0x55555728e870, expr=..., value=<optimized out>)
    at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv.cpp:526
#15 0x00005555559dcc0a in symex_target_equationt::convert_assignments (this=0x55555728d930, decision_procedure=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_target_equation.cpp:374
#16 0x00005555559e3923 in symex_target_equationt::convert_without_assertions (this=0x55555728d930, decision_procedure=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_target_equation.cpp:338
#17 0x00005555559e39c5 in symex_target_equationt::convert (this=0x55555728d930, decision_procedure=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_target_equation.cpp:351
#18 0x00005555557d0126 in convert_symex_target_equation (equation=..., decision_procedure=..., message_handler=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/bmc_util.cpp:158
#19 0x00005555557d03c1 in prepare_property_decider (properties=std::map with 2977 elements = {...}, equation=..., property_decider=..., 
    ui_message_handler=...) at /home/sergeyb/sources/cache/cbmc/src/goto-checker/bmc_util.cpp:372
#20 0x00005555557de4db in multi_path_symex_checkert::prepare_property_decider (properties=std::map with 2977 elements = {...}, 
    this=0x55555728d6a0) at /home/sergeyb/sources/cache/cbmc/src/goto-checker/multi_path_symex_checker.cpp:82
#21 multi_path_symex_checkert::operator() (this=this@entry=0x55555728d6a0, properties=std::map with 2977 elements = {...})
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/multi_path_symex_checker.cpp:69
#22 0x00005555556a6438 in all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator() (this=0x55555728d4b0)
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/all_properties_verifier_with_trace_storage.h:45
#23 0x00005555556a29e3 in cbmc_parse_optionst::doit (this=0x7fffffffd780) at /home/sergeyb/sources/cache/cbmc/src/cbmc/cbmc_parse_options.cpp:776
#24 0x000055555569996f in parse_options_baset::main (this=this@entry=0x7fffffffd780)
    at /home/sergeyb/sources/cache/cbmc/src/util/parse_options.cpp:97
#25 0x0000555555687709 in main (argc=<optimized out>, argv=<optimized out>) at /home/sergeyb/sources/cache/cbmc/src/cbmc/cbmc_main.cpp:48

GOTO binary: vy_cache_goto.zip