./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-vhost-vhost_net.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-vhost-vhost_net.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-vhost-vhost_net.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
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:5232:3-5238:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6092:3-6099:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6112:3-6119:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6200:3-6206:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6260:3-6266:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6366:7-6379:7 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6403:3-6433:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6458:5-6465:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6558:5-6612:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6637:7-6644:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6669:7-6676:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6706:3-6731:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6738:3-6750:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6762:3-6777:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6793:3-6799:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6814:5-6821:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:6847:5-6853:5 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:7016:3-7066:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:7088:3-7111:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:7205:3-7245:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:7258:3-7282:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:7385:3-7408:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:7442:3-7465:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:7586:3-7609:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8258:7-8285:7 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8374:7-8386:7 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8423:3-8438:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8463:3-8493:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8502:3-8508:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8533:3-8555:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8574:3-8607:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8660:3-8683:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8697:3-8734:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8832:7-8845:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8872:7-8885:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8920:7-8933:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:8969:9-8982:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9016:9-9029:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9055:9-9068:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9095:9-9108:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9146:11-9159:11 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9271:3-9430:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9448:7-9461:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9488:7-9501:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9525:3-9684:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9702:7-9715:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9741:7-9754:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9795:9-9808:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9840:9-9853:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9882:9-9895:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9923:11-9936:11 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:9966:9-9979:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10017:11-10030:11 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10064:3-10094:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10130:3-10260:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10269:7-10281:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10300:3-10434:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10443:7-10455:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10475:3-10609:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10618:7-10630:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10708:7-10720:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10840:7-10852:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:10937:5-11096:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11106:9-11118:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11198:7-11210:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11358:9-11371:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11438:9-11451:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11496:3-11655:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11666:7-11679:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11768:9-11781:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11834:3-11847:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11859:3-11878:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11891:3-11904:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11916:3-11935:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:11980:3-11988:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12033:3-12059:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12076:3-12100:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12193:3-12208:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12298:9-12311:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12340:9-12354:9 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12386:7-12399:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12440:5-12447:5 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12543:9-12556:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12683:3-12698:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12810:7-12823:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12846:11-12859:11 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:12893:11-12905:11 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:13080:3-13103:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:13135:3-13158:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:13422:3-13445:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:13562:3-13575:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:13823:3-13890:3 with factor 2
[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][Imprecise][Unsound] Function definition missing for __xchg_wrong_size
[Error][Imprecise][Unsound] Function definition missing for __get_user_bad
[Error][Imprecise][Unsound] Function definition missing for __put_user_bad
[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-vhost-vhost_net.ko.cil.out.yml/witness.yml: No such file or directory")
