./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/elevator_spec2_product24.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/elevator_spec2_product24.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c


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


[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/product-lines/elevator_spec2_product24.cil.c:2205:5-2263:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2280:9-2338:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2702:3-2730:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2762:3-2805:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3105:3-3124:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3152:3-3171:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3255:3-3276:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3312:3-3337:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3397:5-3417:5 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())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:92:1-133:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:752:1-774:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:775:1-797:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:851:1-882:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:883:1-894:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1008:1-1016:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1017:1-1056:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1720:1-1733:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2002:1-2172:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2173:1-2194:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2195:1-2353:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2365:1-2373:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2559:1-2610:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2612:1-2622:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2623:1-2633:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2634:1-2644:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2645:1-2655:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2656:1-2666:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2678:1-2689:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2736:1-2813:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2814:1-2825:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2826:1-2837:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2838:1-2848:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2849:1-2865:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3044:1-3053:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3087:1-3129:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3130:1-3176:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3184:1-3229:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3230:1-3285:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3286:1-3345:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3348:1-3450:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3451:1-3496:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3497:1-3542:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3083-3083)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__2' has dead code:
  on line 2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2398-2398)
  on line 2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2401-2401)
  on line 2404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2404-2404)
  on lines 2409..2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2409-2410)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__3' has dead code:
  on line 2436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2436-2436)
  on line 2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2438-2438)
  on lines 2440..2441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2440-2441)
  on line 2453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2453-2453)
  on lines 2455..2456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2455-2456)
  on line 2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2466-2466)
  on line 2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2468-2468)
  on lines 2470..2471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2470-2471)
  on line 2481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2481-2481)
  on line 2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2483-2483)
  on lines 2485..2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2485-2486)
  on line 2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2496-2496)
  on line 2498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2498-2498)
  on lines 2500..2501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2500-2501)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__4' has dead code:
  on line 2524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2524-2524)
  on line 2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2529-2529)
  on line 2534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2534-2534)
  on line 2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2542-2542)
  on line 2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2544-2544)
  on line 2553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2553-2553)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 1070..1071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1070-1071)
  on lines 1074..1075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1074-1075)
  on lines 1085..1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1085-1086)
  on lines 1092..1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1092-1093)
  on lines 1096..1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1096-1097)
  on lines 1103..1104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1103-1104)
  on line 1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1111-1111)
  on lines 1113..1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1113-1115)
  on lines 1117..1119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1117-1119)
  on lines 1132..1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1132-1134)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:971-971)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 982..984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:982-984)
  on lines 986..988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:986-988)
  on lines 990..992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:990-992)
  on lines 994..996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:994-996)
  on lines 998..999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:998-999)
  on line 1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1005-1005)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:202-202)
  on lines 207..208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:207-208)
  on lines 210..211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:210-211)
  on lines 213..214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:213-214)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 2723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2723-2723)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1615-1615)
  on lines 1620..1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1620-1621)
  on line 1629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1629-1629)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:812-812)
  on line 815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:815-815)
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:818-818)
  on line 821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:821-821)
  on line 824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:824-824)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:962-962)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 2996..2997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2996-2997)
  on lines 3000..3001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3000-3001)
  on lines 3004..3005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3004-3005)
  on lines 3008..3009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3008-3009)
  on lines 3012..3013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3012-3013)
  on lines 3019..3020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3019-3020)
  on line 3027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3027-3027)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 2957..2958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2957-2958)
  on lines 2961..2962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2961-2962)
  on lines 2965..2966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2965-2966)
  on lines 2969..2970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2969-2970)
  on lines 2973..2974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2973-2974)
  on lines 2980..2981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2980-2981)
  on line 2988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2988-2988)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 2918..2919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2918-2919)
  on lines 2922..2923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2922-2923)
  on lines 2926..2927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2926-2927)
  on lines 2930..2931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2930-2931)
  on lines 2934..2935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2934-2935)
  on lines 2941..2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2941-2942)
  on line 2949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2949-2949)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 410..411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:410-411)
  on lines 413..414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:413-414)
  on lines 416..417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:416-417)
  on lines 419..420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:419-420)
  on lines 422..423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:422-423)
  on lines 425..426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:425-426)
  on line 438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:438-438)
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:441-441)
  on line 444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:444-444)
  on line 447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:447-447)
  on line 450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:450-450)
  on lines 463..465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:463-465)
  on lines 467..468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:467-468)
  on lines 470..471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:470-471)
  on lines 473..474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:473-474)
  on lines 476..477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:476-477)
  on lines 479..480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:479-480)
  on lines 490..492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:490-492)
  on lines 494..495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:494-495)
  on lines 497..498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:497-498)
  on lines 500..501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:500-501)
  on lines 503..504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:503-504)
  on lines 506..507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:506-507)
  on lines 517..519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:517-519)
  on lines 521..522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:521-522)
  on lines 524..525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:524-525)
  on lines 527..528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:527-528)
  on lines 530..531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:530-531)
  on lines 533..534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:533-534)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 1576..1577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1576-1577)
  on lines 1580..1581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1580-1581)
  on lines 1584..1585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1584-1585)
  on lines 1588..1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1588-1589)
  on lines 1592..1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1592-1593)
  on line 1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1602-1602)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:804-804)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 2362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2362-2362)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 164..166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:164-166)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 1147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1147-1147)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 230..232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:230-232)
  on lines 234..236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:234-236)
  on lines 238..240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:238-240)
  on lines 242..244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:242-244)
  on lines 246..248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:246-248)
  on lines 250..252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:250-252)
  on lines 295..298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:295-298)
  on lines 300..302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:300-302)
  on lines 304..306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:304-306)
  on lines 308..310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:308-310)
  on lines 312..314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:312-314)
  on lines 316..318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:316-318)
  on lines 328..331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:328-331)
  on lines 333..335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:333-335)
  on lines 337..339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:337-339)
  on lines 341..343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:341-343)
  on lines 345..347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:345-347)
  on lines 349..351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:349-351)
  on lines 361..364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:361-364)
  on lines 366..368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:366-368)
  on lines 370..372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:370-372)
  on lines 374..376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:374-376)
  on lines 378..380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:378-380)
  on lines 382..384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:382-384)
  on lines 400..402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:400-402)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:713-713)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 2907..2909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2907-2909)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:905-905)
  on line 908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:908-908)
  on line 911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:911-911)
  on lines 916..917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:916-917)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1754..1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1754-1757)
  on lines 1767..1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1767-1770)
  on lines 1780..1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1780-1783)
  on lines 1793..1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1793-1796)
  on lines 1806..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1806-1809)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 561..562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:561-562)
  on lines 564..565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:564-565)
  on lines 567..568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:567-568)
  on lines 570..571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:570-571)
  on lines 573..574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:573-574)
  on lines 576..577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:576-577)
  on line 589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:589-589)
  on line 592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:592-592)
  on line 595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:595-595)
  on line 598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:598-598)
  on line 601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:601-601)
  on lines 614..616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:614-616)
  on lines 618..619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:618-619)
  on lines 621..622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:621-622)
  on lines 624..625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:624-625)
  on lines 627..628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:627-628)
  on lines 630..631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:630-631)
  on lines 641..643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:641-643)
  on lines 645..646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:645-646)
  on lines 648..649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:648-649)
  on lines 651..652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:651-652)
  on lines 654..655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:654-655)
  on lines 657..658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:657-658)
  on lines 668..670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:668-670)
  on lines 672..673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:672-673)
  on lines 675..676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:675-676)
  on lines 678..679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:678-679)
  on lines 681..682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:681-682)
  on lines 684..685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:684-685)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:174-174)
  on lines 179..180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:179-180)
  on lines 182..183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:182-183)
  on lines 185..186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:185-186)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:933-933)
  on lines 938..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:938-939)
  on lines 941..942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:941-942)
  on lines 944..945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:944-945)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 2883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2883-2883)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1700-1700)
  on line 1702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1702-1702)
  on line 1704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1704-1704)
  on line 1706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1706-1706)
  on lines 1708..1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1708-1709)
  on line 1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1717-1717)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__twothirdsfull' has dead code:
  on lines 1674..1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1674-1676)
  on line 1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1678-1678)
  on line 1686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1686-1686)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__weight' has dead code:
  on lines 1651..1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1651-1652)
  on line 1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1658-1658)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 1555..1558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1555-1558)
  on line 1560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1560-1560)
  on line 1568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1568-1568)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__twothirdsfull' has dead code:
  on line 1520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1520-1520)
  on line 1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1522-1522)
  on line 1524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1524-1524)
  on line 1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1527-1527)
  on line 1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1530-1530)
  on line 1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1539-1539)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__weight' has dead code:
  on lines 1170..1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1170-1171)
  on line 1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1176-1176)
  on line 1178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1178-1178)
  on lines 1180..1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1180-1182)
  on lines 1192..1195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1192-1195)
  on lines 1220..1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1220-1224)
  on lines 1233..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1233-1234)
  on line 1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1236-1236)
  on lines 1238..1240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1238-1240)
  on lines 1249..1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1249-1253)
  on lines 1262..1263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1262-1263)
  on line 1265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1265-1265)
  on lines 1267..1269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1267-1269)
  on lines 1278..1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1278-1282)
  on lines 1291..1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1291-1292)
  on line 1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1294-1294)
  on lines 1296..1298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1296-1298)
  on lines 1307..1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1307-1311)
  on lines 1313..1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1313-1314)
  on lines 1317..1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1317-1318)
  on lines 1321..1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1321-1322)
  on lines 1334..1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1334-1336)
  on lines 1340..1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1340-1341)
  on line 1343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1343-1343)
  on lines 1345..1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1345-1347)
  on lines 1356..1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1356-1360)
  on lines 1369..1370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1369-1370)
  on line 1372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1372-1372)
  on lines 1374..1376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1374-1376)
  on lines 1385..1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1385-1389)
  on lines 1398..1399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1398-1399)
  on line 1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1401-1401)
  on lines 1403..1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1403-1405)
  on lines 1414..1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1414-1418)
  on lines 1427..1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1427-1428)
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1430-1430)
  on lines 1432..1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1432-1434)
  on lines 1443..1447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1443-1447)
  on lines 1456..1457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1456-1457)
  on line 1459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1459-1459)
  on lines 1461..1463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1461-1463)
  on lines 1472..1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1472-1476)
  on lines 1478..1479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1478-1479)
  on lines 1482..1483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1482-1483)
  on lines 1486..1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1486-1487)
  on line 1499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1499-1499)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1854-1854)
  on line 1856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1856-1856)
  on line 1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1858-1858)
  on line 1868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1868-1868)
  on line 1870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1870-1870)
  on line 1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1872-1872)
  on line 1882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1882-1882)
  on line 1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1884-1884)
  on line 1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1886-1886)
  on line 1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1896-1896)
  on line 1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1898-1898)
  on line 1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1900-1900)
  on line 1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1910-1910)
  on line 1912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1912-1912)
  on line 1914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1914-1914)
  on line 1924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1924-1924)
  on line 1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1926-1926)
  on line 1928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1928-1928)
  on lines 1955..1956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1955-1956)
  on line 1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1958-1958)
  on lines 1960..1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1960-1961)
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1965-1965)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3074-3074)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 350
  dead: 1089 (540 in uncalled functions)
  total lines: 1439
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:811:7-811:13)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2929:13-2929:24)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:814:9-814:15)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:201:7-201:19)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1698:7-1698:10)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2933:15-2933:26)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:817:11-817:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:204:9-204:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2937:17-2937:28)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:820:13-820:19)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:587:9-587:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:588:11-588:22)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:823:15-823:21)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:591:13-591:24)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:826:17-826:23)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:594:15-594:26)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2956:7-2956:18)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:597:17-597:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:229:7-229:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:409:7-409:17)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2960:9-2960:20)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1069:7-1069:14)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:600:19-600:30)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2964:11-2964:22)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:603:21-603:32)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1073:9-1073:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2397:7-2397:17)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1752:7-1752:14)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2968:13-2968:24)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2400:9-2400:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2972:15-2972:26)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2403:11-2403:21)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1519:7-1519:15)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1765:7-1765:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1084:13-1084:27)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2976:17-2976:28)
[Warning][Deadcode][CWE-571] condition 'floor == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2406:13-2406:23)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:436:9-436:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:437:11-437:22)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1091:15-1091:22)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:440:13-440:24)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1778:7-1778:14)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:262:9-262:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2995:7-2995:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1095:17-1095:31)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:443:15-443:26)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2435:7-2435:17)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2999:9-2999:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2702:10-2702:11)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1553:7-1553:14)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:446:17-446:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:904:7-904:19)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1791:7-1791:14)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1102:19-1102:26)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:449:19-449:30)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3003:11-3003:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2706:9-2706:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:907:9-907:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:452:21-452:32)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2710:11-2710:23)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2450:9-2450:19)
[Warning][Deadcode][CWE-571] condition 'floorButtons_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1106:21-1106:35)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3007:13-3007:24)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2451:11-2451:30)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:910:11-910:23)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1804:7-1804:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1575:7-1575:21)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:913:13-913:25)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3011:15-3011:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2722:9-2722:12)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1579:9-1579:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:3015:17-3015:28)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2465:11-2465:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:283:21-283:32)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:932:7-932:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2702:10-2702:11)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1817:7-1817:15)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1583:11-1583:25)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:935:9-935:21)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2706:9-2706:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1587:13-1587:27)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2480:13-2480:23)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2710:11-2710:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1591:15-1591:29)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1165:7-1165:15)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2722:9-2722:12)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1852:9-1852:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1169:9-1169:12)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2495:15-2495:25)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1610:7-1610:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1175:9-1175:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2702:10-2702:11)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1866:9-1866:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1614:9-1614:12)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2706:9-2706:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2522:7-2522:26)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:978:7-978:19)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2710:11-2710:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2527:9-2527:28)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1880:9-1880:18)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1626:7-1626:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1191:11-1191:29)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2532:11-2532:30)
[Warning][Deadcode][CWE-571] condition 'floorButtons_spc2_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2537:13-2537:32)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1894:9-1894:18)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1204:13-1204:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1205:15-1205:32)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1908:9-1908:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:154:15-154:27)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1209:17-1209:24)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2899:7-2899:10)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1650:9-1650:12)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1922:9-1922:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:173:7-173:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2917:7-2917:18)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:560:7-560:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:176:9-176:21)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1672:7-1672:26)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2921:9-2921:20)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1941:9-1941:23)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:2925:11-2925:22)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product24.cil.c:1949:9-1949:16)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
