kani: CBMC invariant violation in precondition (exit code 134)

Mirror issue for https://github.com/diffblue/cbmc/issues/7288 , will update this description with a reproducer once the author of the original issue gets back to us. The error is this one:

Unwinding loop _RNvNvMNtNtCs6ksVFr7TWxF_4core5alloc6layoutNtB4_6Layout5array5innerCs8UtVQrhG5Gl_7ask_cli.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs line 438 column 16 function std::alloc::Layout::array::inner thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 105 column 9 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1536 column 32 function std::result::Result::<std::alloc::Layout, std::alloc::LayoutError>::unwrap_unchecked thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1533 column 15 function std::result::Result::<std::alloc::Layout, std::alloc::LayoutError>::unwrap_unchecked thread 0
Unwinding loop _ZN4core6result19Result$LT$T$C$E$GT$16unwrap_unchecked17hf3f4fa8b2792210eE.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1538 column 5 function std::result::Result::<std::alloc::Layout, std::alloc::LayoutError>::unwrap_unchecked thread 0
Unwinding loop _ZN4core3ptr46drop_in_place$LT$alloc..vec..Vec$LT$u8$GT$$GT$17h42d65b399ad5abe9E.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs line 491 column 1 function std::ptr::drop_in_place::<std::vec::Vec<u8>> thread 0
Not unwinding loop _RINvCs8UtVQrhG5Gl_7ask_cli3askReRShNtNtNtCsb5NFf2JfBbd_3std2io4util4SinkEB2_.11 iteration 10 file /home/asaveau/IdeaProjects/ask-cli/src/lib.rs line 122 column 5 function ask::<&str, &[u8], std::io::Sink> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mut_ptr.rs line 38 column 15 function std::ptr::mut_ptr::<impl *mut u8>::is_null thread 0
Unwinding loop _RNvNvMNtNtCs6ksVFr7TWxF_4core5alloc6layoutNtB4_6Layout5array5innerCs8UtVQrhG5Gl_7ask_cli.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs line 438 column 16 function std::alloc::Layout::array::inner thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 105 column 9 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1536 column 32 function std::result::Result::<std::alloc::Layout, std::alloc::LayoutError>::unwrap_unchecked thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1533 column 15 function std::result::Result::<std::alloc::Layout, std::alloc::LayoutError>::unwrap_unchecked thread 0
Unwinding loop _ZN4core6result19Result$LT$T$C$E$GT$16unwrap_unchecked17hf3f4fa8b2792210eE.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 1538 column 5 function std::result::Result::<std::alloc::Layout, std::alloc::LayoutError>::unwrap_unchecked thread 0
Unwinding loop _ZN4core3ptr46drop_in_place$LT$alloc..vec..Vec$LT$u8$GT$$GT$17h42d65b399ad5abe9E.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2022-10-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs line 491 column 1 function std::ptr::drop_in_place::<std::vec::Vec<u8>> thread 0
Runtime Symex: 41.282s
size of program expression: 476615 steps
slicing removed 348050 assignments
Generated 25977 VCC(s), 12350 remaining after simplification
Runtime Postprocess Equation: 0.941078s
--- begin invariant violation report ---
Invariant check failed
File: ../src/util/bitvector_types.h:42 function: to_bitvector_type
Condition: can_cast_type<bitvector_typet>(type)
Reason: Precondition
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x4e) [0x55faafc8115e]
cbmc(get_backtrace[abi:cxx11]()+0x16a) [0x55faafc820ea]
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&)+0x4f) [0x55faaf3ce7ff]
cbmc(lower_byte_extract(byte_extract_exprt const&, namespacet const&)+0x29c9) [0x55faafa33ee9]
cbmc(lower_byte_operators(exprt const&, namespacet const&)+0x150) [0x55faafa3c310]
cbmc(lower_byte_operators(exprt const&, namespacet const&)+0x8b) [0x55faafa3c24b]
cbmc(lower_byte_operators(exprt const&, namespacet const&)+0x8b) [0x55faafa3c24b]
cbmc(boolbvt::convert_equality(equal_exprt const&)+0x189) [0x55faaf9d7fb9]
cbmc(boolbvt::convert_rest(exprt const&)+0x20e) [0x55faaf9c256e]
cbmc(bv_pointerst::convert_rest(exprt const&)+0xab) [0x55faafa0c1bb]
cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x5aa) [0x55faafa4fd6a]
cbmc(prop_conv_solvert::convert(exprt const&)+0x13f) [0x55faafa52e4f]
cbmc(prop_conv_solvert::add_constraints_to_prop(exprt const&, bool)+0x16d) [0x55faafa4d94d]
cbmc(prop_conv_solvert::set_to(exprt const&, bool)+0x912) [0x55faafa510c2]
cbmc(boolbvt::set_to(exprt const&, bool)+0x64) [0x55faaf9c0c84]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0xd1) [0x55faaf715051]
cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0xd7) [0x55faaf71cad7]
cbmc(symex_target_equationt::convert(decision_proceduret&)+0x21) [0x55faaf71d821]
cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x3de) [0x55faaf50d47e]
cbmc(prepare_property_decider(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&, symex_target_equationt&, goto_symex_property_decidert&, ui_message_handlert&)+0x466) [0x55faaf50db46]
cbmc(multi_path_symex_checkert::operator()(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x16c) [0x55faaf52847c]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x70) [0x55faaf3d7000]
cbmc(cbmc_parse_optionst::doit()+0x1118) [0x55faaf3d4bf8]
cbmc(parse_options_baset::main()+0xa8) [0x55faaf3cc848]
cbmc(main+0x34) [0x55faaf3b8984]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7fdf48429d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7fdf48429e40]
cbmc(_start+0x2a) [0x55faaf3ce43a]


--- end invariant violation report ---
Passing problem to propositional reduction

CBMC failed with status 134
VERIFICATION:- FAILED