./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_spec1_product24.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/elevator_spec1_product24.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:268:5-288:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:573:3-601:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:635:3-678:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2938:5-2996:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3013:9-3071:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3126:3-3145:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3173:3-3192: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:426:1-477:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:480:1-490:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:491:1-501:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:513:1-523:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:524:1-534:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:547:1-558:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:609:1-686:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:687:1-698:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:699:1-710:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:711:1-721:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:722:1-738:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:830:1-871:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1490:1-1512:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1513:1-1535:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1589:1-1620:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1621:1-1632:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1741:1-1749:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1750:1-1789:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2453:1-2466:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2735:1-2905:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2906:1-2927:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2928:1-3086:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3098:1-3106:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3108:1-3150:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3151:1-3197:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3512:1-3521:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:420-420)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__2' has dead code:
  on line 3221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3221-3221)
  on lines 3229..3230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3229-3230)
  on lines 3232..3233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3232-3233)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__3' has dead code:
  on line 3259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3259-3259)
  on line 3261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3261-3261)
  on lines 3263..3264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3263-3264)
  on line 3289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3289-3289)
  on line 3291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3291-3291)
  on lines 3293..3294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3293-3294)
  on line 3304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3304-3304)
  on line 3306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3306-3306)
  on lines 3308..3309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3308-3309)
  on line 3319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3319-3319)
  on line 3321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3321-3321)
  on lines 3323..3324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3323-3324)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__4' has dead code:
  on line 3347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3347-3347)
  on line 3352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3352-3352)
  on line 3360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3360-3360)
  on line 3362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3362-3362)
  on line 3365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3365-3365)
  on line 3367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3367-3367)
  on line 3376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3376-3376)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 1803..1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1803-1804)
  on lines 1807..1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1807-1808)
  on lines 1818..1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1818-1819)
  on lines 1828..1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1828-1830)
  on line 1833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1833-1833)
  on lines 1835..1837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1835-1837)
  on lines 1839..1841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1839-1841)
  on line 1844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1844-1844)
  on lines 1846..1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1846-1848)
  on lines 1850..1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1850-1852)
  on lines 1865..1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1865-1867)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1704-1704)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1715..1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1715-1717)
  on lines 1719..1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1719-1721)
  on lines 1723..1725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1723-1725)
  on lines 1727..1729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1727-1729)
  on lines 1731..1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1731-1732)
  on line 1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1738-1738)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:945-945)
  on lines 953..954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:953-954)
  on lines 956..957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:956-957)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:594-594)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 2348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2348-2348)
  on lines 2353..2354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2353-2354)
  on line 2362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2362-2362)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 1550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1550-1550)
  on line 1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1553-1553)
  on line 1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1556-1556)
  on line 1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1559-1559)
  on line 1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1562-1562)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1695-1695)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 3476..3477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3476-3477)
  on lines 3480..3481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3480-3481)
  on lines 3484..3485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3484-3485)
  on lines 3488..3489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3488-3489)
  on lines 3492..3493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3492-3493)
  on lines 3499..3500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3499-3500)
  on line 3507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3507-3507)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 3437..3438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3437-3438)
  on lines 3441..3442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3441-3442)
  on lines 3449..3450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3449-3450)
  on lines 3453..3454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3453-3454)
  on lines 3460..3461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3460-3461)
  on line 3468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3468-3468)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 3398..3399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3398-3399)
  on lines 3402..3403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3402-3403)
  on lines 3406..3407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3406-3407)
  on lines 3410..3411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3410-3411)
  on lines 3414..3415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3414-3415)
  on lines 3421..3422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3421-3422)
  on line 3429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3429-3429)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 1153..1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1153-1154)
  on lines 1156..1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1156-1157)
  on lines 1159..1160 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1159-1160)
  on lines 1162..1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1162-1163)
  on lines 1165..1166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1165-1166)
  on lines 1168..1169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1168-1169)
  on line 1181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1181-1181)
  on line 1184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1184-1184)
  on line 1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1187-1187)
  on line 1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1190-1190)
  on line 1193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1193-1193)
  on line 1208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1208-1208)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1211-1211)
  on lines 1216..1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1216-1217)
  on lines 1219..1220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1219-1220)
  on lines 1222..1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1222-1223)
  on lines 1233..1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1233-1235)
  on lines 1237..1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1237-1238)
  on lines 1240..1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1240-1241)
  on lines 1243..1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1243-1244)
  on lines 1246..1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1246-1247)
  on lines 1249..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1249-1250)
  on lines 1260..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1260-1262)
  on lines 1264..1265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1264-1265)
  on lines 1267..1268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1267-1268)
  on lines 1270..1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1270-1271)
  on lines 1273..1274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1273-1274)
  on lines 1276..1277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1276-1277)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2309..2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2309-2310)
  on lines 2313..2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2313-2314)
  on lines 2317..2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2317-2318)
  on lines 2321..2322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2321-2322)
  on lines 2325..2326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2325-2326)
  on line 2335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2335-2335)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1542-1542)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 3095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3095-3095)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 889..890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:889-890)
  on lines 902..904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:902-904)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1880-1880)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 973..975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:973-975)
  on lines 977..979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:977-979)
  on lines 981..983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:981-983)
  on lines 985..987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:985-987)
  on lines 989..991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:989-991)
  on lines 993..995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:993-995)
  on lines 1038..1041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1038-1041)
  on lines 1043..1045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1043-1045)
  on lines 1047..1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1047-1049)
  on lines 1051..1053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1051-1053)
  on lines 1055..1057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1055-1057)
  on lines 1059..1061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1059-1061)
  on lines 1071..1074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1071-1074)
  on lines 1076..1078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1076-1078)
  on lines 1080..1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1080-1082)
  on lines 1084..1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1084-1086)
  on lines 1088..1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1088-1090)
  on lines 1092..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1092-1094)
  on lines 1104..1107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1104-1107)
  on lines 1109..1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1109-1111)
  on lines 1113..1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1113-1115)
  on lines 1117..1119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1117-1119)
  on lines 1121..1123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1121-1123)
  on lines 1125..1127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1125-1127)
  on lines 1143..1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1143-1145)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1456-1456)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 782..784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:782-784)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1638-1638)
  on line 1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1641-1641)
  on line 1644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1644-1644)
  on lines 1649..1650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1649-1650)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2487..2490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2487-2490)
  on lines 2500..2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2500-2503)
  on lines 2513..2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2513-2516)
  on lines 2526..2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2526-2529)
  on lines 2539..2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2539-2542)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 1304..1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1304-1305)
  on lines 1307..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1307-1308)
  on lines 1310..1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1310-1311)
  on lines 1313..1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1313-1314)
  on lines 1316..1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1316-1317)
  on lines 1319..1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1319-1320)
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1332-1332)
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1335-1335)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1338-1338)
  on line 1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1341-1341)
  on line 1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1344-1344)
  on lines 1357..1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1357-1359)
  on lines 1361..1362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1361-1362)
  on lines 1364..1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1364-1365)
  on lines 1367..1368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1367-1368)
  on lines 1370..1371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1370-1371)
  on lines 1373..1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1373-1374)
  on lines 1384..1386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1384-1386)
  on lines 1388..1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1388-1389)
  on lines 1391..1392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1391-1392)
  on lines 1394..1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1394-1395)
  on lines 1397..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1397-1398)
  on lines 1400..1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1400-1401)
  on lines 1411..1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1411-1413)
  on lines 1415..1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1415-1416)
  on lines 1418..1419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1418-1419)
  on lines 1421..1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1421-1422)
  on lines 1424..1425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1424-1425)
  on lines 1427..1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1427-1428)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:912-912)
  on lines 917..918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:917-918)
  on lines 920..921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:920-921)
  on lines 923..924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:923-924)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1666-1666)
  on lines 1671..1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1671-1672)
  on lines 1674..1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1674-1675)
  on lines 1677..1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1677-1678)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:758-758)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 2433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2433-2433)
  on line 2435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2435-2435)
  on line 2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2437-2437)
  on line 2439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2439-2439)
  on lines 2441..2442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2441-2442)
  on line 2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2450-2450)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__twothirdsfull' has dead code:
  on lines 2407..2409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2407-2409)
  on line 2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2411-2411)
  on line 2419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2419-2419)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__weight' has dead code:
  on lines 2384..2385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2384-2385)
  on line 2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2391-2391)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 2288..2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2288-2291)
  on line 2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2293-2293)
  on line 2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2301-2301)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__twothirdsfull' has dead code:
  on line 2253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2253-2253)
  on line 2255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2255-2255)
  on line 2257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2257-2257)
  on line 2260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2260-2260)
  on line 2263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2263-2263)
  on line 2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2272-2272)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__weight' has dead code:
  on lines 1903..1904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1903-1904)
  on line 1909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1909-1909)
  on line 1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1911-1911)
  on lines 1913..1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1913-1915)
  on lines 1925..1928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1925-1928)
  on lines 1953..1957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1953-1957)
  on lines 1966..1967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1966-1967)
  on line 1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1969-1969)
  on lines 1971..1973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1971-1973)
  on lines 1982..1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1982-1986)
  on lines 1995..1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1995-1996)
  on line 1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1998-1998)
  on lines 2000..2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2000-2002)
  on lines 2011..2015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2011-2015)
  on lines 2024..2025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2024-2025)
  on line 2027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2027-2027)
  on lines 2029..2031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2029-2031)
  on lines 2040..2044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2040-2044)
  on lines 2046..2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2046-2047)
  on lines 2050..2051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2050-2051)
  on lines 2054..2055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2054-2055)
  on lines 2067..2069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2067-2069)
  on lines 2073..2074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2073-2074)
  on line 2076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2076-2076)
  on lines 2078..2080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2078-2080)
  on lines 2089..2093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2089-2093)
  on lines 2102..2103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2102-2103)
  on line 2105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2105-2105)
  on lines 2107..2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2107-2109)
  on lines 2118..2122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2118-2122)
  on lines 2131..2132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2131-2132)
  on line 2134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2134-2134)
  on lines 2136..2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2136-2138)
  on lines 2147..2151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2147-2151)
  on lines 2160..2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2160-2161)
  on line 2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2163-2163)
  on lines 2165..2167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2165-2167)
  on lines 2176..2180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2176-2180)
  on lines 2189..2190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2189-2190)
  on line 2192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2192-2192)
  on lines 2194..2196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2194-2196)
  on lines 2205..2209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2205-2209)
  on lines 2211..2212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2211-2212)
  on lines 2215..2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2215-2216)
  on lines 2219..2220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2219-2220)
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2232-2232)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2587-2587)
  on line 2589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2589-2589)
  on line 2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2591-2591)
  on line 2601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2601-2601)
  on line 2603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2603-2603)
  on line 2605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2605-2605)
  on line 2615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2615-2615)
  on line 2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2617-2617)
  on line 2619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2619-2619)
  on line 2629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2629-2629)
  on line 2631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2631-2631)
  on line 2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2633-2633)
  on line 2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2643-2643)
  on line 2645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2645-2645)
  on line 2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2647-2647)
  on line 2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2657-2657)
  on line 2659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2659-2659)
  on line 2661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2661-2661)
  on lines 2688..2689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2688-2689)
  on line 2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2691-2691)
  on lines 2693..2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2693-2694)
  on line 2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2698-2698)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3542-3542)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 360
  dead: 1081 (537 in uncalled functions)
  total lines: 1441
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2585:9-2585:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1902:9-1902:12)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2343:7-2343:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1908:9-1908:27)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3436:7-3436:18)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2599:9-2599:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2347:9-2347:12)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3440:9-3440:20)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1711:7-1711:19)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2613:9-2613:18)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2359:7-2359:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1924:11-1924:29)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3448:13-3448:24)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2627:9-2627:18)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3452:15-3452:26)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3220:7-3220:17)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1937:13-1937:31)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:888:13-888:25)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1938:15-1938:32)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2641:9-2641:18)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3456:17-3456:28)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1942:17-1942:24)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:892:15-892:27)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2383:9-2383:12)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3226:11-3226:21)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2655:9-2655:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:573:10-573:11)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3475:7-3475:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:911:7-911:19)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:577:9-577:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:914:9-914:21)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3479:9-3479:20)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2405:7-2405:26)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2674:9-2674:23)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:581:11-581:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1303:7-1303:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3258:7-3258:17)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3483:11-3483:22)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2682:9-2682:16)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:593:9-593:12)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3487:13-3487:24)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3491:15-3491:26)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3273:9-3273:19)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2431:7-2431:10)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1549:7-1549:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:573:10-573:11)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1552:9-1552:15)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:944:7-944:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3495:17-3495:28)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:577:9-577:23)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1555:11-1555:17)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3288:11-3288:21)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:581:11-581:23)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1558:13-1558:19)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1330:9-1330:19)
[Warning][Deadcode][CWE-571] condition 'floorID == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:950:11-950:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1331:11-1331:22)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1561:15-1561:21)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1334:13-1334:24)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:593:9-593:12)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1564:17-1564:23)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1337:15-1337:26)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3303:13-3303:23)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1802:7-1802:14)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1340:17-1340:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:972:7-972:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1152:7-1152:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:573:10-573:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1806:9-1806:23)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1343:19-1343:30)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2485:7-2485:14)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:577:9-577:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1346:21-1346:32)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3318:15-3318:25)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:581:11-581:23)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2252:7-2252:15)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2498:7-2498:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1817:13-1817:27)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3345:7-3345:28)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3350:9-3350:30)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1824:15-1824:22)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2511:7-2511:14)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1180:11-1180:22)
[Warning][Deadcode][CWE-571] condition 'landingButtons_spc1_2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3355:11-3355:32)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:774:7-774:10)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1183:13-1183:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1005:9-1005:19)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2286:7-2286:14)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1186:15-1186:26)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2524:7-2524:14)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1637:7-1637:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1189:17-1189:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1640:9-1640:21)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1192:19-1192:30)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1643:11-1643:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1195:21-1195:32)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3397:7-3397:18)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2537:7-2537:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2308:7-2308:21)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1646:13-1646:25)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1206:11-1206:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1207:13-1207:24)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3401:9-3401:20)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2312:9-2312:23)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1210:15-1210:26)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3405:11-3405:22)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2550:7-2550:15)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2316:11-2316:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1665:7-1665:19)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1213:17-1213:28)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1026:21-1026:32)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1668:9-1668:21)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3409:13-3409:24)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2320:13-2320:27)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3413:15-3413:26)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:2324:15-2324:29)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:1898:7-1898:15)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product24.cil.c:3417:17-3417:28)
[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)
