Closed
Description
On the following C program, which is a minimized version of the program from model-checking/kani#1748:
#include <assert.h>
struct Unit
{
};
int main() {
struct Unit var_0;
int x;
int y = x;
assert(y == x);
return 0;
}Running CBMC with the --z3 option causes an invariant violation:
$ cbmc --version
5.67.0 (cbmc-5.67.0)
$ z3 --version
Z3 version 4.11.2 - 64 bit
$ cbmc test.c --z3
CBMC version 5.67.0 (cbmc-5.67.0) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000595497s
size of program expression: 40 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.326e-05s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2/smt2_conv.cpp:3032 function: convert_struct
Condition: !components.empty()
Reason: struct shall have struct components
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x55efb6b3bda0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x55efb6b3c349]
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) [0x55efb629f738]
cbmc(smt2_convt::convert_struct(struct_exprt const&)+0x43e) [0x55efb69560ee]
cbmc(smt2_convt::convert_expr(exprt const&)+0x755) [0x55efb6943c35]
cbmc(smt2_convt::convert_expr(exprt const&)+0x1139) [0x55efb6944619]
cbmc(smt2_convt::convert(exprt const&)+0x53f) [0x55efb695a86f]
cbmc(smt2_convt::handle(exprt const&)+0xa3) [0x55efb695aa83]
cbmc(symex_target_equationt::convert_decls(decision_proceduret&)+0xed) [0x55efb65f2a6d]
cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0xe1) [0x55efb65f7791]
cbmc(symex_target_equationt::convert(decision_proceduret&)+0x42) [0x55efb65f8332]
cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x334) [0x55efb63ef214]
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&)+0x3c5) [0x55efb63ef695]
cbmc(multi_path_symex_checkert::operator()(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x155) [0x55efb6400ec5]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x89) [0x55efb62a9a29]
cbmc(cbmc_parse_optionst::doit()+0xf8e) [0x55efb62a5f8e]
cbmc(parse_options_baset::main()+0x8f) [0x55efb629d84f]
cbmc(main+0x39) [0x55efb6289859]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7ffaa63d20b3]
cbmc(_start+0x2e) [0x55efb629f14e]
--- end invariant violation report ---
Aborted (core dumped)
CBMC version: 5.67.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc test.c --z3
What behaviour did you expect: Verification successful
What happened instead: Invariant violation