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


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1495:5-1553:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1570:9-1628:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2651:3-2679:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2711:3-2754:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2937:3-2958:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2994:3-3019:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3079:5-3099:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3244:3-3263:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3291:3-3310: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] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:90:1-112:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:113:1-135:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:189:1-220:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:221:1-232:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:233:1-252:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:366:1-374:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:375:1-414:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:889:1-922:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1010:1-1023:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1292:1-1462:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1463:1-1484:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1485:1-1643:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1655:1-1663:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1669:1-1678:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1749:1-1790:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2509:1-2560:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2561:1-2571:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2572:1-2582:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2583:1-2593:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2594:1-2604:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2605:1-2615:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2627:1-2638:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2685:1-2762:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2763:1-2774:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2775:1-2786:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2787:1-2797:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2798:1-2814:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2866:1-2911:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2912:1-2967:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2968:1-3027:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3030:1-3132:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3133:1-3178:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3179:1-3224:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3226:1-3268:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3269:1-3315:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1708-1708)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__2' has dead code:
  on line 3339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3339-3339)
  on line 3342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3342-3342)
  on line 3345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3345-3345)
  on lines 3350..3351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3350-3351)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__3' has dead code:
  on line 3377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3377-3377)
  on line 3379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3379-3379)
  on lines 3381..3382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3381-3382)
  on line 3394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3394-3394)
  on lines 3396..3397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3396-3397)
  on line 3407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3407-3407)
  on line 3409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3409-3409)
  on lines 3411..3412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3411-3412)
  on line 3422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3422-3422)
  on line 3424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3424-3424)
  on lines 3426..3427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3426-3427)
  on line 3437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3437-3437)
  on line 3439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3439-3439)
  on lines 3441..3442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3441-3442)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__4' has dead code:
  on line 3465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3465-3465)
  on line 3470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3470-3470)
  on line 3475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3475-3475)
  on line 3483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3483-3483)
  on line 3485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3485-3485)
  on line 3494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3494-3494)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 428..429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:428-429)
  on lines 432..433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:432-433)
  on lines 443..444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:443-444)
  on lines 450..451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:450-451)
  on lines 454..455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:454-455)
  on lines 461..462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:461-462)
  on line 469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:469-469)
  on lines 471..473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:471-473)
  on lines 475..477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:475-477)
  on lines 490..492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:490-492)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:329-329)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 340..342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:340-342)
  on lines 344..346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:344-346)
  on lines 348..350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:348-350)
  on lines 352..354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:352-354)
  on lines 356..357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:356-357)
  on line 363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:363-363)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 1859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1859-1859)
  on lines 1864..1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1864-1865)
  on lines 1867..1868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1867-1868)
  on lines 1870..1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1870-1871)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2672-2672)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:933-933)
  on lines 938..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:938-939)
  on line 947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:947-947)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:150-150)
  on line 153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:153-153)
  on line 156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:156-156)
  on line 159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:159-159)
  on line 162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:162-162)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:320-320)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 2472..2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2472-2473)
  on lines 2476..2477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2476-2477)
  on lines 2480..2481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2480-2481)
  on lines 2484..2485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2484-2485)
  on lines 2488..2489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2488-2489)
  on lines 2495..2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2495-2496)
  on line 2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2503-2503)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 2433..2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2433-2434)
  on lines 2437..2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2437-2438)
  on lines 2441..2442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2441-2442)
  on lines 2445..2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2445-2446)
  on lines 2449..2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2449-2450)
  on lines 2456..2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2456-2457)
  on line 2464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2464-2464)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 2394..2395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2394-2395)
  on lines 2398..2399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2398-2399)
  on lines 2402..2403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2402-2403)
  on lines 2406..2407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2406-2407)
  on lines 2410..2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2410-2411)
  on lines 2417..2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2417-2418)
  on line 2425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2425-2425)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 2067..2068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2067-2068)
  on lines 2070..2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2070-2071)
  on lines 2073..2074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2073-2074)
  on lines 2076..2077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2076-2077)
  on lines 2079..2080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2079-2080)
  on lines 2082..2083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2082-2083)
  on line 2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2095-2095)
  on line 2098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2098-2098)
  on line 2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2101-2101)
  on line 2104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2104-2104)
  on line 2107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2107-2107)
  on lines 2120..2122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2120-2122)
  on lines 2124..2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2124-2125)
  on lines 2127..2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2127-2128)
  on lines 2130..2131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2130-2131)
  on lines 2133..2134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2133-2134)
  on lines 2136..2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2136-2137)
  on lines 2147..2149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2147-2149)
  on lines 2151..2152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2151-2152)
  on lines 2154..2155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2154-2155)
  on lines 2157..2158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2157-2158)
  on lines 2160..2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2160-2161)
  on lines 2163..2164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2163-2164)
  on lines 2174..2176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2174-2176)
  on lines 2178..2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2178-2179)
  on lines 2181..2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2181-2182)
  on lines 2184..2185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2184-2185)
  on lines 2187..2188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2187-2188)
  on lines 2190..2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2190-2191)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:142-142)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1652-1652)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 1821..1823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1821-1823)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:505-505)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 1887..1889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1887-1889)
  on lines 1891..1893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1891-1893)
  on lines 1895..1897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1895-1897)
  on lines 1899..1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1899-1901)
  on lines 1903..1905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1903-1905)
  on lines 1907..1909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1907-1909)
  on lines 1952..1955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1952-1955)
  on lines 1957..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1957-1959)
  on lines 1961..1963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1961-1963)
  on lines 1965..1967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1965-1967)
  on lines 1969..1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1969-1971)
  on lines 1973..1975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1973-1975)
  on lines 1985..1988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1985-1988)
  on lines 1990..1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1990-1992)
  on lines 1994..1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1994-1996)
  on lines 1998..2000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1998-2000)
  on lines 2002..2004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2002-2004)
  on lines 2006..2008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2006-2008)
  on lines 2018..2021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2018-2021)
  on lines 2023..2025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2023-2025)
  on lines 2027..2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2027-2029)
  on lines 2031..2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2031-2033)
  on lines 2035..2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2035-2037)
  on lines 2039..2041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2039-2041)
  on lines 2057..2059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2057-2059)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 2370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2370-2370)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 2854..2856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2854-2856)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:263-263)
  on line 266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:266-266)
  on line 269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:269-269)
  on lines 274..275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:274-275)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1044..1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1044-1047)
  on lines 1057..1060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1057-1060)
  on lines 1070..1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1070-1073)
  on lines 1083..1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1083-1086)
  on lines 1096..1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1096-1099)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 2218..2219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2218-2219)
  on lines 2221..2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2221-2222)
  on lines 2224..2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2224-2225)
  on lines 2227..2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2227-2228)
  on lines 2230..2231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2230-2231)
  on lines 2233..2234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2233-2234)
  on line 2246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2246-2246)
  on line 2249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2249-2249)
  on line 2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2252-2252)
  on line 2255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2255-2255)
  on line 2258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2258-2258)
  on lines 2271..2273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2271-2273)
  on lines 2275..2276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2275-2276)
  on lines 2278..2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2278-2279)
  on lines 2281..2282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2281-2282)
  on lines 2284..2285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2284-2285)
  on lines 2287..2288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2287-2288)
  on lines 2298..2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2298-2300)
  on lines 2302..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2302-2303)
  on lines 2305..2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2305-2306)
  on lines 2308..2309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2308-2309)
  on lines 2311..2312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2311-2312)
  on lines 2314..2315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2314-2315)
  on lines 2325..2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2325-2327)
  on lines 2329..2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2329-2330)
  on lines 2332..2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2332-2333)
  on lines 2335..2336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2335-2336)
  on lines 2338..2339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2338-2339)
  on lines 2341..2342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2341-2342)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1831-1831)
  on lines 1836..1837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1836-1837)
  on lines 1839..1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1839-1840)
  on lines 1842..1843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1842-1843)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:291-291)
  on lines 296..297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:296-297)
  on lines 299..300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:299-300)
  on lines 302..303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:302-303)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2833-2833)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:990-990)
  on line 992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:992-992)
  on line 994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:994-994)
  on line 996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:996-996)
  on lines 998..999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:998-999)
  on line 1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1007-1007)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 969..970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:969-970)
  on line 976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:976-976)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 873..876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:873-876)
  on line 878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:878-878)
  on line 886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:886-886)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on lines 528..529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:528-529)
  on line 534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:534-534)
  on line 536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:536-536)
  on lines 538..540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:538-540)
  on lines 550..553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:550-553)
  on lines 578..582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:578-582)
  on lines 591..592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:591-592)
  on line 594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:594-594)
  on lines 596..598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:596-598)
  on lines 607..611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:607-611)
  on lines 620..621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:620-621)
  on line 623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:623-623)
  on lines 625..627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:625-627)
  on lines 636..640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:636-640)
  on lines 649..650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:649-650)
  on line 652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:652-652)
  on lines 654..656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:654-656)
  on lines 665..669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:665-669)
  on lines 671..672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:671-672)
  on lines 675..676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:675-676)
  on lines 679..680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:679-680)
  on lines 692..694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:692-694)
  on lines 698..699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:698-699)
  on line 701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:701-701)
  on lines 703..705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:703-705)
  on lines 714..718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:714-718)
  on lines 727..728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:727-728)
  on line 730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:730-730)
  on lines 732..734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:732-734)
  on lines 743..747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:743-747)
  on lines 756..757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:756-757)
  on line 759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:759-759)
  on lines 761..763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:761-763)
  on lines 772..776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:772-776)
  on lines 785..786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:785-786)
  on line 788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:788-788)
  on lines 790..792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:790-792)
  on lines 801..805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:801-805)
  on lines 814..815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:814-815)
  on line 817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:817-817)
  on lines 819..821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:819-821)
  on lines 830..834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:830-834)
  on lines 836..837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:836-837)
  on lines 840..841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:840-841)
  on lines 844..845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:844-845)
  on line 857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:857-857)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1144-1144)
  on line 1146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1146-1146)
  on line 1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1148-1148)
  on line 1158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1158-1158)
  on line 1160 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1160-1160)
  on line 1162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1162-1162)
  on line 1172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1172-1172)
  on line 1174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1174-1174)
  on line 1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1176-1176)
  on line 1186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1186-1186)
  on line 1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1188-1188)
  on line 1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1190-1190)
  on line 1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1200-1200)
  on line 1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1202-1202)
  on line 1204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1204-1204)
  on line 1214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1214-1214)
  on line 1216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1216-1216)
  on line 1218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1218-1218)
  on lines 1245..1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1245-1246)
  on line 1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1248-1248)
  on lines 1250..1251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1250-1251)
  on line 1255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1255-1255)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1699-1699)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 327
  dead: 1094 (567 in uncalled functions)
  total lines: 1421
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:431:9-431:23)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3391:9-3391:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3392:11-3392:30)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1094:7-1094:14)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:871:7-871:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:442:13-442:27)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3406:11-3406:21)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1107:7-1107:15)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:449:15-449:22)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3421:13-3421:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:453:17-453:31)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2393:7-2393:18)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1142:9-1142:18)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:460:19-460:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:262:7-262:19)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2397:9-2397:20)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3436:15-3436:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:265:9-265:21)
[Warning][Deadcode][CWE-571] condition 'floorButtons_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:464:21-464:35)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2401:11-2401:22)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1156:9-1156:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:268:11-268:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1811:15-1811:27)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2405:13-2405:24)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:271:13-271:25)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3463:7-3463:26)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1170:9-1170:18)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2409:15-2409:26)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3468:9-3468:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1830:7-1830:19)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:928:7-928:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:290:7-290:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2413:17-2413:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3473:11-3473:30)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1184:9-1184:18)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2217:7-2217:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1833:9-1833:21)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:932:9-932:12)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:293:9-293:21)
[Warning][Deadcode][CWE-571] condition 'floorButtons_spc2_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3478:13-3478:32)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2651:10-2651:11)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1198:9-1198:18)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2432:7-2432:18)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:944:7-944:26)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2655:9-2655:23)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:523:7-523:15)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2436:9-2436:20)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2659:11-2659:23)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1212:9-1212:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:527:9-527:12)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1858:7-1858:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2440:11-2440:22)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:533:9-533:27)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2671:9-2671:12)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1861:9-1861:21)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2444:13-2444:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2244:9-2244:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2245:11-2245:22)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1231:9-1231:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:968:9-968:12)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:336:7-336:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2448:15-2448:26)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2651:10-2651:11)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2248:13-2248:24)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1239:9-1239:16)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:549:11-549:29)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2452:17-2452:28)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2251:15-2251:26)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2655:9-2655:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2254:17-2254:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1886:7-1886:17)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2659:11-2659:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2066:7-2066:17)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:988:7-988:10)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2257:19-2257:30)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:562:13-562:31)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2471:7-2471:18)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:563:15-563:32)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2671:9-2671:12)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2260:21-2260:32)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:567:17-567:24)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2475:9-2475:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2651:10-2651:11)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2479:11-2479:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2655:9-2655:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2483:13-2483:24)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:149:7-149:13)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2659:11-2659:23)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2093:9-2093:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2487:15-2487:26)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2094:11-2094:22)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:152:9-152:15)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2097:13-2097:24)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:155:11-155:17)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2491:17-2491:28)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1919:9-1919:19)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1042:7-1042:14)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2100:15-2100:26)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:158:13-158:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3338:7-3338:17)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2103:17-2103:28)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:161:15-161:21)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3341:9-3341:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2106:19-2106:30)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:164:17-164:23)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1055:7-1055:14)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3344:11-3344:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2846:7-2846:10)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:2109:21-2109:32)
[Warning][Deadcode][CWE-571] condition 'floor == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3347:13-3347:23)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1068:7-1068:14)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1940:21-1940:32)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:3376:7-3376:17)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:1081:7-1081:14)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product28.cil.c:427:7-427:14)
[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)
