./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/elevator_spec9_productSimulator.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/elevator_spec9_productSimulator.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_spec9_productSimulator.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_spec9_productSimulator.cil.c:198:3-226:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:260:3-303:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:490:3-511:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:547:3-572:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:632:5-652:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:809:3-828:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:856:3-875:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3605:5-3663:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3680:9-3738: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] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2123:3-2123:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2956:5-2956:40)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2958:5-2958:40)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:51:1-102:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:105:1-115:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:116:1-126:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:127:1-137:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:138:1-148:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:149:1-159:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:172:1-183:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:234:1-311:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:312:1-323:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:324:1-335:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:336:1-346:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:347:1-363:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:419:1-464:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:465:1-520:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:521:1-580:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:583:1-685:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:686:1-731:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:732:1-777:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:791:1-833:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:834:1-880:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:924:1-965:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1941:1-1963:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1964:1-1986:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2294:1-2302:1)
[Warning][Deadcode] Function 'printState__before__overloaded' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3385:1-3555:1)
[Warning][Deadcode] Function 'printState__role__overloaded' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3556:1-3577:1)
[Warning][Deadcode] Function 'printState' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3578:1-3594:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3595:1-3753:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3765:1-3773:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1717-1717)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__2' has dead code:
  on line 1575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1575-1575)
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1578-1578)
  on line 1581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1581-1581)
  on lines 1586..1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1586-1587)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__3' has dead code:
  on line 1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1623-1623)
  on line 1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1631-1631)
  on line 1639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1639-1639)
  on line 1655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1655-1655)
[Warning][Deadcode] Function '__utac_acc__Specification9_spec__4' has dead code:
  on line 1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1679-1679)
  on line 1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1684-1684)
  on line 1689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1689-1689)
  on line 1699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1699-1699)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 2356..2357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2356-2357)
  on lines 2360..2361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2360-2361)
  on lines 2371..2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2371-2372)
  on lines 2378..2379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2378-2379)
  on lines 2382..2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2382-2383)
  on lines 2389..2390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2389-2390)
  on lines 2400..2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2400-2401)
  on lines 2404..2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2404-2405)
  on line 2420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2420-2420)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 2257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2257-2257)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on line 2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2291-2291)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 1034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1034-1034)
  on lines 1039..1040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1039-1040)
  on lines 1042..1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1042-1043)
  on lines 1045..1046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1045-1046)
[Warning][Deadcode] Function 'enterElevator__before__weight' has dead code:
  on line 2028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2028-2028)
  on line 2031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2031-2031)
  on line 2034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2034-2034)
  on line 2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2037-2037)
  on line 2040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2040-2040)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 2248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2248-2248)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 1886..1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1886-1887)
  on lines 1890..1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1890-1891)
  on lines 1894..1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1894-1895)
  on lines 1898..1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1898-1899)
  on lines 1902..1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1902-1903)
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1909-1910)
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1917-1917)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 1847..1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1847-1848)
  on lines 1851..1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1851-1852)
  on lines 1855..1856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1855-1856)
  on lines 1859..1860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1859-1860)
  on lines 1863..1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1863-1864)
  on lines 1870..1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1870-1871)
  on line 1878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1878-1878)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on line 3096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3096-3096)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 1808..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1808-1809)
  on lines 1812..1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1812-1813)
  on lines 1816..1817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1816-1817)
  on lines 1820..1821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1820-1821)
  on lines 1824..1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1824-1825)
  on lines 1831..1832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1831-1832)
  on line 1839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1839-1839)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 1242..1243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1242-1243)
  on lines 1245..1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1245-1246)
  on lines 1248..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1248-1249)
  on lines 1251..1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1251-1252)
  on lines 1254..1255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1254-1255)
  on lines 1257..1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1257-1258)
  on line 1270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1270-1270)
  on line 1273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1273-1273)
  on line 1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1276-1276)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1279-1279)
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1282-1282)
  on lines 1295..1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1295-1297)
  on lines 1299..1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1299-1300)
  on lines 1302..1303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1302-1303)
  on lines 1305..1306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1305-1306)
  on lines 1308..1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1308-1309)
  on lines 1311..1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1311-1312)
  on lines 1322..1324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1322-1324)
  on lines 1326..1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1326-1327)
  on lines 1329..1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1329-1330)
  on lines 1332..1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1332-1333)
  on lines 1335..1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1335-1336)
  on lines 1338..1339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1338-1339)
  on lines 1349..1351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1349-1351)
  on lines 1353..1354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1353-1354)
  on lines 1356..1357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1356-1357)
  on lines 1359..1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1359-1360)
  on lines 1362..1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1362-1363)
  on lines 1365..1366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1365-1366)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2905..2906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2905-2906)
  on lines 2909..2910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2909-2910)
  on lines 2913..2914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2913-2914)
  on lines 2921..2922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2921-2922)
  on line 2931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2931-2931)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 2020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2020-2020)
[Warning][Deadcode] Function 'isBlocked__before__overloaded' has dead code:
  on line 1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1993-1993)
[Warning][Deadcode] Function 'isBlocked__role__overloaded' has dead code:
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2002-2002)
[Warning][Deadcode] Function 'isEmpty' has dead code:
  on lines 2308..2309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2308-2309)
  on lines 2312..2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2312-2313)
  on lines 2316..2317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2316-2317)
  on lines 2320..2321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2320-2321)
  on lines 2324..2325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2324-2325)
  on line 2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2340-2340)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 3762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3762-3762)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:998-998)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 2433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2433-2433)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on line 1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1234-1234)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1545-1545)
[Warning][Deadcode] Function 'leaveElevator' has dead code:
  on line 2176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2176-2176)
  on line 2178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2178-2178)
[Warning][Deadcode] Function 'leaveElevator__before__weight' has dead code:
  on line 2089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2089-2089)
  on line 2092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2092-2092)
  on line 2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2095-2095)
  on line 2098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2098-2098)
  on line 2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2101-2101)
[Warning][Deadcode] Function 'main' has dead code:
  on line 409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:409-409)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2191-2191)
  on line 2194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2194-2194)
  on line 2197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2197-2197)
  on lines 2202..2203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2202-2203)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 3119..3122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3119-3122)
  on lines 3132..3135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3132-3135)
  on lines 3145..3148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3145-3148)
  on lines 3158..3161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3158-3161)
  on lines 3171..3174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3171-3174)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 1393..1394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1393-1394)
  on lines 1396..1397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1396-1397)
  on lines 1399..1400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1399-1400)
  on lines 1402..1403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1402-1403)
  on lines 1405..1406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1405-1406)
  on lines 1408..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1408-1409)
  on line 1421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1421-1421)
  on line 1424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1424-1424)
  on line 1427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1427-1427)
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1430-1430)
  on line 1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1433-1433)
  on lines 1446..1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1446-1448)
  on lines 1450..1451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1450-1451)
  on lines 1453..1454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1453-1454)
  on lines 1456..1457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1456-1457)
  on lines 1459..1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1459-1460)
  on lines 1462..1463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1462-1463)
  on lines 1473..1475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1473-1475)
  on lines 1477..1478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1477-1478)
  on lines 1480..1481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1480-1481)
  on lines 1483..1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1483-1484)
  on lines 1486..1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1486-1487)
  on lines 1489..1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1489-1490)
  on lines 1500..1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1500-1502)
  on lines 1504..1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1504-1505)
  on lines 1507..1508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1507-1508)
  on lines 1510..1511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1510-1511)
  on lines 1513..1514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1513-1514)
  on lines 1516..1517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1516-1517)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 1741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1741-1741)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 3082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3082-3082)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__before__executivefloor' has dead code:
  on line 3033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3033-3033)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__before__twothirdsfull' has dead code:
  on line 2987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2987-2987)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__role__executivefloor' has dead code:
  on line 3047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3047-3047)
  on line 3049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3049-3049)
  on line 3051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3051-3051)
  on line 3053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3053-3053)
  on lines 3055..3056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3055-3056)
  on line 3064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3064-3064)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__role__twothirdsfull' has dead code:
  on line 3015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3015-3015)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 2897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2897-2897)
[Warning][Deadcode] Function 'stopRequestedInDirection__before__executivefloor' has dead code:
  on line 2847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2847-2847)
[Warning][Deadcode] Function 'stopRequestedInDirection__before__twothirdsfull' has dead code:
  on lines 2468..2469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2468-2469)
  on lines 2481..2482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2481-2482)
  on lines 2510..2511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2510-2511)
  on lines 2526..2527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2526-2527)
  on lines 2539..2540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2539-2540)
  on lines 2555..2556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2555-2556)
  on lines 2584..2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2584-2585)
  on lines 2597..2598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2597-2598)
  on lines 2604..2605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2604-2605)
  on lines 2633..2634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2633-2634)
  on lines 2646..2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2646-2647)
  on lines 2662..2663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2662-2663)
  on lines 2675..2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2675-2676)
  on lines 2691..2692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2691-2692)
  on lines 2704..2705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2704-2705)
  on lines 2720..2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2720-2721)
  on lines 2749..2750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2749-2750)
  on lines 2762..2763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2762-2763)
  on lines 2769..2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2769-2770)
  on line 2786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2786-2786)
[Warning][Deadcode] Function 'stopRequestedInDirection__role__executivefloor' has dead code:
  on lines 2864..2867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2864-2867)
  on line 2869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2869-2869)
  on line 2877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2877-2877)
[Warning][Deadcode] Function 'stopRequestedInDirection__role__twothirdsfull' has dead code:
  on line 2826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2826-2826)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 3381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3381-3381)
[Warning][Deadcode] Function 'timeShift__before__overloaded' has dead code:
  on line 3219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3219-3219)
  on line 3221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3221-3221)
  on line 3223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3223-3223)
  on line 3233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3233-3233)
  on line 3235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3235-3235)
  on line 3237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3237-3237)
  on line 3247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3247-3247)
  on line 3249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3249-3249)
  on line 3251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3251-3251)
  on line 3261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3261-3261)
  on line 3263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3263-3263)
  on line 3265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3265-3265)
  on line 3275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3275-3275)
  on line 3277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3277-3277)
  on line 3279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3279-3279)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1797-1797)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 707
  dead: 833 (497 in uncalled functions)
  total lines: 1540
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2554:25-2554:32)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1638:17-1638:36)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1214:27-1214:38)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2566:25-2566:43)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1241:7-1241:17)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3045:7-3045:10)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1654:21-1654:40)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1677:7-1677:26)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2583:29-2583:36)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2153:7-2153:10)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1682:9-1682:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1687:11-1687:30)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2595:29-2595:47)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2596:31-2596:45)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_empty' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2169:7-2169:31)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1697:15-1697:34)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1268:9-1268:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1269:11-1269:22)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1272:13-1272:24)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2190:7-2190:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1275:15-1275:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2193:9-2193:21)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1278:17-1278:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2196:11-2196:23)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1281:19-1281:30)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3117:7-3117:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2199:13-2199:25)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1284:21-1284:32)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2632:13-2632:20)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3130:7-3130:14)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2644:13-2644:31)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2645:15-2645:29)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3143:7-3143:14)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2661:17-2661:24)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3156:7-3156:14)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2673:17-2673:35)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2674:19-2674:33)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3169:7-3169:14)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1807:7-1807:18)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1811:9-1811:20)
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2690:21-2690:28)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1815:11-1815:22)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1819:13-1819:24)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2702:21-2702:39)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2703:23-2703:37)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1823:15-1823:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1827:17-1827:28)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3217:9-3217:18)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2719:25-2719:32)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3231:9-3231:18)
[Warning][Deadcode][CWE-570] condition 'persons_0 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2307:7-2307:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1846:7-1846:18)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2731:25-2731:43)
[Warning][Deadcode][CWE-570] condition 'persons_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2311:9-2311:23)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1850:9-1850:20)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1392:7-1392:17)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3245:9-3245:18)
[Warning][Deadcode][CWE-570] condition 'persons_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2315:11-2315:25)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1854:11-1854:22)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3259:9-3259:18)
[Warning][Deadcode][CWE-570] condition 'persons_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2319:13-2319:27)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1858:13-1858:24)
[Warning][Deadcode][CWE-570] condition 'tmp___5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2748:29-2748:36)
[Warning][Deadcode][CWE-570] condition 'persons_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2323:15-2323:29)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1862:15-1862:26)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:3273:9-3273:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1033:7-1033:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1866:17-1866:28)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1036:9-1036:21)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2760:29-2760:47)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:198:10-198:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2761:31-2761:45)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1419:9-1419:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1420:11-1420:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:202:9-202:23)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1423:13-1423:24)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1885:7-1885:18)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:206:11-206:23)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2355:7-2355:14)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1426:15-1426:26)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1889:9-1889:20)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2359:9-2359:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1429:17-1429:28)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:218:9-218:12)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1893:11-1893:22)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1432:19-1432:30)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1435:21-1435:32)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1897:13-1897:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:198:10-198:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2370:13-2370:27)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1901:15-1901:26)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:202:9-202:23)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:206:11-206:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1905:17-1905:28)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2377:15-2377:22)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:218:9-218:12)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2381:17-2381:31)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1082:19-1082:30)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2388:19-2388:26)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:198:10-198:11)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:202:9-202:23)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2862:7-2862:14)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2399:23-2399:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:218:9-218:12)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2403:25-2403:39)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1115:21-1115:32)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:198:10-198:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2904:7-2904:21)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2908:9-2908:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2912:11-2912:25)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2467:13-2467:20)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2920:15-2920:29)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2479:13-2479:31)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2027:7-2027:13)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1148:23-1148:34)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2480:15-2480:29)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2030:9-2030:15)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2033:11-2033:17)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2036:13-2036:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1574:7-1574:17)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2039:15-2039:21)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1577:9-1577:19)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2042:17-2042:23)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1580:11-1580:21)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2508:17-2508:35)
[Warning][Deadcode][CWE-571] condition 'floor == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1583:13-1583:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2509:19-2509:33)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1181:25-1181:36)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2525:21-2525:28)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2088:7-2088:13)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2091:9-2091:15)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2537:21-2537:39)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2538:23-2538:37)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2094:11-2094:17)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2097:13-2097:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1622:13-1622:32)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2100:15-2100:21)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc9_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:1630:15-1630:34)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec9_productSimulator.cil.c:2103:17-2103:23)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
