./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_spec3_product27.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_spec3_product27.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_spec3_product27.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_spec3_product27.cil.c:1444:5-1502:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1519:9-1577:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1635:3-1654:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1682:3-1701:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2174:3-2202:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2234:3-2277:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3155:3-3176:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3212:3-3237:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3297:5-3317:5 with factor 2
[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 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:112:1-134:1)
[Warning][Deadcode] Function 'isBlocked' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:135:1-143:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:188:1-219:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:220:1-231:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:232:1-251:1)
[Warning][Deadcode] Function 'areDoorsOpen' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:317:1-325:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:369:1-408:1)
[Warning][Deadcode] Function 'anyStopRequested' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:409:1-488:1)
[Warning][Deadcode] Function 'isIdle' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:489:1-501:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:883:1-916:1)
[Warning][Deadcode] Function 'printState' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1263:1-1433:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1434:1-1592:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1604:1-1612:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1617:1-1659:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1660:1-1706:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2032:1-2083:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2095:1-2105:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2106:1-2116:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2117:1-2127:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2128:1-2138:1)
[Warning][Deadcode] Function 'bigMacCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2139:1-2149:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2208:1-2285:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2286:1-2297:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2298:1-2309:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2310:1-2320:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2321:1-2337:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3044:1-3053:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3084:1-3129:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3130:1-3185:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3186:1-3245:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3248:1-3350:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3351:1-3396:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3397:1-3442:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3449-3449)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__1' has dead code:
  on line 1851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1851-1851)
  on line 1853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1853-1853)
  on lines 1855..1856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1855-1856)
  on line 1862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1862-1862)
  on line 1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1864-1864)
  on lines 1866..1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1866-1867)
  on line 1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1873-1873)
  on line 1875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1875-1875)
  on lines 1877..1878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1877-1878)
  on line 1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1884-1884)
  on line 1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1886-1886)
  on lines 1888..1889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1888-1889)
  on line 1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1895-1895)
  on line 1897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1897-1897)
  on lines 1899..1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1899-1900)
  on line 1928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1928-1928)
  on line 1939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1939-1939)
  on line 1950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1950-1950)
  on line 1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1958-1958)
  on lines 1960..1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1960-1961)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__2' has dead code:
  on line 1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1996-1996)
  on line 1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1998-1998)
  on line 2000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2000-2000)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 350..351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:350-351)
  on line 357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:357-357)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2528-2528)
  on line 2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2531-2531)
  on line 2534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2534-2534)
  on line 2537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2537-2537)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 2171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2171-2171)
  on line 2174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2174-2174)
  on lines 2177..2178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2177-2178)
  on line 2180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2180-2180)
  on line 2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2182-2182)
  on line 2192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2192-2192)
  on lines 2194..2195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2194-2195)
  on line 2198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2198-2198)
  on line 2201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2201-2201)
  on line 2205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2205-2205)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:927-927)
  on line 933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:933-933)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on lines 151..152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:151-152)
  on lines 154..155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:154-155)
  on lines 157..158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:157-158)
  on lines 160..161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:160-161)
  on lines 163..164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:163-164)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:314-314)
[Warning][Deadcode] Function 'getCurrentHeading' has dead code:
  on line 366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:366-366)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 1794..1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1794-1796)
  on lines 1798..1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1798-1800)
  on lines 1802..1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1802-1804)
  on lines 1806..1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1806-1808)
  on lines 1810..1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1810-1812)
  on lines 1814..1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1814-1815)
  on line 1822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1822-1822)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 1755..1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1755-1757)
  on lines 1759..1761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1759-1761)
  on lines 1763..1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1763-1765)
  on lines 1767..1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1767-1769)
  on lines 1771..1773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1771-1773)
  on lines 1775..1776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1775-1776)
  on line 1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1783-1783)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on lines 1012..1013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1012-1013)
  on line 1015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1015-1015)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 1716..1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1716-1718)
  on lines 1720..1722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1720-1722)
  on lines 1724..1726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1724-1726)
  on lines 1728..1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1728-1730)
  on lines 1732..1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1732-1734)
  on lines 1736..1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1736-1737)
  on line 1744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1744-1744)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 2736..2737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2736-2737)
  on lines 2739..2740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2739-2740)
  on lines 2742..2743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2742-2743)
  on lines 2745..2746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2745-2746)
  on lines 2748..2749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2748-2749)
  on lines 2751..2752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2751-2752)
  on lines 2763..2764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2763-2764)
  on lines 2766..2767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2766-2767)
  on lines 2769..2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2769-2770)
  on lines 2772..2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2772-2773)
  on lines 2775..2776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2775-2776)
  on lines 2778..2779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2778-2779)
  on lines 2790..2791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2790-2791)
  on lines 2793..2794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2793-2794)
  on lines 2796..2797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2796-2797)
  on lines 2799..2800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2799-2800)
  on lines 2802..2803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2802-2803)
  on lines 2805..2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2805-2806)
  on lines 2817..2818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2817-2818)
  on lines 2820..2821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2820-2821)
  on lines 2823..2824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2823-2824)
  on lines 2826..2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2826-2827)
  on lines 2829..2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2829-2830)
  on lines 2832..2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2832-2833)
  on lines 2847..2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2847-2848)
  on lines 2850..2851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2850-2851)
  on lines 2853..2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2853-2854)
  on lines 2856..2857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2856-2857)
  on lines 2859..2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2859-2860)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1601-1601)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2469..2470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2469-2470)
  on lines 2473..2474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2473-2474)
  on lines 2490..2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2490-2492)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2556..2558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2556-2558)
  on lines 2560..2562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2560-2562)
  on lines 2564..2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2564-2566)
  on lines 2568..2570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2568-2570)
  on lines 2572..2574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2572-2574)
  on lines 2576..2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2576-2578)
  on lines 2589..2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2589-2591)
  on lines 2593..2595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2593-2595)
  on lines 2597..2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2597-2599)
  on lines 2601..2603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2601-2603)
  on lines 2605..2607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2605-2607)
  on lines 2609..2611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2609-2611)
  on lines 2622..2624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2622-2624)
  on lines 2626..2628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2626-2628)
  on lines 2630..2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2630-2632)
  on lines 2634..2636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2634-2636)
  on lines 2638..2640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2638-2640)
  on lines 2642..2644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2642-2644)
  on lines 2655..2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2655-2657)
  on lines 2659..2661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2659-2661)
  on lines 2663..2665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2663-2665)
  on lines 2667..2669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2667-2669)
  on lines 2671..2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2671-2673)
  on lines 2675..2677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2675-2677)
  on lines 2726..2728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2726-2728)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 3039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3039-3039)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 2376..2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2376-2378)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on lines 259..260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:259-260)
  on lines 262..263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:262-263)
  on lines 265..266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:265-266)
  on lines 268..269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:268-269)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1051..1054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1051-1054)
  on lines 1064..1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1064-1067)
  on lines 1077..1080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1077-1080)
  on lines 1090..1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1090-1093)
  on lines 1103..1106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1103-1106)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 2887..2888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2887-2888)
  on lines 2890..2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2890-2891)
  on lines 2893..2894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2893-2894)
  on lines 2896..2897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2896-2897)
  on lines 2899..2900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2899-2900)
  on lines 2902..2903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2902-2903)
  on lines 2914..2915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2914-2915)
  on lines 2917..2918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2917-2918)
  on lines 2920..2921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2920-2921)
  on lines 2923..2924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2923-2924)
  on lines 2926..2927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2926-2927)
  on lines 2929..2930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2929-2930)
  on lines 2941..2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2941-2942)
  on lines 2944..2945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2944-2945)
  on lines 2947..2948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2947-2948)
  on lines 2950..2951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2950-2951)
  on lines 2953..2954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2953-2954)
  on lines 2956..2957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2956-2957)
  on lines 2968..2969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2968-2969)
  on lines 2971..2972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2971-2972)
  on lines 2974..2975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2974-2975)
  on lines 2977..2978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2977-2978)
  on lines 2980..2981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2980-2981)
  on lines 2983..2984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2983-2984)
  on lines 2998..2999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2998-2999)
  on lines 3001..3002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3001-3002)
  on lines 3004..3005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3004-3005)
  on lines 3007..3008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3007-3008)
  on lines 3010..3011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3010-3011)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2500-2500)
  on line 2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2503-2503)
  on line 2506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2506-2506)
  on line 2509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2509-2509)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:285-285)
  on line 288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:288-288)
  on line 291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:291-291)
  on line 294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:294-294)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2352-2352)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1001-1001)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 963..964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:963-964)
  on line 970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:970-970)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:880-880)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on line 519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:519-519)
  on lines 521..523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:521-523)
  on lines 527..528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:527-528)
  on line 530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:530-530)
  on lines 532..534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:532-534)
  on lines 543..547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:543-547)
  on lines 556..557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:556-557)
  on line 559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:559-559)
  on lines 561..563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:561-563)
  on lines 572..576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:572-576)
  on lines 585..586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:585-586)
  on line 588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:588-588)
  on lines 590..592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:590-592)
  on lines 601..605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:601-605)
  on lines 614..615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:614-615)
  on line 617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:617-617)
  on lines 619..621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:619-621)
  on lines 630..634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:630-634)
  on lines 643..644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:643-644)
  on line 646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:646-646)
  on lines 648..650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:648-650)
  on lines 659..663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:659-663)
  on lines 665..666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:665-666)
  on lines 669..670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:669-670)
  on lines 673..674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:673-674)
  on lines 687..688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:687-688)
  on lines 698..699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:698-699)
  on lines 721..722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:721-722)
  on line 724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:724-724)
  on lines 726..728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:726-728)
  on lines 737..741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:737-741)
  on lines 750..751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:750-751)
  on line 753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:753-753)
  on lines 755..757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:755-757)
  on lines 766..770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:766-770)
  on lines 779..780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:779-780)
  on line 782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:782-782)
  on lines 784..786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:784-786)
  on lines 795..799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:795-799)
  on lines 808..809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:808-809)
  on line 811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:811-811)
  on lines 813..815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:813-815)
  on lines 824..828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:824-828)
  on lines 830..831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:830-831)
  on lines 834..835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:834-835)
  on lines 838..839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:838-839)
  on line 851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:851-851)
[Warning][Deadcode] Function 'test' has dead code:
  on line 2027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2027-2027)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 1141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1141-1141)
  on line 1143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1143-1143)
  on line 1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1145-1145)
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1155-1155)
  on line 1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1157-1157)
  on line 1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1159-1159)
  on line 1169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1169-1169)
  on line 1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1171-1171)
  on line 1173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1173-1173)
  on line 1183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1183-1183)
  on line 1185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1185-1185)
  on line 1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1187-1187)
  on line 1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1197-1197)
  on line 1199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1199-1199)
  on line 1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1201-1201)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1211-1211)
  on line 1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1213-1213)
  on line 1215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1215-1215)
  on line 1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1252-1252)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:3074-3074)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 352
  dead: 1051 (545 in uncalled functions)
  total lines: 1403
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1088:7-1088:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2480:15-2480:27)
[Warning][Deadcode][CWE-570] condition 'tmp___10' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1101:7-1101:15)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2499:7-2499:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2886:7-2886:17)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2502:9-2502:21)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1912:9-1912:31)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2687:15-2687:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2505:11-2505:23)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1712:7-1712:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2508:13-2508:25)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1923:11-1923:33)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2511:15-2511:27)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1927:13-1927:20)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:256:7-256:19)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1139:9-1139:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2527:7-2527:19)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:686:9-686:28)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1934:13-1934:35)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2530:9-2530:21)
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1938:15-1938:22)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1153:9-1153:18)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:692:9-692:27)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:693:11-693:28)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2913:9-2913:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2533:11-2533:23)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1945:15-1945:37)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:697:13-697:20)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2708:27-2708:38)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2536:13-2536:25)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1167:9-1167:18)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1949:17-1949:24)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2539:15-2539:27)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:284:7-284:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:708:11-708:29)
[Warning][Deadcode][CWE-570] condition 'currentFloorID___0 > 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1956:17-1956:39)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:709:13-709:31)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2555:7-2555:17)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1181:9-1181:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:926:9-926:12)
[Warning][Deadcode][CWE-571] condition 'floorButtons_0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:710:15-710:29)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:287:9-287:21)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2735:7-2735:17)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1751:7-1751:18)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:932:9-932:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:290:11-290:23)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1195:9-1195:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:293:13-293:25)
[Warning][Deadcode][CWE-570] condition 'dir == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:517:7-517:15)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2940:11-2940:21)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:296:15-296:27)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1209:9-1209:18)
[Warning][Deadcode][CWE-570] condition 'expectedDirection == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1994:9-1994:31)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2762:9-2762:19)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:962:9-962:12)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2588:9-2588:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2368:7-2368:10)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2967:13-2967:23)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1790:7-1790:18)
[Warning][Deadcode][CWE-571] condition 'tmp___7' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1245:11-1245:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:346:15-346:27)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2789:11-2789:21)
[Warning][Deadcode][CWE-571] condition 'ofHeading == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1008:7-1008:21)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2994:15-2994:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2995:17-2995:28)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2621:11-2621:21)
[Warning][Deadcode][CWE-571] condition 'p == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:148:7-148:13)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1036:7-1036:14)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2816:13-2816:23)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1049:7-1049:14)
[Warning][Deadcode][CWE-570] condition 'tmp___10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1850:7-1850:20)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1062:7-1062:14)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2654:13-2654:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2468:9-2468:21)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2843:15-2843:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2844:17-2844:28)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:1075:7-1075:14)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product27.cil.c:2472:11-2472:23)
[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)
