Repository navigation
Using z3 with symbolic boolean array crashes CBMC #2002
Description
I tried this code:
#[kani::proof]
fn main() {
let _arr: [bool; 1] = kani::any();
}using the following command line invocation:
kani test1.rs --enable-unstable --cbmc-args --z3
with Kani version: 438e582
I expected to see this happen: Verification successful
Instead, this happened: CBMC crashed:
Runtime Symex: 0.114774s
size of program expression: 4174 steps
slicing removed 2993 assignments
Generated 298 VCC(s), 48 remaining after simplification
Runtime Postprocess Equation: 0.0009437s
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2/smt2_conv.cpp:5643 function: convert_type
Condition: Check return value
Reason: to_union_type(ns.follow(type)).components().empty() || width != 0
Backtrace:
cbmc(+0xa98040) [0x55e09d4f4040]
cbmc(+0xa985e9) [0x55e09d4f45e9]
cbmc(+0x225a74) [0x55e09cc81a74]
cbmc(+0x8b6066) [0x55e09d312066]
cbmc(+0x8908b7) [0x55e09d2ec8b7]
cbmc(+0x890782) [0x55e09d2ec782]
cbmc(+0x8b03e7) [0x55e09d30c3e7]
cbmc(+0x8b0cad) [0x55e09d30ccad]
cbmc(+0x8b02a6) [0x55e09d30c2a6]
cbmc(+0x8b0cad) [0x55e09d30ccad]
cbmc(+0x8b0b6f) [0x55e09d30cb6f]
cbmc(+0x8b0d57) [0x55e09d30cd57]
cbmc(+0x8b0c24) [0x55e09d30cc24]
cbmc(+0x8b0fdf) [0x55e09d30cfdf]
cbmc(+0x8ad5a8) [0x55e09d3095a8]
cbmc(+0x8ad5e3) [0x55e09d3095e3]
cbmc(+0x8ad5e3) [0x55e09d3095e3]
cbmc(+0x8affd8) [0x55e09d30bfd8]
cbmc(+0x8b1cda) [0x55e09d30dcda]
cbmc(+0x5508f1) [0x55e09cfac8f1]
cbmc(+0x5590a6) [0x55e09cfb50a6]
cbmc(+0x559c52) [0x55e09cfb5c52]
cbmc(+0x348d84) [0x55e09cda4d84]
cbmc(+0x349205) [0x55e09cda5205]
cbmc(+0x35ac95) [0x55e09cdb6c95]
cbmc(+0x201189) [0x55e09cc5d189]
cbmc(+0x1fd6ae) [0x55e09cc596ae]
cbmc(+0x1f4e9f) [0x55e09cc50e9f]
cbmc(+0x1e0ec9) [0x55e09cc3cec9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f9e98c530b3]
cbmc(+0x1f681e) [0x55e09cc5281e]
Diagnostics:
<< EXTRA DIAGNOSTICS >>
failed to get width of union
<< END EXTRA DIAGNOSTICS >>
--- end invariant violation report ---
Passing problem to SMT2 QF_AUFBV using Z3
Activity
rahulku commentedon Dec 15, 2022
cbmc issue?
zhassan-aws commentedon Dec 15, 2022
I'm trying to reproduce it on a C program (similar to what I did for diffblue/cbmc#7308), to make debugging easier. So far, I haven't been successful.
zhassan-aws commentedon Dec 15, 2022
Created diffblue/cbmc#7442 with the goto binary for the time being.
[-]Using z3 with symbolic boolear array crashes CBMC[/-][+]Using z3 with symbolic boolean array crashes CBMC[/+]Update CBMC version to 5.79.0