Core dumping while generating SMT2 formulation

[mm95]

Hi,
I ran cbmc with fmt.c from coreutils-8.23 with --smt2 and --outfile option but received 'core dumped' message with below log.
cbmc: smt2/smt2_conv.cpp:2284: void smt2_convt::convert_typecast(const typecast_exprt&): Assertion `boolbv_width(src_type)==boolbv_width(dest_type)' failed.

before running , I updated cbmc with last commit (a44b420...).
I simplify fmt.c in two version, and get different log error with them.
Sorry if the programs may be complex yet.
fmt_simplify1.c.txt
fmt_simplify2.c.txt

thanks so much,
Maryam.

[mgudemann]

hi @mm95 what is your exact command line ?
I downloaded coreutils 8.23, build it, copied your simplified files into src and executed there:

cbmc --smt2 --outfile fmt.simp1.smt fmt.simp1.c -I ../lib/ --unwind 5

giving

...
Unwinding loop flush_paragraph.5 iteration 4 (5 max) file fmt.simp1.c line 205 function flush_paragraph thread 0
Not unwinding loop flush_paragraph.5 iteration 5 (5 max) file fmt.simp1.c line 205 function flush_paragraph thread 0
Not unwinding loop get_line.0 iteration 5 (5 max) file fmt.simp1.c line 231 function get_line thread 0
Not unwinding loop fmt.0 iteration 5 (5 max) file fmt.simp1.c line 249 function fmt thread 0
size of program expression: 10088 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to SMT2
converting SSA
Unexpected case: TODO typecast2 array -> unsignedbv src == byte_extract_little_endian(invalid_object11#0, 0l, unsigned char [1l])

and

cbmc --smt2 --outfile fmt.simp2.smt fmt.simp2.c -I ../lib/ --unwind 5

giving

...
Not unwinding loop flush_paragraph.5 iteration 5 (5 max) file fmt.simp2.c line 205 function flush_paragraph thread 0
Not unwinding loop get_line.0 iteration 5 (5 max) file fmt.simp2.c line 231 function get_line thread 0
Not unwinding loop fmt.0 iteration 5 (5 max) file fmt.simp2.c line 249 function fmt thread 0
size of program expression: 8978 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to SMT2
converting SSA
cbmc: smt2/smt2_conv.cpp:2284: void smt2_convt::convert_typecast(const typecast_exprt&): Assertion `boolbv_width(src_type)==boolbv_width(dest_type)' failed.

Are these the same results as you have?

[mm95]

Hello,
I used the commands like you,

cbmc   --smt2   --outfile   smtf.smt2     -I /coreutils-8.23/lib/  -I/coreutils/src/   --unwind 2  

and got the result like your results too.

[mgudemann]

@mm95 thank you, the assertion violation was caused by a missing bitvector extension. The other error is a (still) missing TODO for a typecast. With the corrected bitvector extension we hit the same TODO with both your examples.

[mm95]

Thanks so much for your notice.

[NlightNFotis]

Hi.

I can see that the code triggering this issue is still there, but it's worth noting that we are currently working on a reworked SMT backend. It's still some way off achieving feature parity with the old one, but going forward it's going to become the default SMT backend once it becomes more feature rich.

So while this is a problem for now, we do not anticipate this exact issue is going to plague the new iteration of it.

[tautschnig]

I ran the above commands with current CBMC (5.69.1) and can no longer observe the issue with either of the two input files. Closing.