./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_spec9_product30.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_spec9_product30.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_spec9_product30.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_spec9_product30.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:268:5-288:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:667:3-686:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:714:3-733:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2295:5-2353:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2370:9-2428:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3249:3-3277:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3309:3-3352:3 with factor 1
[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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:419:1-428:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:649:1-691:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:692:1-738:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:885:1-907:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:908:1-930:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:984:1-1015:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1016:1-1027:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1028:1-1047:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1160:1-1168:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1811:1-1824:1)
[Warning][Deadcode] Function 'printState__wrappee__twothirdsfull' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2092:1-2262:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2263:1-2284:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2285:1-2443:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2481:1-2522:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3107:1-3158:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3159:1-3169:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3170:1-3180:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3181:1-3191:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3192:1-3202:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3203:1-3213:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3225:1-3236:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3283:1-3360:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3361:1-3372:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3373:1-3384:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3385:1-3395:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3396:1-3412:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:458-458)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__2' has dead code:
  on line 490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:490-490)
  on line 493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:493-493)
  on line 496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:496-496)
  on lines 501..502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:501-502)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__3' has dead code:
  on lines 537..538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:537-538)
  on line 546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:546-546)
  on lines 553..554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:553-554)
  on lines 561..562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:561-562)
  on lines 569..570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:569-570)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__4' has dead code:
  on line 594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:594-594)
  on line 599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:599-599)
  on line 604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:604-604)
  on line 612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:612-612)
  on line 614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:614-614)
  on line 623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:623-623)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 1222..1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1222-1223)
  on lines 1226..1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1226-1227)
  on lines 1237..1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1237-1238)
  on lines 1244..1245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1244-1245)
  on lines 1248..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1248-1249)
  on lines 1255..1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1255-1256)
  on line 1263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1263-1263)
  on lines 1265..1267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1265-1267)
  on lines 1269..1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1269-1271)
  on lines 1284..1286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1284-1286)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1123-1123)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1134..1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1134-1136)
  on lines 1138..1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1138-1140)
  on lines 1142..1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1142-1144)
  on lines 1146..1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1146-1148)
  on lines 1150..1151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1150-1151)
  on line 1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1157-1157)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2591-2591)
  on lines 2596..2597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2596-2597)
  on lines 2599..2600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2599-2600)
  on lines 2602..2603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2602-2603)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 3270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3270-3270)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1737-1737)
  on lines 1742..1743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1742-1743)
  on line 1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1751-1751)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:945-945)
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:948-948)
  on line 951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:951-951)
  on line 954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:954-954)
  on line 957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:957-957)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1114-1114)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 825..826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:825-826)
  on lines 829..830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:829-830)
  on lines 833..834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:833-834)
  on lines 837..838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:837-838)
  on lines 841..842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:841-842)
  on lines 848..849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:848-849)
  on line 856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:856-856)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 786..787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:786-787)
  on lines 790..791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:790-791)
  on lines 794..795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:794-795)
  on lines 798..799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:798-799)
  on lines 802..803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:802-803)
  on lines 809..810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:809-810)
  on line 817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:817-817)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 747..748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:747-748)
  on lines 751..752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:751-752)
  on lines 755..756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:755-756)
  on lines 759..760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:759-760)
  on lines 763..764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:763-764)
  on lines 770..771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:770-771)
  on line 778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:778-778)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 2799..2800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2799-2800)
  on lines 2802..2803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2802-2803)
  on lines 2805..2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2805-2806)
  on lines 2808..2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2808-2809)
  on lines 2811..2812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2811-2812)
  on lines 2814..2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2814-2815)
  on line 2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2827-2827)
  on line 2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2830-2830)
  on line 2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2833-2833)
  on line 2836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2836-2836)
  on line 2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2839-2839)
  on lines 2852..2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2852-2854)
  on lines 2856..2857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2856-2857)
  on lines 2859..2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2859-2860)
  on lines 2862..2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2862-2863)
  on lines 2865..2866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2865-2866)
  on lines 2868..2869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2868-2869)
  on lines 2879..2881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2879-2881)
  on lines 2883..2884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2883-2884)
  on lines 2886..2887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2886-2887)
  on lines 2889..2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2889-2890)
  on lines 2892..2893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2892-2893)
  on lines 2895..2896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2895-2896)
  on lines 2906..2908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2906-2908)
  on lines 2910..2911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2910-2911)
  on lines 2913..2914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2913-2914)
  on lines 2916..2917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2916-2917)
  on lines 2919..2920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2919-2920)
  on lines 2922..2923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2922-2923)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 1698..1699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1698-1699)
  on lines 1702..1703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1702-1703)
  on lines 1706..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1706-1707)
  on lines 1710..1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1710-1711)
  on lines 1714..1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1714-1715)
  on line 1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1724-1724)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:937-937)
[Warning][Deadcode] Function 'isEmpty' has dead code:
  on lines 1174..1175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1174-1175)
  on lines 1178..1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1178-1179)
  on lines 1182..1183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1182-1183)
  on lines 1186..1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1186-1187)
  on lines 1190..1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1190-1191)
  on line 1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1206-1206)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2543..2545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2543-2545)
  on lines 2553..2555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2553-2555)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1299-1299)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2619..2621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2619-2621)
  on lines 2623..2625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2623-2625)
  on lines 2627..2629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2627-2629)
  on lines 2631..2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2631-2633)
  on lines 2635..2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2635-2637)
  on lines 2639..2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2639-2641)
  on lines 2684..2687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2684-2687)
  on lines 2689..2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2689-2691)
  on lines 2693..2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2693-2695)
  on lines 2697..2699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2697-2699)
  on lines 2701..2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2701-2703)
  on lines 2705..2707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2705-2707)
  on lines 2717..2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2717-2720)
  on lines 2722..2724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2722-2724)
  on lines 2726..2728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2726-2728)
  on lines 2730..2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2730-2732)
  on lines 2734..2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2734-2736)
  on lines 2738..2740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2738-2740)
  on lines 2750..2753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2750-2753)
  on lines 2755..2757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2755-2757)
  on lines 2759..2761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2759-2761)
  on lines 2763..2765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2763-2765)
  on lines 2767..2769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2767-2769)
  on lines 2771..2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2771-2773)
  on lines 2789..2791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2789-2791)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 3102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3102-3102)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 3450..3452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3450-3452)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1057-1057)
  on line 1060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1060-1060)
  on line 1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1063-1063)
  on lines 1068..1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1068-1069)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1845..1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1845-1848)
  on lines 1858..1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1858-1861)
  on lines 1871..1874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1871-1874)
  on lines 1884..1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1884-1887)
  on lines 1897..1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1897-1900)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 2950..2951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2950-2951)
  on lines 2953..2954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2953-2954)
  on lines 2956..2957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2956-2957)
  on lines 2959..2960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2959-2960)
  on lines 2962..2963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2962-2963)
  on lines 2965..2966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2965-2966)
  on line 2978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2978-2978)
  on line 2981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2981-2981)
  on line 2984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2984-2984)
  on line 2987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2987-2987)
  on line 2990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2990-2990)
  on lines 3003..3005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3003-3005)
  on lines 3007..3008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3007-3008)
  on lines 3010..3011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3010-3011)
  on lines 3013..3014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3013-3014)
  on lines 3016..3017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3016-3017)
  on lines 3019..3020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3019-3020)
  on lines 3030..3032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3030-3032)
  on lines 3034..3035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3034-3035)
  on lines 3037..3038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3037-3038)
  on lines 3040..3041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3040-3041)
  on lines 3043..3044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3043-3044)
  on lines 3046..3047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3046-3047)
  on lines 3057..3059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3057-3059)
  on lines 3061..3062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3061-3062)
  on lines 3064..3065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3064-3065)
  on lines 3067..3068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3067-3068)
  on lines 3070..3071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3070-3071)
  on lines 3073..3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3073-3074)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2563-2563)
  on lines 2568..2569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2568-2569)
  on lines 2571..2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2571-2572)
  on lines 2574..2575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2574-2575)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1085-1085)
  on lines 1090..1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1090-1091)
  on lines 1093..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1093-1094)
  on lines 1096..1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1096-1097)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 3429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3429-3429)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on lines 1796..1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1796-1798)
  on line 1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1800-1800)
  on line 1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1808-1808)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 1773..1774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1773-1774)
  on line 1780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1780-1780)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1671-1671)
  on line 1673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1673-1673)
  on line 1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1675-1675)
  on line 1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1678-1678)
  on line 1681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1681-1681)
  on line 1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1690-1690)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on lines 1322..1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1322-1323)
  on line 1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1328-1328)
  on line 1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1330-1330)
  on lines 1332..1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1332-1334)
  on lines 1344..1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1344-1347)
  on lines 1372..1376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1372-1376)
  on lines 1385..1386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1385-1386)
  on line 1388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1388-1388)
  on lines 1390..1392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1390-1392)
  on lines 1401..1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1401-1405)
  on lines 1414..1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1414-1415)
  on line 1417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1417-1417)
  on lines 1419..1421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1419-1421)
  on lines 1430..1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1430-1434)
  on lines 1443..1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1443-1444)
  on line 1446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1446-1446)
  on lines 1448..1450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1448-1450)
  on lines 1459..1463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1459-1463)
  on lines 1465..1466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1465-1466)
  on lines 1469..1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1469-1470)
  on lines 1473..1474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1473-1474)
  on lines 1486..1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1486-1488)
  on lines 1492..1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1492-1493)
  on line 1495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1495-1495)
  on lines 1497..1499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1497-1499)
  on lines 1508..1512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1508-1512)
  on lines 1521..1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1521-1522)
  on line 1524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1524-1524)
  on lines 1526..1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1526-1528)
  on lines 1537..1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1537-1541)
  on lines 1550..1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1550-1551)
  on line 1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1553-1553)
  on lines 1555..1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1555-1557)
  on lines 1566..1570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1566-1570)
  on lines 1579..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1579-1580)
  on line 1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1582-1582)
  on lines 1584..1586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1584-1586)
  on lines 1595..1599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1595-1599)
  on lines 1608..1609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1608-1609)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1611-1611)
  on lines 1613..1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1613-1615)
  on lines 1624..1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1624-1628)
  on lines 1630..1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1630-1631)
  on lines 1634..1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1634-1635)
  on lines 1638..1639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1638-1639)
  on line 1651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1651-1651)
[Warning][Deadcode] Function 'timeShift__wrappee__twothirdsfull' has dead code:
  on line 1945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1945-1945)
  on line 1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1947-1947)
  on line 1949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1949-1949)
  on line 1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1959-1959)
  on line 1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1961-1961)
  on line 1963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1963-1963)
  on line 1973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1973-1973)
  on line 1975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1975-1975)
  on line 1977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1977-1977)
  on line 1987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1987-1987)
  on line 1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1989-1989)
  on line 1991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1991-1991)
  on line 2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2001-2001)
  on line 2003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2003-2003)
  on line 2005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2005-2005)
  on line 2015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2015-2015)
  on line 2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2017-2017)
  on line 2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2019-2019)
  on lines 2046..2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2046-2047)
  on line 2049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2049-2049)
  on lines 2051..2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2051-2052)
  on line 2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2056-2056)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:449-449)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 354
  dead: 1064 (525 in uncalled functions)
  total lines: 1418
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:947:9-947:15)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3269:9-3269:12)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2672:21-2672:32)
[Warning][Deadcode][CWE-570] condition 'persons_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1177:9-1177:23)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:950:11-950:17)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:746:7-746:18)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1843:7-1843:14)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:953:13-953:19)
[Warning][Deadcode][CWE-570] condition 'persons_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1181:11-1181:25)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3249:10-3249:11)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:956:15-956:21)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:750:9-750:20)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:535:9-535:16)
[Warning][Deadcode][CWE-570] condition 'persons_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1185:13-1185:27)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:536:11-536:21)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:959:17-959:23)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3253:9-3253:23)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:754:11-754:22)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1856:7-1856:14)
[Warning][Deadcode][CWE-570] condition 'persons_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1189:15-1189:29)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3257:11-3257:23)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:544:13-544:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:758:13-758:24)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:545:15-545:34)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:762:15-762:26)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:552:15-552:25)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1869:7-1869:14)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:766:17-766:28)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:560:17-560:27)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1221:7-1221:14)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1882:7-1882:14)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3442:7-3442:10)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:568:19-568:29)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1225:9-1225:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:785:7-785:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:592:7-592:26)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:789:9-789:20)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1895:7-1895:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:597:9-597:28)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2539:13-2539:25)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:793:11-793:22)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1670:7-1670:15)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:602:11-602:30)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1236:13-1236:27)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:797:13-797:24)
[Warning][Deadcode][CWE-571] condition 'floorButtons_spc9_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:607:13-607:32)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1908:7-1908:15)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1243:15-1243:22)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:801:15-801:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2562:7-2562:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1247:17-1247:31)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:805:17-805:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1697:7-1697:21)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2949:7-2949:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2565:9-2565:21)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1701:9-1701:23)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1254:19-1254:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1056:7-1056:19)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1943:9-1943:18)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:824:7-824:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1705:11-1705:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1059:9-1059:21)
[Warning][Deadcode][CWE-571] condition 'floorButtons_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1258:21-1258:35)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1062:11-1062:23)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:828:9-828:20)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1957:9-1957:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1709:13-1709:27)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2590:7-2590:19)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1065:13-1065:25)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:832:11-832:22)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1713:15-1713:29)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2593:9-2593:21)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1971:9-1971:18)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:836:13-836:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2976:9-2976:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2977:11-2977:22)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1084:7-1084:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:840:15-840:26)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2980:13-2980:24)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1985:9-1985:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1087:9-1087:21)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1732:7-1732:26)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2983:15-2983:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:844:17-844:28)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1736:9-1736:12)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2986:17-2986:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2618:7-2618:17)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1999:9-1999:18)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2798:7-2798:17)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1317:7-1317:15)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2989:19-2989:30)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1748:7-1748:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1321:9-1321:12)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2992:21-2992:32)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2013:9-2013:18)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1327:9-1327:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3249:10-3249:11)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2032:9-2032:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1130:7-1130:19)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3253:9-3253:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1772:9-1772:12)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1343:11-1343:29)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2825:9-2825:19)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2040:9-2040:16)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2826:11-2826:22)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3257:11-3257:23)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2829:13-2829:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2651:9-2651:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:489:7-489:17)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3269:9-3269:12)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2832:15-2832:26)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1356:13-1356:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1357:15-1357:32)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:492:9-492:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2835:17-2835:28)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1794:7-1794:26)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1361:17-1361:24)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:495:11-495:21)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2838:19-2838:30)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3249:10-3249:11)
[Warning][Deadcode][CWE-571] condition 'floor == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:498:13-498:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:2841:21-2841:32)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3253:9-3253:23)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:3257:11-3257:23)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:944:7-944:13)
[Warning][Deadcode][CWE-570] condition 'persons_0 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product30.cil.c:1173:7-1173:21)
[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)
