./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_product20.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_product20.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_product20.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_product20.cil.c:1655:5-1713:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1730:9-1788:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1911:3-1932:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1968:3-1993:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2053:5-2073:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2934:3-2953:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2981:3-3000:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3150:3-3178:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3210:3-3253:3 with factor 1
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:272:1-294:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:295:1-317:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:371:1-402:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:403:1-414:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:527:1-535:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:536:1-575:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1050:1-1083:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1171:1-1184:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1452:1-1622:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1623:1-1644:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1645:1-1803:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1815:1-1823:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1840:1-1885:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1886:1-1941:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1942:1-2001:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2004:1-2106:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2107:1-2152:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2153:1-2198:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2237:1-2278:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2880:1-2889:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2916:1-2958:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2959:1-3005:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3008:1-3059:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3060:1-3070:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3071:1-3081:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3082:1-3092:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3093:1-3103:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3104:1-3114:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3126:1-3137:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3184:1-3261:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3262:1-3273:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3274:1-3285:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3286:1-3296:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3297:1-3313:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1830-1830)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__2' has dead code:
  on line 78 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:78-78)
  on line 81 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:81-81)
  on line 84 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:84-84)
  on lines 89..90 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:89-90)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__3' has dead code:
  on line 116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:116-116)
  on line 118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:118-118)
  on lines 120..121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:120-121)
  on line 133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:133-133)
  on lines 135..136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:135-136)
  on line 146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:146-146)
  on line 148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:148-148)
  on lines 150..151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:150-151)
  on line 161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:161-161)
  on line 163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:163-163)
  on lines 165..166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:165-166)
  on line 176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:176-176)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:178-178)
  on lines 180..181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:180-181)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__4' has dead code:
  on line 204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:204-204)
  on line 209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:209-209)
  on line 214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:214-214)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:222-222)
  on line 224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:224-224)
  on line 233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:233-233)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 589..590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:589-590)
  on lines 593..594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:593-594)
  on lines 604..605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:604-605)
  on lines 611..612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:611-612)
  on lines 615..616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:615-616)
  on lines 622..623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:622-623)
  on line 630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:630-630)
  on lines 632..634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:632-634)
  on lines 636..638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:636-638)
  on lines 651..653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:651-653)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:490-490)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 501..503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:501-503)
  on lines 505..507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:505-507)
  on lines 509..511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:509-511)
  on lines 513..515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:513-515)
  on lines 517..518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:517-518)
  on line 524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:524-524)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2347-2347)
  on lines 2352..2353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2352-2353)
  on lines 2355..2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2355-2356)
  on lines 2358..2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2358-2359)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 3171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3171-3171)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1094-1094)
  on lines 1099..1100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1099-1100)
  on line 1108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1108-1108)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:332-332)
  on line 335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:335-335)
  on line 338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:338-338)
  on line 341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:341-341)
  on line 344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:344-344)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:481-481)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 3440..3441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3440-3441)
  on lines 3444..3445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3444-3445)
  on lines 3448..3449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3448-3449)
  on lines 3452..3453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3452-3453)
  on lines 3456..3457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3456-3457)
  on lines 3463..3464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3463-3464)
  on line 3471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3471-3471)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 3401..3402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3401-3402)
  on lines 3405..3406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3405-3406)
  on lines 3409..3410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3409-3410)
  on lines 3413..3414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3413-3414)
  on lines 3417..3418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3417-3418)
  on lines 3424..3425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3424-3425)
  on line 3432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3432-3432)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 3362..3363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3362-3363)
  on lines 3366..3367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3366-3367)
  on lines 3370..3371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3370-3371)
  on lines 3374..3375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3374-3375)
  on lines 3378..3379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3378-3379)
  on lines 3385..3386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3385-3386)
  on line 3393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3393-3393)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 2555..2556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2555-2556)
  on lines 2558..2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2558-2559)
  on lines 2561..2562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2561-2562)
  on lines 2564..2565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2564-2565)
  on lines 2567..2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2567-2568)
  on lines 2570..2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2570-2571)
  on line 2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2583-2583)
  on line 2586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2586-2586)
  on line 2589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2589-2589)
  on line 2592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2592-2592)
  on line 2595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2595-2595)
  on lines 2608..2610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2608-2610)
  on lines 2612..2613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2612-2613)
  on lines 2615..2616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2615-2616)
  on lines 2618..2619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2618-2619)
  on lines 2621..2622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2621-2622)
  on lines 2624..2625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2624-2625)
  on lines 2635..2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2635-2637)
  on lines 2639..2640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2639-2640)
  on lines 2642..2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2642-2643)
  on lines 2645..2646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2645-2646)
  on lines 2648..2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2648-2649)
  on lines 2651..2652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2651-2652)
  on lines 2662..2664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2662-2664)
  on lines 2666..2667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2666-2667)
  on lines 2669..2670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2669-2670)
  on lines 2672..2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2672-2673)
  on lines 2675..2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2675-2676)
  on lines 2678..2679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2678-2679)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:324-324)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1812-1812)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2309..2311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2309-2311)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:666-666)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2375..2377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2375-2377)
  on lines 2379..2381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2379-2381)
  on lines 2383..2385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2383-2385)
  on lines 2387..2389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2387-2389)
  on lines 2391..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2391-2393)
  on lines 2395..2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2395-2397)
  on lines 2440..2443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2440-2443)
  on lines 2445..2447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2445-2447)
  on lines 2449..2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2449-2451)
  on lines 2453..2455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2453-2455)
  on lines 2457..2459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2457-2459)
  on lines 2461..2463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2461-2463)
  on lines 2473..2476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2473-2476)
  on lines 2478..2480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2478-2480)
  on lines 2482..2484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2482-2484)
  on lines 2486..2488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2486-2488)
  on lines 2490..2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2490-2492)
  on lines 2494..2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2494-2496)
  on lines 2506..2509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2506-2509)
  on lines 2511..2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2511-2513)
  on lines 2515..2517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2515-2517)
  on lines 2519..2521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2519-2521)
  on lines 2523..2525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2523-2525)
  on lines 2527..2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2527-2529)
  on lines 2545..2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2545-2547)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 2858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2858-2858)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 3351..3353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3351-3353)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:424-424)
  on line 427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:427-427)
  on line 430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:430-430)
  on lines 435..436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:435-436)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1205..1208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1205-1208)
  on lines 1218..1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1218-1221)
  on lines 1231..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1231-1234)
  on lines 1244..1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1244-1247)
  on lines 1257..1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1257-1260)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 2706..2707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2706-2707)
  on lines 2709..2710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2709-2710)
  on lines 2712..2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2712-2713)
  on lines 2715..2716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2715-2716)
  on lines 2718..2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2718-2719)
  on lines 2721..2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2721-2722)
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2734-2734)
  on line 2737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2737-2737)
  on line 2740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2740-2740)
  on line 2743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2743-2743)
  on line 2746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2746-2746)
  on lines 2759..2761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2759-2761)
  on lines 2763..2764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2763-2764)
  on lines 2766..2767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2766-2767)
  on lines 2769..2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2769-2770)
  on lines 2772..2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2772-2773)
  on lines 2775..2776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2775-2776)
  on lines 2786..2788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2786-2788)
  on lines 2790..2791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2790-2791)
  on lines 2793..2794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2793-2794)
  on lines 2796..2797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2796-2797)
  on lines 2799..2800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2799-2800)
  on lines 2802..2803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2802-2803)
  on lines 2813..2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2813-2815)
  on lines 2817..2818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2817-2818)
  on lines 2820..2821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2820-2821)
  on lines 2823..2824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2823-2824)
  on lines 2826..2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2826-2827)
  on lines 2829..2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2829-2830)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2319-2319)
  on lines 2324..2325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2324-2325)
  on lines 2327..2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2327-2328)
  on lines 2330..2331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2330-2331)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:452-452)
  on lines 457..458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:457-458)
  on lines 460..461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:460-461)
  on lines 463..464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:463-464)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 3330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3330-3330)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 1151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1151-1151)
  on line 1153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1153-1153)
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1155-1155)
  on line 1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1157-1157)
  on lines 1159..1160 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1159-1160)
  on line 1168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1168-1168)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__weight' has dead code:
  on lines 1130..1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1130-1131)
  on line 1137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1137-1137)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 1034..1037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1034-1037)
  on line 1039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1039-1039)
  on line 1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1047-1047)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__weight' has dead code:
  on lines 689..690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:689-690)
  on line 695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:695-695)
  on line 697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:697-697)
  on lines 699..701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:699-701)
  on lines 711..714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:711-714)
  on lines 739..743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:739-743)
  on lines 752..753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:752-753)
  on line 755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:755-755)
  on lines 757..759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:757-759)
  on lines 768..772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:768-772)
  on lines 781..782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:781-782)
  on line 784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:784-784)
  on lines 786..788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:786-788)
  on lines 797..801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:797-801)
  on lines 810..811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:810-811)
  on line 813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:813-813)
  on lines 815..817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:815-817)
  on lines 826..830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:826-830)
  on lines 832..833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:832-833)
  on lines 836..837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:836-837)
  on lines 840..841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:840-841)
  on lines 853..855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:853-855)
  on lines 859..860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:859-860)
  on line 862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:862-862)
  on lines 864..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:864-866)
  on lines 875..879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:875-879)
  on lines 888..889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:888-889)
  on line 891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:891-891)
  on lines 893..895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:893-895)
  on lines 904..908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:904-908)
  on lines 917..918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:917-918)
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:920-920)
  on lines 922..924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:922-924)
  on lines 933..937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:933-937)
  on lines 946..947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:946-947)
  on line 949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:949-949)
  on lines 951..953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:951-953)
  on lines 962..966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:962-966)
  on lines 975..976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:975-976)
  on line 978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:978-978)
  on lines 980..982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:980-982)
  on lines 991..995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:991-995)
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:997-998)
  on lines 1001..1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1001-1002)
  on lines 1005..1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1005-1006)
  on line 1018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1018-1018)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1305-1305)
  on line 1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1307-1307)
  on line 1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1309-1309)
  on line 1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1319-1319)
  on line 1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1321-1321)
  on line 1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1323-1323)
  on line 1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1333-1333)
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1335-1335)
  on line 1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1337-1337)
  on line 1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1347-1347)
  on line 1349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1349-1349)
  on line 1351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1351-1351)
  on line 1361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1361-1361)
  on line 1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1363-1363)
  on line 1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1365-1365)
  on line 1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1375-1375)
  on line 1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1377-1377)
  on line 1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1379-1379)
  on lines 1406..1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1406-1407)
  on line 1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1409-1409)
  on lines 1411..1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1411-1412)
  on line 1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1416-1416)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2910-2910)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 327
  dead: 1085 (558 in uncalled functions)
  total lines: 1412
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:684:7-684:15)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:207:9-207:28)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3416:15-3416:26)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1373:9-1373:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:688:9-688:12)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:212:11-212:30)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3420:17-3420:28)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:694:9-694:27)
[Warning][Deadcode][CWE-571] condition 'floorButtons_spc2_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:217:13-217:32)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2318:7-2318:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2705:7-2705:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2321:9-2321:21)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1392:9-1392:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1129:9-1129:12)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:497:7-497:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3439:7-3439:18)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1400:9-1400:16)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:710:11-710:29)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3443:9-3443: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_product20.cil.c:3150:10-3150:11)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3447:11-3447:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3154:9-3154:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1149:7-1149:10)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2346:7-2346:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:723:13-723:31)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3158:11-3158:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3451:13-3451:24)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:724:15-724:32)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2349:9-2349:21)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:728:17-728:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2732:9-2732:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3455:15-3455:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3170:9-3170:12)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2733:11-2733:22)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2736:13-2736:24)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3459:17-3459:28)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2739:15-2739: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_product20.cil.c:3150:10-3150:11)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2742:17-2742:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2374:7-2374:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2554:7-2554:17)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3154:9-3154:23)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2745:19-2745:30)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3158:11-3158:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2748:21-2748:32)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1203:7-1203:14)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3170:9-3170:12)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:331:7-331:13)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:334:9-334:15)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1216:7-1216:14)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3150:10-3150:11)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:337:11-337:17)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:340:13-340:19)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2581:9-2581:19)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3154:9-3154:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2582:11-2582:22)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:343:15-343:21)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1229:7-1229:14)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3158:11-3158:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:77:7-77:17)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2585:13-2585:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2407:9-2407:19)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:346:17-346:23)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:80:9-80:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2588:15-2588:26)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:83:11-83:21)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2591:17-2591:28)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1242:7-1242:14)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:588:7-588:14)
[Warning][Deadcode][CWE-571] condition 'floor == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:86:13-86:23)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2594:19-2594:30)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:592:9-592:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2597:21-2597:32)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3343:7-3343:10)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1255:7-1255:14)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1032:7-1032:14)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:115:7-115:17)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:603:13-603:27)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2428:21-2428:32)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3361:7-3361:18)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1268:7-1268:15)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3365:9-3365:20)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:610:15-610:22)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:130:9-130:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:131:11-131:30)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3369:11-3369:22)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:614:17-614:31)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3373:13-3373:24)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:145:11-145:21)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1303:9-1303:18)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:621:19-621:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:423:7-423:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3377:15-3377:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:426:9-426:21)
[Warning][Deadcode][CWE-571] condition 'floorButtons_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:625:21-625:35)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3381:17-3381:28)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1317:9-1317:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:429:11-429:23)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:160:13-160:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:432:13-432:25)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1331:9-1331:18)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3400:7-3400:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:451:7-451:19)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1089:7-1089:26)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3404:9-3404:20)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:175:15-175:25)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1345:9-1345:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:454:9-454:21)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1093:9-1093:12)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3408:11-3408:22)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1359:9-1359:18)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:3412:13-3412:24)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:202:7-202:26)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:1105:7-1105:26)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product20.cil.c:2299:15-2299:27)
[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)
