/home/leostrakosch/Documents/SV/sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i violation_witness C klee CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) /home/leostrakosch/Documents/SV/sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i dee4f98e3deb83265bbf70c3b5c0f3c1ff37b06c 32bit true \result == 1; __VERIFIER_nondet_uint true 5 \result == 0; __VERIFIER_nondet_uint