./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_product22.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_product22.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_product22.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_product22.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:268:5-288:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1125:3-1144:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1172:3-1191:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1342:3-1370:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1402:3-1445:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3131:5-3189:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3206:9-3264:9 with factor 4
[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_product22.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_product22.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_product22.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_product22.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_product22.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_product22.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:458:1-499:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1107:1-1149:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1150:1-1196:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1199:1-1250:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1251:1-1261:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1262:1-1272:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1284:1-1294:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1295:1-1305:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1317:1-1328:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1376:1-1453:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1454:1-1465:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1466:1-1477:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1478:1-1488:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1489:1-1505:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1689:1-1698:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1744:1-1766:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1767:1-1789:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1843:1-1874:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1875:1-1886:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1995:1-2003:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2004:1-2043:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2646:1-2659:1)
[Warning][Deadcode] Function 'printState__wrappee__twothirdsfull' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2928:1-3098:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3099:1-3120:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3121:1-3279:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1093-1093)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__2' has dead code:
  on line 3303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3303-3303)
  on lines 3311..3312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3311-3312)
  on lines 3314..3315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3314-3315)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__3' has dead code:
  on line 3341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3341-3341)
  on line 3343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3343-3343)
  on lines 3345..3346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3345-3346)
  on line 3371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3371-3371)
  on line 3373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3373-3373)
  on lines 3375..3376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3375-3376)
  on line 3386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3386-3386)
  on line 3388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3388-3388)
  on lines 3390..3391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3390-3391)
  on line 3401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3401-3401)
  on line 3403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3403-3403)
  on lines 3405..3406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3405-3406)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__4' has dead code:
  on line 3429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3429-3429)
  on line 3434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3434-3434)
  on line 3442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3442-3442)
  on line 3444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3444-3444)
  on line 3447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3447-3447)
  on line 3449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3449-3449)
  on line 3458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3458-3458)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 2057..2058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2057-2058)
  on lines 2061..2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2061-2062)
  on lines 2072..2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2072-2073)
  on lines 2082..2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2082-2084)
  on line 2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2087-2087)
  on lines 2089..2091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2089-2091)
  on lines 2093..2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2093-2095)
  on line 2098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2098-2098)
  on lines 2100..2102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2100-2102)
  on lines 2104..2106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2104-2106)
  on lines 2119..2121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2119-2121)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1958-1958)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1969..1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1969-1971)
  on lines 1973..1975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1973-1975)
  on lines 1977..1979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1977-1979)
  on lines 1981..1983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1981-1983)
  on lines 1985..1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1985-1986)
  on line 1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1992-1992)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:573-573)
  on lines 581..582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:581-582)
  on lines 584..585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:584-585)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1363-1363)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2572-2572)
  on lines 2577..2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2577-2578)
  on line 2586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2586-2586)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1804-1804)
  on line 1807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1807-1807)
  on line 1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1810-1810)
  on line 1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1813-1813)
  on line 1816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1816-1816)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1949-1949)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 1653..1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1653-1654)
  on lines 1657..1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1657-1658)
  on lines 1661..1662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1661-1662)
  on lines 1665..1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1665-1666)
  on lines 1669..1670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1669-1670)
  on lines 1676..1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1676-1677)
  on line 1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1684-1684)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 1614..1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1614-1615)
  on lines 1618..1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1618-1619)
  on lines 1626..1627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1626-1627)
  on lines 1630..1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1630-1631)
  on lines 1637..1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1637-1638)
  on line 1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1645-1645)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 1575..1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1575-1576)
  on lines 1579..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1579-1580)
  on lines 1583..1584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1583-1584)
  on lines 1587..1588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1587-1588)
  on lines 1591..1592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1591-1592)
  on lines 1598..1599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1598-1599)
  on line 1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1606-1606)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 781..782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:781-782)
  on lines 784..785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:784-785)
  on lines 787..788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:787-788)
  on lines 790..791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:790-791)
  on lines 793..794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:793-794)
  on lines 796..797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:796-797)
  on line 809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:809-809)
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:812-812)
  on line 815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:815-815)
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:818-818)
  on line 821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:821-821)
  on line 836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:836-836)
  on line 839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:839-839)
  on lines 844..845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:844-845)
  on lines 847..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:847-848)
  on lines 850..851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:850-851)
  on lines 861..863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:861-863)
  on lines 865..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:865-866)
  on lines 868..869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:868-869)
  on lines 871..872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:871-872)
  on lines 874..875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:874-875)
  on lines 877..878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:877-878)
  on lines 888..890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:888-890)
  on lines 892..893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:892-893)
  on lines 895..896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:895-896)
  on lines 898..899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:898-899)
  on lines 901..902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:901-902)
  on lines 904..905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:904-905)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2533..2534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2533-2534)
  on lines 2537..2538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2537-2538)
  on lines 2541..2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2541-2542)
  on lines 2545..2546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2545-2546)
  on lines 2549..2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2549-2550)
  on line 2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2559-2559)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1796-1796)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 516..518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:516-518)
  on lines 520..522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:520-522)
  on lines 530..532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:530-532)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 2134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2134-2134)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 601..603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:601-603)
  on lines 605..607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:605-607)
  on lines 609..611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:609-611)
  on lines 613..615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:613-615)
  on lines 617..619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:617-619)
  on lines 621..623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:621-623)
  on lines 666..669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:666-669)
  on lines 671..673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:671-673)
  on lines 675..677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:675-677)
  on lines 679..681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:679-681)
  on lines 683..685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:683-685)
  on lines 687..689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:687-689)
  on lines 699..702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:699-702)
  on lines 704..706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:704-706)
  on lines 708..710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:708-710)
  on lines 712..714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:712-714)
  on lines 716..718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:716-718)
  on lines 720..722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:720-722)
  on lines 732..735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:732-735)
  on lines 737..739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:737-739)
  on lines 741..743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:741-743)
  on lines 745..747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:745-747)
  on lines 749..751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:749-751)
  on lines 753..755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:753-755)
  on lines 771..773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:771-773)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1084-1084)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 1549..1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1549-1551)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1892-1892)
  on line 1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1895-1895)
  on line 1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1898-1898)
  on lines 1903..1904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1903-1904)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2680..2683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2680-2683)
  on lines 2693..2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2693-2696)
  on lines 2706..2709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2706-2709)
  on lines 2719..2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2719-2722)
  on lines 2732..2735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2732-2735)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 932..933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:932-933)
  on lines 935..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:935-936)
  on lines 938..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:938-939)
  on lines 941..942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:941-942)
  on lines 944..945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:944-945)
  on lines 947..948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:947-948)
  on line 960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:960-960)
  on line 963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:963-963)
  on line 966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:966-966)
  on line 969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:969-969)
  on line 972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:972-972)
  on lines 985..987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:985-987)
  on lines 989..990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:989-990)
  on lines 992..993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:992-993)
  on lines 995..996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:995-996)
  on lines 998..999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:998-999)
  on lines 1001..1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1001-1002)
  on lines 1012..1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1012-1014)
  on lines 1016..1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1016-1017)
  on lines 1019..1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1019-1020)
  on lines 1022..1023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1022-1023)
  on lines 1025..1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1025-1026)
  on lines 1028..1029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1028-1029)
  on lines 1039..1041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1039-1041)
  on lines 1043..1044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1043-1044)
  on lines 1046..1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1046-1047)
  on lines 1049..1050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1049-1050)
  on lines 1052..1053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1052-1053)
  on lines 1055..1056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1055-1056)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:540-540)
  on lines 545..546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:545-546)
  on lines 548..549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:548-549)
  on lines 551..552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:551-552)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1920-1920)
  on lines 1925..1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1925-1926)
  on lines 1928..1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1928-1929)
  on lines 1931..1932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1931-1932)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 1525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1525-1525)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on lines 2631..2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2631-2633)
  on line 2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2635-2635)
  on line 2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2643-2643)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__weight' has dead code:
  on lines 2608..2609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2608-2609)
  on line 2615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2615-2615)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 2506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2506-2506)
  on line 2508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2508-2508)
  on line 2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2510-2510)
  on line 2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2513-2513)
  on line 2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2516-2516)
  on line 2525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2525-2525)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__weight' has dead code:
  on lines 2157..2158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2157-2158)
  on line 2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2163-2163)
  on line 2165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2165-2165)
  on lines 2167..2169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2167-2169)
  on lines 2179..2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2179-2182)
  on lines 2207..2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2207-2211)
  on lines 2220..2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2220-2221)
  on line 2223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2223-2223)
  on lines 2225..2227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2225-2227)
  on lines 2236..2240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2236-2240)
  on lines 2249..2250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2249-2250)
  on line 2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2252-2252)
  on lines 2254..2256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2254-2256)
  on lines 2265..2269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2265-2269)
  on lines 2278..2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2278-2279)
  on line 2281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2281-2281)
  on lines 2283..2285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2283-2285)
  on lines 2294..2298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2294-2298)
  on lines 2300..2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2300-2301)
  on lines 2304..2305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2304-2305)
  on lines 2308..2309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2308-2309)
  on lines 2321..2323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2321-2323)
  on lines 2327..2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2327-2328)
  on line 2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2330-2330)
  on lines 2332..2334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2332-2334)
  on lines 2343..2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2343-2347)
  on lines 2356..2357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2356-2357)
  on line 2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2359-2359)
  on lines 2361..2363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2361-2363)
  on lines 2372..2376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2372-2376)
  on lines 2385..2386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2385-2386)
  on line 2388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2388-2388)
  on lines 2390..2392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2390-2392)
  on lines 2401..2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2401-2405)
  on lines 2414..2415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2414-2415)
  on line 2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2417-2417)
  on lines 2419..2421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2419-2421)
  on lines 2430..2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2430-2434)
  on lines 2443..2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2443-2444)
  on line 2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2446-2446)
  on lines 2448..2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2448-2450)
  on lines 2459..2463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2459-2463)
  on lines 2465..2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2465-2466)
  on lines 2469..2470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2469-2470)
  on lines 2473..2474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2473-2474)
  on line 2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2486-2486)
[Warning][Deadcode] Function 'timeShift__wrappee__twothirdsfull' has dead code:
  on line 2780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2780-2780)
  on line 2782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2782-2782)
  on line 2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2784-2784)
  on line 2794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2794-2794)
  on line 2796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2796-2796)
  on line 2798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2798-2798)
  on line 2808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2808-2808)
  on line 2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2810-2810)
  on line 2812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2812-2812)
  on line 2822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2822-2822)
  on line 2824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2824-2824)
  on line 2826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2826-2826)
  on line 2836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2836-2836)
  on line 2838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2838-2838)
  on line 2840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2840-2840)
  on line 2850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2850-2850)
  on line 2852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2852-2852)
  on line 2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2854-2854)
  on lines 2881..2882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2881-2882)
  on line 2884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2884-2884)
  on lines 2886..2887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2886-2887)
  on line 2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2891-2891)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1719-1719)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 343
  dead: 1068 (534 in uncalled functions)
  total lines: 1411
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2505:7-2505:15)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2071:13-2071:27)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3385:13-3385:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:512:11-512:23)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2743:7-2743:15)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1625:13-1625:24)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2078:15-2078:22)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1629:15-1629:26)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3400:15-3400:25)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2532:7-2532:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1633:17-1633:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2536:9-2536:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1891:7-1891:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:539:7-539:19)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2778:9-2778:18)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3427:7-3427:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2540:11-2540:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1894:9-1894:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1342:10-1342:11)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:542:9-542:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1652:7-1652:18)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3432:9-3432:30)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1897:11-1897:23)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2792:9-2792:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2544:13-2544:27)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1346:9-1346:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:931:7-931:17)
[Warning][Deadcode][CWE-571] condition 'landingButtons_spc1_2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3437:11-3437:32)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1656:9-1656:20)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1900:13-1900:25)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1350:11-1350:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2548:15-2548:29)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1660:11-1660:22)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2806:9-2806:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1362:9-1362:12)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1919:7-1919:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1664:13-1664:24)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2820:9-2820:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1922:9-1922:21)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:572:7-572:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1668:15-1668:26)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2567:7-2567:26)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1342:10-1342:11)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2571:9-2571:12)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1672:17-1672:28)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2834:9-2834:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:578:11-578:23)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1346:9-1346:23)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:958:9-958:19)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2152:7-2152:15)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:959:11-959:22)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1350:11-1350:23)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2583:7-2583:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2156:9-2156:12)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:962:13-962:24)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2848:9-2848:18)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:965:15-965:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2162:9-2162:27)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1362:9-1362:12)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:600:7-600:17)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:968:17-968:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:780:7-780:17)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:971:19-971:30)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2867:9-2867:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1965:7-1965:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1342:10-1342:11)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:974:21-974:32)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2607:9-2607:12)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2178:11-2178:29)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2875:9-2875:16)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1346:9-1346:23)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1350:11-1350:23)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2191:13-2191:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2192:15-2192:32)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2629:7-2629:26)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2196:17-2196:24)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:808:11-808:22)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:811:13-811:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:633:9-633:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:814:15-814:26)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1541:7-1541:10)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:817:17-817:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3302:7-3302:17)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:820:19-820:30)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:823:21-823:32)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3308:11-3308:21)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:834:11-834:21)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2678:7-2678:14)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:835:13-835:24)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1574:7-1574:18)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:838:15-838:26)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1803:7-1803:13)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1578:9-1578:20)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:841:17-841:28)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:654:21-654:32)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2691:7-2691:14)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1806:9-1806:15)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1582:11-1582:22)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3340:7-3340:17)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1809:11-1809:17)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1586:13-1586:24)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1812:13-1812:19)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2704:7-2704:14)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1815:15-1815:21)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1590:15-1590:26)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3355:9-3355:19)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1818:17-1818:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1594:17-1594:28)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2056:7-2056:14)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2717:7-2717:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2060:9-2060:23)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:3370:11-3370:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1613:7-1613:18)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:2730:7-2730:14)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product22.cil.c:1617:9-1617:20)
[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)
