./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/elevator_spec9_product32.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/elevator_spec9_product32.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_product32.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_product32.cil.c:2405:5-2463:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2480:9-2538:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2652:3-2673:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2709:3-2734:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2794:5-2814:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3124:3-3152:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3184:3-3227:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3467:3-3486:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3514:3-3533:3 with factor 5
[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] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:92:1-133:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:934:1-956:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:957:1-979:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1033:1-1064:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1065:1-1076:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1077:1-1096:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1209:1-1217:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1921:1-1934:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2202:1-2372:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2373:1-2394:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2395:1-2553:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2565:1-2573:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2581:1-2626:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2627:1-2682:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2683:1-2742:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2745:1-2847:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2848:1-2893:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2894:1-2939:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2945:1-2954:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2981:1-3032:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3034:1-3044:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3045:1-3055:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3056:1-3066:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3067:1-3077:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3078:1-3088:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3100:1-3111:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3158:1-3235:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3236:1-3247:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3248:1-3259:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3260:1-3270:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3271:1-3287:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3449:1-3491:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3492:1-3538:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:722-722)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__2' has dead code:
  on line 769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:769-769)
  on line 772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:772-772)
  on line 775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:775-775)
  on lines 780..781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:780-781)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__3' has dead code:
  on lines 816..817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:816-817)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:825-825)
  on lines 832..833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:832-833)
  on lines 840..841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:840-841)
  on lines 848..849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:848-849)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__4' has dead code:
  on line 873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:873-873)
  on line 878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:878-878)
  on line 883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:883-883)
  on line 891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:891-891)
  on line 893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:893-893)
  on line 902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:902-902)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 1271..1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1271-1272)
  on lines 1275..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1275-1276)
  on lines 1286..1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1286-1287)
  on lines 1293..1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1293-1294)
  on lines 1297..1298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1297-1298)
  on lines 1304..1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1304-1305)
  on line 1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1312-1312)
  on lines 1314..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1314-1316)
  on lines 1318..1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1318-1320)
  on lines 1333..1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1333-1335)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1172-1172)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1183..1185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1183-1185)
  on lines 1187..1189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1187-1189)
  on lines 1191..1193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1191-1193)
  on lines 1195..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1195-1197)
  on lines 1199..1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1199-1200)
  on line 1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1206-1206)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:202-202)
  on lines 207..208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:207-208)
  on lines 210..211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:210-211)
  on lines 213..214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:213-214)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 3145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3145-3145)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 1816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1816-1816)
  on lines 1821..1822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1821-1822)
  on line 1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1830-1830)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:994-994)
  on line 997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:997-997)
  on line 1000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1000-1000)
  on line 1003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1003-1003)
  on line 1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1006-1006)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1163-1163)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 3414..3415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3414-3415)
  on lines 3418..3419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3418-3419)
  on lines 3422..3423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3422-3423)
  on lines 3426..3427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3426-3427)
  on lines 3430..3431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3430-3431)
  on lines 3437..3438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3437-3438)
  on line 3445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3445-3445)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 3375..3376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3375-3376)
  on lines 3379..3380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3379-3380)
  on lines 3383..3384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3383-3384)
  on lines 3387..3388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3387-3388)
  on lines 3391..3392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3391-3392)
  on lines 3398..3399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3398-3399)
  on line 3406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3406-3406)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 3336..3337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3336-3337)
  on lines 3340..3341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3340-3341)
  on lines 3344..3345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3344-3345)
  on lines 3348..3349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3348-3349)
  on lines 3352..3353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3352-3353)
  on lines 3359..3360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3359-3360)
  on line 3367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3367-3367)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 410..411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:410-411)
  on lines 413..414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:413-414)
  on lines 416..417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:416-417)
  on lines 419..420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:419-420)
  on lines 422..423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:422-423)
  on lines 425..426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:425-426)
  on line 438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:438-438)
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:441-441)
  on line 444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:444-444)
  on line 447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:447-447)
  on line 450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:450-450)
  on lines 463..465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:463-465)
  on lines 467..468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:467-468)
  on lines 470..471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:470-471)
  on lines 473..474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:473-474)
  on lines 476..477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:476-477)
  on lines 479..480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:479-480)
  on lines 490..492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:490-492)
  on lines 494..495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:494-495)
  on lines 497..498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:497-498)
  on lines 500..501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:500-501)
  on lines 503..504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:503-504)
  on lines 506..507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:506-507)
  on lines 517..519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:517-519)
  on lines 521..522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:521-522)
  on lines 524..525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:524-525)
  on lines 527..528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:527-528)
  on lines 530..531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:530-531)
  on lines 533..534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:533-534)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 1777..1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1777-1778)
  on lines 1781..1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1781-1782)
  on lines 1785..1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1785-1786)
  on lines 1789..1790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1789-1790)
  on lines 1793..1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1793-1794)
  on line 1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1803-1803)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:986-986)
[Warning][Deadcode] Function 'isEmpty' has dead code:
  on lines 1223..1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1223-1224)
  on lines 1227..1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1227-1228)
  on lines 1231..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1231-1232)
  on lines 1235..1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1235-1236)
  on lines 1239..1240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1239-1240)
  on line 1255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1255-1255)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 2562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2562-2562)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 164..166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:164-166)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 1348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1348-1348)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 230..232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:230-232)
  on lines 234..236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:234-236)
  on lines 238..240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:238-240)
  on lines 242..244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:242-244)
  on lines 246..248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:246-248)
  on lines 250..252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:250-252)
  on lines 295..298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:295-298)
  on lines 300..302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:300-302)
  on lines 304..306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:304-306)
  on lines 308..310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:308-310)
  on lines 312..314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:312-314)
  on lines 316..318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:316-318)
  on lines 328..331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:328-331)
  on lines 333..335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:333-335)
  on lines 337..339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:337-339)
  on lines 341..343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:341-343)
  on lines 345..347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:345-347)
  on lines 349..351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:349-351)
  on lines 361..364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:361-364)
  on lines 366..368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:366-368)
  on lines 370..372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:370-372)
  on lines 374..376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:374-376)
  on lines 378..380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:378-380)
  on lines 382..384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:382-384)
  on lines 400..402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:400-402)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:713-713)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 3325..3327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3325-3327)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1106-1106)
  on line 1109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1109-1109)
  on line 1112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1112-1112)
  on lines 1117..1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1117-1118)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1955..1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1955-1958)
  on lines 1968..1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1968-1971)
  on lines 1981..1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1981-1984)
  on lines 1994..1997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1994-1997)
  on lines 2007..2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2007-2010)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 561..562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:561-562)
  on lines 564..565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:564-565)
  on lines 567..568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:567-568)
  on lines 570..571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:570-571)
  on lines 573..574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:573-574)
  on lines 576..577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:576-577)
  on line 589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:589-589)
  on line 592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:592-592)
  on line 595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:595-595)
  on line 598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:598-598)
  on line 601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:601-601)
  on lines 614..616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:614-616)
  on lines 618..619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:618-619)
  on lines 621..622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:621-622)
  on lines 624..625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:624-625)
  on lines 627..628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:627-628)
  on lines 630..631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:630-631)
  on lines 641..643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:641-643)
  on lines 645..646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:645-646)
  on lines 648..649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:648-649)
  on lines 651..652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:651-652)
  on lines 654..655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:654-655)
  on lines 657..658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:657-658)
  on lines 668..670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:668-670)
  on lines 672..673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:672-673)
  on lines 675..676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:675-676)
  on lines 678..679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:678-679)
  on lines 681..682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:681-682)
  on lines 684..685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:684-685)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:174-174)
  on lines 179..180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:179-180)
  on lines 182..183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:182-183)
  on lines 185..186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:185-186)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1134-1134)
  on lines 1139..1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1139-1140)
  on lines 1142..1143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1142-1143)
  on lines 1145..1146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1145-1146)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 3304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3304-3304)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1901-1901)
  on line 1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1903-1903)
  on line 1905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1905-1905)
  on line 1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1907-1907)
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1909-1910)
  on line 1918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1918-1918)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 1852..1853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1852-1853)
  on line 1859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1859-1859)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__twothirdsfull' has dead code:
  on lines 1875..1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1875-1877)
  on line 1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1879-1879)
  on line 1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1887-1887)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 1756..1759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1756-1759)
  on line 1761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1761-1761)
  on line 1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1769-1769)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on lines 1371..1372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1371-1372)
  on line 1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1377-1377)
  on line 1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1379-1379)
  on lines 1381..1383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1381-1383)
  on lines 1393..1396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1393-1396)
  on lines 1421..1425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1421-1425)
  on lines 1434..1435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1434-1435)
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1437-1437)
  on lines 1439..1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1439-1441)
  on lines 1450..1454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1450-1454)
  on lines 1463..1464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1463-1464)
  on line 1466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1466-1466)
  on lines 1468..1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1468-1470)
  on lines 1479..1483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1479-1483)
  on lines 1492..1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1492-1493)
  on line 1495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1495-1495)
  on lines 1497..1499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1497-1499)
  on lines 1508..1512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1508-1512)
  on lines 1514..1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1514-1515)
  on lines 1518..1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1518-1519)
  on lines 1522..1523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1522-1523)
  on lines 1535..1537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1535-1537)
  on lines 1541..1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1541-1542)
  on line 1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1544-1544)
  on lines 1546..1548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1546-1548)
  on lines 1557..1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1557-1561)
  on lines 1570..1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1570-1571)
  on line 1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1573-1573)
  on lines 1575..1577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1575-1577)
  on lines 1586..1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1586-1590)
  on lines 1599..1600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1599-1600)
  on line 1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1602-1602)
  on lines 1604..1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1604-1606)
  on lines 1615..1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1615-1619)
  on lines 1628..1629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1628-1629)
  on line 1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1631-1631)
  on lines 1633..1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1633-1635)
  on lines 1644..1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1644-1648)
  on lines 1657..1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1657-1658)
  on line 1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1660-1660)
  on lines 1662..1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1662-1664)
  on lines 1673..1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1673-1677)
  on lines 1679..1680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1679-1680)
  on lines 1683..1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1683-1684)
  on lines 1687..1688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1687-1688)
  on line 1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1700-1700)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__twothirdsfull' has dead code:
  on line 1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1721-1721)
  on line 1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1723-1723)
  on line 1725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1725-1725)
  on line 1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1728-1728)
  on line 1731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1731-1731)
  on line 1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1740-1740)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 2055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2055-2055)
  on line 2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2057-2057)
  on line 2059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2059-2059)
  on line 2069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2069-2069)
  on line 2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2071-2071)
  on line 2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2073-2073)
  on line 2083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2083-2083)
  on line 2085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2085-2085)
  on line 2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2087-2087)
  on line 2097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2097-2097)
  on line 2099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2099-2099)
  on line 2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2101-2101)
  on line 2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2111-2111)
  on line 2113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2113-2113)
  on line 2115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2115-2115)
  on line 2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2125-2125)
  on line 2127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2127-2127)
  on line 2129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2129-2129)
  on lines 2156..2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2156-2157)
  on line 2159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2159-2159)
  on lines 2161..2162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2161-2162)
  on line 2166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2166-2166)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2975-2975)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 370
  dead: 1078 (528 in uncalled functions)
  total lines: 1448
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3132:11-3132:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:201:7-201:19)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1720:7-1720:15)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1966:7-1966:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1285:13-1285:27)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3144:9-3144:12)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:204:9-204:21)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:814:9-814:16)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:815:11-815:21)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.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_spec9_product32.cil.c:588:11-588:22)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1292:15-1292:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3124:10-3124:11)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1979:7-1979:14)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:591:13-591:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:823:13-823:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1296:17-1296:31)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:824:15-824:34)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:594:15-594:26)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3128:9-3128:23)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1754:7-1754:14)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:831:15-831:25)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.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_spec9_product32.cil.c:229:7-229:17)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3132:11-3132:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:409:7-409:17)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1992:7-1992:14)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1303:19-1303:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1105:7-1105:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:600:19-600:30)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1108:9-1108:21)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:839:17-839:27)
[Warning][Deadcode][CWE-571] condition 'floorButtons_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1307:21-1307:35)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:603:21-603:32)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1111:11-1111:23)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2005:7-2005:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1776:7-1776:21)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:847:19-847:29)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1114:13-1114:25)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1780:9-1780:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:871:7-871:26)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3317:7-3317:10)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2018:7-2018:15)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1784:11-1784:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1133:7-1133:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:876:9-876:28)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:436:9-436:19)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1136:9-1136:21)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:881:11-881:30)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:437:11-437:22)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1788:13-1788:27)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3335:7-3335:18)
[Warning][Deadcode][CWE-571] condition 'floorButtons_spc9_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:886:13-886:32)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:440:13-440:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:262:9-262:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1792:15-1792:29)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:443:15-443:26)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3339:9-3339:20)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1366:7-1366:15)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:446:17-446:28)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3343:11-3343:22)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2053:9-2053:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1370:9-1370:12)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:449:19-449:30)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3347:13-3347:24)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1811:7-1811:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1376:9-1376:27)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:452:21-452:32)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2067:9-2067:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1815:9-1815:12)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3351:15-3351:26)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1179:7-1179:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3355:17-3355:28)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2081:9-2081:18)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1827:7-1827:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1392:11-1392:29)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:283:21-283:32)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2095:9-2095:18)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3374:7-3374:18)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1405:13-1405:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1406:15-1406:32)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3378:9-3378:20)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2109:9-2109:18)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1410:17-1410:24)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1851:9-1851:12)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3382:11-3382:22)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2123:9-2123:18)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3386:13-3386:24)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:993:7-993:13)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3390:15-3390:26)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1873:7-1873:26)
[Warning][Deadcode][CWE-570] condition 'persons_0 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1222:7-1222:21)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:996:9-996:15)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2142:9-2142:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3394:17-3394:28)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:999:11-999:17)
[Warning][Deadcode][CWE-570] condition 'persons_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1226:9-1226:23)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:2150:9-2150:16)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1002:13-1002:19)
[Warning][Deadcode][CWE-570] condition 'persons_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1230:11-1230:25)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1005:15-1005:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3413:7-3413:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1899:7-1899:10)
[Warning][Deadcode][CWE-570] condition 'persons_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1234:13-1234:27)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1008:17-1008:23)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3417:9-3417:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3124:10-3124:11)
[Warning][Deadcode][CWE-570] condition 'persons_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1238:15-1238:29)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3421:11-3421:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3128:9-3128:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:768:7-768:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:154:15-154:27)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3132:11-3132:23)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:771:9-771:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3425:13-3425:24)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:774:11-774:21)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3429:15-3429:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3144:9-3144:12)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:173:7-173:19)
[Warning][Deadcode][CWE-571] condition 'floor == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:777:13-777:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:560:7-560:17)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3433:17-3433:28)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:176:9-176:21)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1270:7-1270:14)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3124:10-3124:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1274:9-1274:23)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:1953:7-1953:14)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_product32.cil.c:3128:9-3128:23)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
