./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-scsi-dc395x.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-scsi-dc395x.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-scsi-dc395x.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-scsi-dc395x.ko.cil.out.i:12427: Warning: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:12427: 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-scsi-dc395x.ko.cil.out.i:4689:3-4720:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:4798:3-4829:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:4877:3-4908:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:4992:3-4998:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:5217:3-5255:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:5286:3-5324:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:5353:3-5391:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:5420:3-5458:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:5888:5-5896:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:5920:3-5934:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:5964:3-5975:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6011:3-6026:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6040:3-6048:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6077:3-6093:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6101:5-6111:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6139:3-6151:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6276:3-6292:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6319:3-6335:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6388:3-6394:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6456:3-6469:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6481:3-6522:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6547:5-6554:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6664:3-6694:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6731:5-6746:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:6882:5-6889:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:7057:3-7078:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:7439:7-7451:7 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:7498:5-7510:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:7577:5-7584:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:7782:3-7794:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:7847:5-7858:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:7912:3-7932:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8264:13-8270:13 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8291:11-8314:11 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8363:15-8369:15 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8381:15-8387:15 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8569:11-8575:11 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8595:9-8609:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8624:13-8630:13 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8642:13-8648:13 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:8860:3-8873:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:9005:3-9018:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:9489:3-9504:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10144:7-10150:7 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10218:9-10224:9 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10236:9-10242:9 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10323:5-10350:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10376:5-10401:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10445:3-10454:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10654:5-10666:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10737:3-10753:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10808:3-10820:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10875:3-10884:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10901:3-10920:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10926:3-10945:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:10970:3-10989:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11002:3-11015:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11045:3-11056:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11085:3-11106:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11133:3-11144:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11176:3-11185:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11206:5-11215:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11227:5-11236:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11250:5-11259:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11303:3-11313:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11344:3-11352:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11394:5-11409:5 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11539:3-11545:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11550:3-11556:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11579:3-11587:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11594:3-11604:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11796:5-11803:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:11941:5-11948:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:12157:5-12169:5 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:12188:5-12200:5 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:12573:3-12685:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:12731:3-12744:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:12756:3-12775:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:12788:3-12801:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko.cil.out.i:12813:3-12832: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][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-scsi-dc395x.ko.cil.out.yml/witness.yml: No such file or directory")
