./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4239: Warning: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4239: CIL only supports attribute((alias)) for functions.

[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:3937:3-3943:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4121:5-4131:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4173:3-4191:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4391:3-4401:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4433:3-4458:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4467:3-4483:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4488:3-4511:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4520:3-4550:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4712:7-4719:7 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4729:5-4735:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4756:9-4760:9 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4893:3-4899:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4905:3-4911:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:4950:5-4991:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5030:3-5040:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5065:5-5082:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5089:5-5106:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5126:3-5136:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5195:3-5205:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5227:3-5237:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5250:3-5268:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5275:3-5286:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5293:3-5311:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5350:3-5360:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5366:5-5376:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5394:7-5401:7 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5451:9-5458:9 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5479:9-5486:9 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5523:3-5533:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5541:5-5548:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5559:3-5567:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5576:3-5586:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5606:3-5616:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5645:3-5655:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5692:3-5702:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5778:3-5788:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5796:5-5803:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5814:3-5824:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5832:3-5842:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5860:3-5870:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5894:3-5904:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5928:3-5938:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5944:5-5954:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5978:3-5988:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:5998:5-6008:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6017:5-6027:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6059:5-6069:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6084:5-6094:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6105:5-6115:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6140:3-6150:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6172:5-6182:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6229:3-6239:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6261:5-6271:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6304:3-6314:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6334:5-6344:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6365:7-6381:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6404:5-6414:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6424:5-6434:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6444:5-6454:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6554:3-6564:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6585:3-6595:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6605:3-6615:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6625:3-6655:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6665:3-6675:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6682:3-6692:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6700:3-6710:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6878:5-6885:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6917:9-6924:9 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6957:11-6964:11 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6989:7-6996:7 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:7027:3-7040:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:7084:5-7091:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:7147:9-7154:9 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:7173:7-7180:7 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:7682:3-7695:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:7707:3-7726:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:7739:3-7752:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:7764:3-7783:3 with factor 8
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Imprecise][Unsound] Function definition missing for __bad_percpu_size
[Error][Analyzer] About to crash!

Fatal error: exception Failure("Yaml_unix.of_file: /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.yml/witness.yml: No such file or directory")
