Crash when running with CBMC's SMT solver option #1748
Description
I tried this code:
#[kani::proof]
fn main() {
let x: i32 = kani::any();
let y = x;
assert!(x == y);
}using the following command line invocation:
kani test.rs --enable-unstable --cbmc-args --z3
with Kani version: 07092de
I expected to see this happen: Verification succeeded
Instead, this happened:
$ kani test.rs --enable-unstable --cbmc-args --z3
file /home/ubuntu/git/kani/library/kani/src/arbitrary.rs line 21 column 26 function <i32 as kani::Arbitrary>::any: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/git/kani/library/kani/src/lib.rs line 85 column 5 function kani::any::<i32>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 342 column 42 function std::fmt::ArgumentV1::new_display::<std::fmt::Arguments>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 342 column 68 function std::fmt::ArgumentV1::new_display::<std::fmt::Arguments>: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/macros/mod.rs line 709 column 47 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/macros/mod.rs line 709 column 47 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panic.rs line 57 column 38 function kani::any_raw_inner::<i32>: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 395 column 12 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 395 column 12 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 395 column 12 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 395 column 12 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb3'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 395 column 12 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb6'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 395 column 12 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb4'
file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panic.rs line 57 column 38 function std::fmt::Arguments::new_v1: adding goto-destructor code on jump to 'bb5'
file /home/ubuntu/examples/trivial/test.rs line 3 column 18 function main: adding goto-destructor code on jump to 'bb1'
file /home/ubuntu/examples/trivial/test.rs line 5 column 5 function main: adding goto-destructor code on jump to 'bb2'
file /home/ubuntu/git/kani/library/kani/src/lib.rs line 108 column 5 function kani::any_raw_internal::<i32, 4>: adding goto-destructor code on jump to 'bb1'
Checking harness main...
CBMC 5.67.0 (cbmc-5.67.0)
CBMC version 5.67.0 (cbmc-5.67.0) 64-bit x86_64 linux
Reading GOTO program from file test.for-main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.0073559s
size of program expression: 492 steps
slicing removed 283 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 4.6592e-05s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Runtime Convert SSA: 0.000348786s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.11375s
Runtime decision procedure: 0.114173s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.0168971s
Runtime decision procedure: 0.0169387s
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/json_goto_trace.cpp:121 function: convert_decl
Condition: step.full_lhs_value.is_not_nil()
Reason: full_lhs_value in assignment must not be nil
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x5564ec6b0da0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x5564ec6b1349]
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) [0x5564ebe14738]
cbmc(convert_decl(json_objectt&, conversion_dependenciest const&, trace_optionst const&)+0x3aa6) [0x5564ec2b0116]
cbmc(void convert<json_stream_arrayt>(namespacet const&, goto_tracet const&, json_stream_arrayt&, trace_optionst)+0x5c2) [0x5564ebf6a382]
cbmc(output_properties_with_traces(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > > const&, goto_trace_storaget const&, trace_optionst const&, unsigned long, ui_message_handlert&)+0xbec) [0x5564ebf843dc]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::report()+0x94) [0x5564ebe1bac4]
cbmc(cbmc_parse_optionst::doit()+0xf9a) [0x5564ebe1af9a]
cbmc(parse_options_baset::main()+0x8f) [0x5564ebe1284f]
cbmc(main+0x39) [0x5564ebdfe859]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f60311e80b3]
cbmc(_start+0x2e) [0x5564ebe1414e]
--- end invariant violation report ---
Verification Time: 1.3128812s