./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_spec2_product30.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_spec2_product30.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:318:3-346:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:380:3-423:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:555:3-574:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:602:3-621:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2963:5-3021:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3038:9-3096:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3190:3-3211:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3247:3-3272:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3332:5-3352: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] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:172:1-223:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:225:1-235:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:236:1-246:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:247:1-257:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:258:1-268:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:269:1-279:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:292:1-303:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:354:1-431:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:432:1-443:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:444:1-455:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:456:1-466:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:467:1-483:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:537:1-579:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:580:1-626:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:679:1-720:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1305:1-1314:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1553:1-1575:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1576:1-1598:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1652:1-1683:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1684:1-1695:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1696:1-1715:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1828:1-1836:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1837:1-1876:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2479:1-2492:1)
[Warning][Deadcode] Function 'printState__wrappee__twothirdsfull' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2760:1-2930:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2931:1-2952:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2953:1-3111:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3119:1-3164:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3165:1-3220:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3221:1-3280:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3283:1-3385:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3386:1-3431:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:3432:1-3477:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:633-633)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__2' has dead code:
  on line 1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1375-1375)
  on line 1378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1378-1378)
  on line 1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1381-1381)
  on lines 1386..1387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1386-1387)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__3' has dead code:
  on line 1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1413-1413)
  on line 1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1415-1415)
  on lines 1417..1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1417-1418)
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1430-1430)
  on lines 1432..1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1432-1433)
  on line 1443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1443-1443)
  on line 1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1445-1445)
  on lines 1447..1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1447-1448)
  on line 1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1458-1458)
  on line 1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1460-1460)
  on lines 1462..1463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1462-1463)
  on line 1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1473-1473)
  on line 1475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1475-1475)
  on lines 1477..1478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1477-1478)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__4' has dead code:
  on line 1501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1501-1501)
  on line 1506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1506-1506)
  on line 1511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1511-1511)
  on line 1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1519-1519)
  on line 1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1521-1521)
  on line 1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1530-1530)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 1890..1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1890-1891)
  on lines 1894..1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1894-1895)
  on lines 1905..1906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1905-1906)
  on lines 1912..1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1912-1913)
  on lines 1916..1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1916-1917)
  on lines 1923..1924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1923-1924)
  on line 1931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1931-1931)
  on lines 1933..1935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1933-1935)
  on lines 1937..1939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1937-1939)
  on lines 1952..1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1952-1954)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1791-1791)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1802..1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1802-1804)
  on lines 1806..1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1806-1808)
  on lines 1810..1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1810-1812)
  on lines 1814..1816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1814-1816)
  on lines 1818..1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1818-1819)
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1825-1825)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:789-789)
  on lines 794..795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:794-795)
  on lines 797..798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:797-798)
  on lines 800..801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:800-801)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:339-339)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2405-2405)
  on lines 2410..2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2410-2411)
  on line 2419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2419-2419)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 1613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1613-1613)
  on line 1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1616-1616)
  on line 1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1619-1619)
  on line 1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1622-1622)
  on line 1625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1625-1625)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1782-1782)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 135..136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:135-136)
  on lines 139..140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:139-140)
  on lines 143..144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:143-144)
  on lines 147..148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:147-148)
  on lines 151..152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:151-152)
  on lines 158..159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:158-159)
  on line 166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:166-166)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 96..97 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:96-97)
  on lines 100..101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:100-101)
  on lines 104..105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:104-105)
  on lines 108..109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:108-109)
  on lines 112..113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:112-113)
  on lines 119..120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:119-120)
  on line 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:127-127)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 57..58 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:57-58)
  on lines 61..62 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:61-62)
  on lines 65..66 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:65-66)
  on lines 69..70 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:69-70)
  on lines 73..74 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:73-74)
  on lines 80..81 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:80-81)
  on line 88 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:88-88)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:997-998)
  on lines 1000..1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1000-1001)
  on lines 1003..1004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1003-1004)
  on lines 1006..1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1006-1007)
  on lines 1009..1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1009-1010)
  on lines 1012..1013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1012-1013)
  on line 1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1025-1025)
  on line 1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1028-1028)
  on line 1031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1031-1031)
  on line 1034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1034-1034)
  on line 1037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1037-1037)
  on lines 1050..1052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1050-1052)
  on lines 1054..1055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1054-1055)
  on lines 1057..1058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1057-1058)
  on lines 1060..1061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1060-1061)
  on lines 1063..1064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1063-1064)
  on lines 1066..1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1066-1067)
  on lines 1077..1079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1077-1079)
  on lines 1081..1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1081-1082)
  on lines 1084..1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1084-1085)
  on lines 1087..1088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1087-1088)
  on lines 1090..1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1090-1091)
  on lines 1093..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1093-1094)
  on lines 1104..1106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1104-1106)
  on lines 1108..1109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1108-1109)
  on lines 1111..1112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1111-1112)
  on lines 1114..1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1114-1115)
  on lines 1117..1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1117-1118)
  on lines 1120..1121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1120-1121)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2366..2367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2366-2367)
  on lines 2370..2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2370-2371)
  on lines 2374..2375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2374-2375)
  on lines 2378..2379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2378-2379)
  on lines 2382..2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2382-2383)
  on line 2392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2392-2392)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1605-1605)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 741..743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:741-743)
  on lines 751..753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:751-753)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 1967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1967-1967)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 817..819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:817-819)
  on lines 821..823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:821-823)
  on lines 825..827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:825-827)
  on lines 829..831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:829-831)
  on lines 833..835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:833-835)
  on lines 837..839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:837-839)
  on lines 882..885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:882-885)
  on lines 887..889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:887-889)
  on lines 891..893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:891-893)
  on lines 895..897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:895-897)
  on lines 899..901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:899-901)
  on lines 903..905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:903-905)
  on lines 915..918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:915-918)
  on lines 920..922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:920-922)
  on lines 924..926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:924-926)
  on lines 928..930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:928-930)
  on lines 932..934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:932-934)
  on lines 936..938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:936-938)
  on lines 948..951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:948-951)
  on lines 953..955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:953-955)
  on lines 957..959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:957-959)
  on lines 961..963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:961-963)
  on lines 965..967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:965-967)
  on lines 969..971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:969-971)
  on lines 987..989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:987-989)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1300-1300)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 527..529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:527-529)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1725-1725)
  on line 1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1728-1728)
  on line 1731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1731-1731)
  on lines 1736..1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1736-1737)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2513..2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2513-2516)
  on lines 2526..2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2526-2529)
  on lines 2539..2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2539-2542)
  on lines 2552..2555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2552-2555)
  on lines 2565..2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2565-2568)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 1148..1149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1148-1149)
  on lines 1151..1152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1151-1152)
  on lines 1154..1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1154-1155)
  on lines 1157..1158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1157-1158)
  on lines 1160..1161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1160-1161)
  on lines 1163..1164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1163-1164)
  on line 1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1176-1176)
  on line 1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1179-1179)
  on line 1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1182-1182)
  on line 1185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1185-1185)
  on line 1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1188-1188)
  on lines 1201..1203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1201-1203)
  on lines 1205..1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1205-1206)
  on lines 1208..1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1208-1209)
  on lines 1211..1212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1211-1212)
  on lines 1214..1215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1214-1215)
  on lines 1217..1218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1217-1218)
  on lines 1228..1230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1228-1230)
  on lines 1232..1233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1232-1233)
  on lines 1235..1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1235-1236)
  on lines 1238..1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1238-1239)
  on lines 1241..1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1241-1242)
  on lines 1244..1245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1244-1245)
  on lines 1255..1257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1255-1257)
  on lines 1259..1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1259-1260)
  on lines 1262..1263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1262-1263)
  on lines 1265..1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1265-1266)
  on lines 1268..1269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1268-1269)
  on lines 1271..1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1271-1272)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:761-761)
  on lines 766..767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:766-767)
  on lines 769..770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:769-770)
  on lines 772..773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:772-773)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1753-1753)
  on lines 1758..1759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1758-1759)
  on lines 1761..1762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1761-1762)
  on lines 1764..1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1764-1765)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:503-503)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on lines 2464..2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2464-2466)
  on line 2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2468-2468)
  on line 2476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2476-2476)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 2441..2442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2441-2442)
  on line 2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2448-2448)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 2339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2339-2339)
  on line 2341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2341-2341)
  on line 2343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2343-2343)
  on line 2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2346-2346)
  on line 2349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2349-2349)
  on line 2358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2358-2358)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on lines 1990..1991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1990-1991)
  on line 1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1996-1996)
  on line 1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1998-1998)
  on lines 2000..2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2000-2002)
  on lines 2012..2015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2012-2015)
  on lines 2040..2044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2040-2044)
  on lines 2053..2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2053-2054)
  on line 2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2056-2056)
  on lines 2058..2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2058-2060)
  on lines 2069..2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2069-2073)
  on lines 2082..2083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2082-2083)
  on line 2085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2085-2085)
  on lines 2087..2089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2087-2089)
  on lines 2098..2102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2098-2102)
  on lines 2111..2112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2111-2112)
  on line 2114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2114-2114)
  on lines 2116..2118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2116-2118)
  on lines 2127..2131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2127-2131)
  on lines 2133..2134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2133-2134)
  on lines 2137..2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2137-2138)
  on lines 2141..2142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2141-2142)
  on lines 2154..2156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2154-2156)
  on lines 2160..2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2160-2161)
  on line 2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2163-2163)
  on lines 2165..2167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2165-2167)
  on lines 2176..2180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2176-2180)
  on lines 2189..2190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2189-2190)
  on line 2192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2192-2192)
  on lines 2194..2196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2194-2196)
  on lines 2205..2209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2205-2209)
  on lines 2218..2219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2218-2219)
  on line 2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2221-2221)
  on lines 2223..2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2223-2225)
  on lines 2234..2238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2234-2238)
  on lines 2247..2248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2247-2248)
  on line 2250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2250-2250)
  on lines 2252..2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2252-2254)
  on lines 2263..2267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2263-2267)
  on lines 2276..2277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2276-2277)
  on line 2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2279-2279)
  on lines 2281..2283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2281-2283)
  on lines 2292..2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2292-2296)
  on lines 2298..2299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2298-2299)
  on lines 2302..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2302-2303)
  on lines 2306..2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2306-2307)
  on line 2319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2319-2319)
[Warning][Deadcode] Function 'timeShift__wrappee__twothirdsfull' has dead code:
  on line 2613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2613-2613)
  on line 2615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2615-2615)
  on line 2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2617-2617)
  on line 2627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2627-2627)
  on line 2629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2629-2629)
  on line 2631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2631-2631)
  on line 2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2641-2641)
  on line 2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2643-2643)
  on line 2645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2645-2645)
  on line 2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2655-2655)
  on line 2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2657-2657)
  on line 2659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2659-2659)
  on line 2669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2669-2669)
  on line 2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2671-2671)
  on line 2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2673-2673)
  on line 2683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2683-2683)
  on line 2685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2685-2685)
  on line 2687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2687-2687)
  on lines 2714..2715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2714-2715)
  on line 2717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2717-2717)
  on lines 2719..2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2719-2720)
  on line 2724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2724-2724)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1335-1335)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 334
  dead: 1084 (546 in uncalled functions)
  total lines: 1418
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:150:15-150:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2440:9-2440:12)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2011:11-2011:29)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2708:9-2708:16)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:154:17-154:28)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2024:13-2024:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2025:15-2025:32)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2462:7-2462:26)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2029:17-2029:24)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:519:7-519:10)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1612:7-1612:13)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:737:13-737:25)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1615:9-1615:15)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1618:11-1618:17)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2511:7-2511:14)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1621:13-1621:19)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1624:15-1624:21)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1374:7-1374:17)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:760:7-760:19)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1627:17-1627:23)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1377:9-1377:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1147:7-1147:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:763:9-763:21)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2524:7-2524:14)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1380:11-1380:21)
[Warning][Deadcode][CWE-571] condition 'floor == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1383:13-1383:23)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2537:7-2537:14)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:788:7-788:19)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1889:7-1889:14)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1412:7-1412:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:791:9-791:21)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2550:7-2550:14)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:56:7-56:18)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1174:9-1174:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1893:9-1893:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1175:11-1175:22)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:60:9-60:20)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1178:13-1178:24)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2563:7-2563:14)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1427:9-1427:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:64:11-64:22)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1428:11-1428:30)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1181:15-1181:26)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2338:7-2338:15)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1184:17-1184:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:816:7-816:17)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:68:13-68:24)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1904:13-1904:27)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:996:7-996:17)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1187:19-1187:30)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2576:7-2576:15)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:72:15-72:26)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1442:11-1442:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1190:21-1190:32)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1911:15-1911:22)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:76:17-76:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1915:17-1915:31)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2365:7-2365:21)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1457:13-1457:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:318:10-318:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2369:9-2369:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:95:7-95:18)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1922:19-1922:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1724:7-1724:19)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2611:9-2611:18)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:322:9-322:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2373:11-2373:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1727:9-1727:21)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1023:9-1023:19)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:99:9-99:20)
[Warning][Deadcode][CWE-571] condition 'floorButtons_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1926:21-1926:35)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1024:11-1024:22)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:326:11-326:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1730:11-1730:23)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1472:15-1472:25)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2625:9-2625:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2377:13-2377:27)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1027:13-1027:24)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:103:11-103:22)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:849:9-849:19)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1733:13-1733:25)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:338:9-338:12)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1030:15-1030:26)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2381:15-2381:29)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:107:13-107:24)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2639:9-2639:18)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1033:17-1033:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1499:7-1499:26)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:111:15-111:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1752:7-1752:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1036:19-1036:30)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:318:10-318:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1504:9-1504:28)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2653:9-2653:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1755:9-1755:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1039:21-1039:32)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:115:17-115:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1509:11-1509:30)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:322:9-322:23)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2400:7-2400:26)
[Warning][Deadcode][CWE-571] condition 'floorButtons_spc2_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1514:13-1514:32)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:326:11-326:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2404:9-2404:12)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2667:9-2667:18)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1985:7-1985:15)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:134:7-134:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:338:9-338:12)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:870:21-870:32)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2416:7-2416:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1989:9-1989:12)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2681:9-2681:18)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:138:9-138:20)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1995:9-1995:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:318:10-318:11)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:142:11-142:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:322:9-322:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:146:13-146:24)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:2700:9-2700:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:1798:7-1798:19)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product30.cil.c:326:11-326: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
