Invariant violation with `--cover assertions --pointer-check`

[zhassan-aws]

CBMC version: 5.46.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc --cover assertions --pointer-check vec.goto
What behaviour did you expect: Verification Successful
What happened instead: Invariant violation

The attached goto file is generated by running RMC on the following Rust program:

fn main() {
    let mut v = Vec::<i32>::new();
    v.push(1);
    assert!(v.len() == 1);
}

using rmc vec.rs --keep-temps.

$ cbmc --cover assertions --pointer-check  vec.goto 
CBMC version 5.46.0 (cbmc-5.46.0) 64-bit x86_64 linux
Reading GOTO program from file
Reading: vec.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Rewriting existing assertions as assumptions
Ignoring block 5 location 16 main (missing source location)
Ignoring block 7 location 19 main (missing source location)
Ignoring block 8 location 20 main (missing source location)
Ignoring block 2 location 54 _RNvXs8_NtCs8oL8HdYXHwV_5alloc11collectionsNtB5_19TryReserveErrorKindNtNtCs61cxoXOqFbB_4core5clone5Clone5cloneCs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 5 location 108 _RNvNtCs8oL8HdYXHwV_5alloc5alloc7reallocCs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 2 location 231 _RINvMNtCs61cxoXOqFbB_4core6optionINtB3_6OptionINtNtNtB5_3ptr8non_null7NonNullhEE5ok_orNtNtB5_5alloc10AllocErrorECs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 7 location 255 _RINvMNtCs61cxoXOqFbB_4core6optionINtB3_6OptionINtNtNtB5_3ptr8non_null7NonNullhEE5ok_orNtNtB5_5alloc10AllocErrorECs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 8 location 256 _RINvMNtCs61cxoXOqFbB_4core6optionINtB3_6OptionINtNtNtB5_3ptr8non_null7NonNullhEE5ok_orNtNtB5_5alloc10AllocErrorECs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 9 location 257 _RINvMNtCs61cxoXOqFbB_4core6optionINtB3_6OptionINtNtNtB5_3ptr8non_null7NonNullhEE5ok_orNtNtB5_5alloc10AllocErrorECs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 10 location 258 _RINvMNtCs61cxoXOqFbB_4core6optionINtB3_6OptionINtNtNtB5_3ptr8non_null7NonNullhEE5ok_orNtNtB5_5alloc10AllocErrorECs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 11 location 265 _RINvMNtCs61cxoXOqFbB_4core6optionINtB3_6OptionINtNtNtB5_3ptr8non_null7NonNullhEE5ok_orNtNtB5_5alloc10AllocErrorECs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 5 location 280 _RNvNtCs8oL8HdYXHwV_5alloc5alloc5allocCs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 2 location 319 _RNvXsy_NtCs61cxoXOqFbB_4core6resultINtB5_6ResultNtNtNtB7_5alloc6layout6LayoutNtNtCs8oL8HdYXHwV_5alloc11collections19TryReserveErrorKindENtNtNtB7_3ops9try_trait3Try6branchCs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 1 location 373 vec.6635f0d8::vec::global::0::_init (missing source location)
Ignoring block 4 location 544 _RINvNtCs8oL8HdYXHwV_5alloc7raw_vec11finish_growNtNtB4_5alloc6GlobalECs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 12 location 565 _RINvNtCs8oL8HdYXHwV_5alloc7raw_vec11finish_growNtNtB4_5alloc6GlobalECs7qQnkpzyyQS_3vec (missing source location)
Ignoring block 2 location 669 _RINvNtCs61cxoXOqFbB_4core3ptr13drop_in_placeINtNtCs8oL8HdYXHwV_5alloc7raw_vec6RawVeclEECs7qQnkpzyyQS_3vec (missing source location)
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-instrument/cover_basic_blocks.cpp:189 function: update_source_lines
Condition: !str.empty()
Reason: source lines set must not be empty
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x55f16e8125e0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x55f16e812b89]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x48) [0x55f16e0b0558]
cbmc(cover_basic_blockst::update_source_lines(cover_basic_blockst::block_infot&)+0x1d1) [0x55f16e12a551]
cbmc(cover_basic_blockst::cover_basic_blockst(goto_programt const&)+0x250) [0x55f16e12b810]
cbmc(+0x31ad39) [0x55f16e113d39]
cbmc(instrument_cover_goals(cover_configt const&, symbol_tablet const&, goto_functionst&, message_handlert&)+0x4de) [0x55f16e1146ce]
cbmc(cbmc_parse_optionst::process_goto_program(goto_modelt&, optionst const&, messaget&)+0x273) [0x55f16e0b1ce3]
cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0x5df) [0x55f16e0b26df]
cbmc(cbmc_parse_optionst::doit()+0x58f) [0x55f16e0b6fff]
cbmc(parse_options_baset::main()+0x8f) [0x55f16e0ae66f]
cbmc(main+0x39) [0x55f16e09cfa9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f4fcc7730b3]
cbmc(_start+0x2e) [0x55f16e0aff6e]


--- end invariant violation report ---
Aborted (core dumped)

vec.tar.gz