./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_spec14_product32.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_spec14_product32.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_spec14_product32.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_spec14_product32.cil.c:336:3-364:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:398:3-441:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:623:3-644:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:680:3-705:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:765:5-785:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:970:3-989:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1017:3-1036:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3201:5-3259:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3276:9-3334: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][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:190:1-241:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:254:1-264:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:265:1-275:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:276:1-286:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:287:1-297:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:372:1-449:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:450:1-461:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:462:1-473:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:474:1-484:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:485:1-501:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:552:1-597:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:598:1-653:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:654:1-713:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:716:1-818:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:819:1-864:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:865:1-910:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:913:1-922:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:952:1-994:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:995:1-1041:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1085:1-1126:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1733:1-1755:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1756:1-1778:1)
[Warning][Deadcode] Function 'isBlocked' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1779:1-1787:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1832:1-1863:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1864:1-1875:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1876:1-1895:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2004:1-2012:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2013:1-2052:1)
[Warning][Deadcode] Function 'anyStopRequested' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2053:1-2132:1)
[Warning][Deadcode] Function 'isIdle' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2133:1-2145:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2716:1-2729:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2998:1-3168:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3169:1-3190:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3191:1-3349:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3376-3376)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1967-1967)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1978..1980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1978-1980)
  on lines 1982..1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1982-1984)
  on lines 1986..1988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1986-1988)
  on lines 1990..1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1990-1992)
  on lines 1994..1995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1994-1995)
  on line 2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2001-2001)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 1195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1195-1195)
  on line 1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1201-1201)
  on line 1204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1204-1204)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:333-333)
  on line 336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:336-336)
  on lines 339..340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:339-340)
  on line 342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:342-342)
  on line 344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:344-344)
  on line 354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:354-354)
  on lines 356..357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:356-357)
  on line 360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:360-360)
  on line 363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:363-363)
  on line 367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:367-367)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 2611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2611-2611)
  on lines 2616..2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2616-2617)
  on line 2625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2625-2625)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 1793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1793-1793)
  on line 1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1796-1796)
  on line 1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1799-1799)
  on line 1802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1802-1802)
  on line 1805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1805-1805)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1958-1958)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 135..136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:135-136)
  on lines 139..140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:139-140)
  on lines 143..144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:143-144)
  on lines 147..148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:147-148)
  on lines 151..152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:151-152)
  on lines 158..159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:158-159)
  on line 166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:166-166)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 100..101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:100-101)
  on lines 104..105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:104-105)
  on lines 108..109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:108-109)
  on lines 112..113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:112-113)
  on lines 119..120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:119-120)
  on line 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.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_spec14_product32.cil.c:57-58)
  on lines 61..62 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:61-62)
  on lines 65..66 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:65-66)
  on lines 69..70 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:69-70)
  on lines 73..74 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:73-74)
  on lines 80..81 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:80-81)
  on line 88 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:88-88)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 1403..1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1403-1404)
  on lines 1406..1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1406-1407)
  on lines 1409..1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1409-1410)
  on lines 1412..1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1412-1413)
  on lines 1415..1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1415-1416)
  on lines 1418..1419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1418-1419)
  on line 1431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1431-1431)
  on line 1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1434-1434)
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1437-1437)
  on line 1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1440-1440)
  on line 1443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1443-1443)
  on lines 1457..1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1457-1458)
  on lines 1460..1461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1460-1461)
  on lines 1463..1464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1463-1464)
  on lines 1466..1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1466-1467)
  on lines 1469..1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1469-1470)
  on lines 1472..1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1472-1473)
  on lines 1484..1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1484-1485)
  on lines 1487..1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1487-1488)
  on lines 1490..1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1490-1491)
  on lines 1493..1494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1493-1494)
  on lines 1496..1497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1496-1497)
  on lines 1499..1500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1499-1500)
  on lines 1514..1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1514-1515)
  on lines 1517..1518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1517-1518)
  on lines 1520..1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1520-1521)
  on lines 1523..1524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1523-1524)
  on lines 1526..1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1526-1527)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2572..2573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2572-2573)
  on lines 2576..2577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2576-2577)
  on lines 2580..2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2580-2581)
  on lines 2584..2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2584-2585)
  on lines 2588..2589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2588-2589)
  on line 2598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2598-2598)
[Warning][Deadcode] Function 'isExecutiveFloor' has dead code:
  on line 3367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3367-3367)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 3358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3358-3358)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 1140..1141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1140-1141)
  on lines 1144..1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1144-1145)
  on lines 1157..1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1157-1159)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 1223..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1223-1225)
  on lines 1227..1229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1227-1229)
  on lines 1231..1233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1231-1233)
  on lines 1235..1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1235-1237)
  on lines 1239..1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1239-1241)
  on lines 1243..1245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1243-1245)
  on lines 1288..1291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1288-1291)
  on lines 1293..1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1293-1295)
  on lines 1297..1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1297-1299)
  on lines 1301..1303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1301-1303)
  on lines 1305..1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1305-1307)
  on lines 1309..1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1309-1311)
  on lines 1321..1324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1321-1324)
  on lines 1326..1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1326-1328)
  on lines 1330..1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1330-1332)
  on lines 1334..1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1334-1336)
  on lines 1338..1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1338-1340)
  on lines 1342..1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1342-1344)
  on lines 1354..1357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1354-1357)
  on lines 1359..1361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1359-1361)
  on lines 1363..1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1363-1365)
  on lines 1367..1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1367-1369)
  on lines 1371..1373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1371-1373)
  on lines 1375..1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1375-1377)
  on lines 1393..1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1393-1395)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1706-1706)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 540..542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:540-542)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1901-1901)
  on line 1904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1904-1904)
  on line 1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1907-1907)
  on lines 1912..1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1912-1913)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2750..2753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2750-2753)
  on lines 2763..2766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2763-2766)
  on lines 2776..2779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2776-2779)
  on lines 2789..2792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2789-2792)
  on lines 2802..2805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2802-2805)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 1554..1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1554-1555)
  on lines 1557..1558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1557-1558)
  on lines 1560..1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1560-1561)
  on lines 1563..1564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1563-1564)
  on lines 1566..1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1566-1567)
  on lines 1569..1570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1569-1570)
  on line 1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1582-1582)
  on line 1585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1585-1585)
  on line 1588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1588-1588)
  on line 1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1591-1591)
  on line 1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1594-1594)
  on lines 1607..1609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1607-1609)
  on lines 1611..1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1611-1612)
  on lines 1614..1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1614-1615)
  on lines 1617..1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1617-1618)
  on lines 1620..1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1620-1621)
  on lines 1623..1624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1623-1624)
  on lines 1634..1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1634-1636)
  on lines 1638..1639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1638-1639)
  on lines 1641..1642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1641-1642)
  on lines 1644..1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1644-1645)
  on lines 1647..1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1647-1648)
  on lines 1650..1651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1650-1651)
  on lines 1661..1663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1661-1663)
  on lines 1665..1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1665-1666)
  on lines 1668..1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1668-1669)
  on lines 1671..1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1671-1672)
  on lines 1674..1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1674-1675)
  on lines 1677..1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1677-1678)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 1167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1167-1167)
  on lines 1172..1173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1172-1173)
  on lines 1175..1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1175-1176)
  on lines 1178..1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1178-1179)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1929-1929)
  on lines 1934..1935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1934-1935)
  on lines 1937..1938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1937-1938)
  on lines 1940..1941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1940-1941)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:516-516)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2696-2696)
  on line 2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2698-2698)
  on line 2700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2700-2700)
  on line 2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2702-2702)
  on lines 2704..2705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2704-2705)
  on line 2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2713-2713)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 2647..2648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2647-2648)
  on line 2654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2654-2654)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__twothirdsfull' has dead code:
  on lines 2670..2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2670-2672)
  on line 2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2674-2674)
  on line 2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2682-2682)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 2551..2554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2551-2554)
  on line 2556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2556-2556)
  on line 2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2564-2564)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on lines 2166..2167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2166-2167)
  on line 2172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2172-2172)
  on line 2174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2174-2174)
  on lines 2176..2178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2176-2178)
  on lines 2188..2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2188-2191)
  on lines 2216..2220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2216-2220)
  on lines 2229..2230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2229-2230)
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2232-2232)
  on lines 2234..2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2234-2236)
  on lines 2245..2249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2245-2249)
  on lines 2258..2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2258-2259)
  on line 2261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2261-2261)
  on lines 2263..2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2263-2265)
  on lines 2274..2278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2274-2278)
  on lines 2287..2288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2287-2288)
  on line 2290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2290-2290)
  on lines 2292..2294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2292-2294)
  on lines 2303..2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2303-2307)
  on lines 2309..2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2309-2310)
  on lines 2313..2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2313-2314)
  on lines 2317..2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2317-2318)
  on lines 2330..2332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2330-2332)
  on lines 2336..2337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2336-2337)
  on line 2339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2339-2339)
  on lines 2341..2343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2341-2343)
  on lines 2352..2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2352-2356)
  on lines 2365..2366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2365-2366)
  on line 2368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2368-2368)
  on lines 2370..2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2370-2372)
  on lines 2381..2385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2381-2385)
  on lines 2394..2395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2394-2395)
  on line 2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2397-2397)
  on lines 2399..2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2399-2401)
  on lines 2410..2414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2410-2414)
  on lines 2423..2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2423-2424)
  on line 2426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2426-2426)
  on lines 2428..2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2428-2430)
  on lines 2439..2443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2439-2443)
  on lines 2452..2453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2452-2453)
  on line 2455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2455-2455)
  on lines 2457..2459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2457-2459)
  on lines 2468..2472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2468-2472)
  on lines 2474..2475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2474-2475)
  on lines 2478..2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2478-2479)
  on lines 2482..2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2482-2483)
  on line 2495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2495-2495)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__twothirdsfull' has dead code:
  on line 2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2516-2516)
  on line 2518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2518-2518)
  on line 2520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2520-2520)
  on line 2523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2523-2523)
  on line 2526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2526-2526)
  on line 2535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2535-2535)
[Warning][Deadcode] Function 'test' has dead code:
  on line 184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:184-184)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 2850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2850-2850)
  on line 2852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2852-2852)
  on line 2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2854-2854)
  on line 2864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2864-2864)
  on line 2866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2866-2866)
  on line 2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2868-2868)
  on line 2878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2878-2878)
  on line 2880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2880-2880)
  on line 2882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2882-2882)
  on line 2892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2892-2892)
  on line 2894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2894-2894)
  on line 2896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2896-2896)
  on line 2906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2906-2906)
  on line 2908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2908-2908)
  on line 2910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2910-2910)
  on line 2920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2920-2920)
  on line 2922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2922-2922)
  on line 2924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2924-2924)
  on lines 2951..2952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2951-2952)
  on line 2954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2954-2954)
  on lines 2956..2957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2956-2957)
  on line 2961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2961-2961)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:943-943)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 311
  dead: 1085 (584 in uncalled functions)
  total lines: 1396
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:150:15-150:26)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3395:9-3395:16)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1430:11-1430:22)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:3401:11-3401:18)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:154:17-154:28)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2515:7-2515:15)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2761:7-2761:14)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1433:13-1433:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1255:9-1255:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1436:15-1436:26)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1439:17-1439:28)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2774:7-2774:14)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1442:19-1442:30)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:532:7-532:10)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1445:21-1445:32)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2549:7-2549:14)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1456:11-1456:21)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2787:7-2787:14)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1900:7-1900:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1903:9-1903:21)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1906:11-1906:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1276:21-1276:32)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2800:7-2800:14)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2571:7-2571:21)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1909:13-1909:25)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2575:9-2575:23)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2813:7-2813:15)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2579:11-2579:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1928:7-1928:19)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1483:13-1483:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1931:9-1931:21)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2583:13-2583:27)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2587:15-2587:29)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2161:7-2161:15)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2848:9-2848:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2165:9-2165:12)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:56:7-56:18)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2606:7-2606:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2171:9-2171:27)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2862:9-2862:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2610:9-2610:12)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1510:15-1510:25)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:60:9-60:20)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1511:17-1511:28)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1974:7-1974:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1139:11-1139:23)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:64:11-64:22)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2876:9-2876:18)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2622:7-2622:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2187:11-2187:29)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1143:13-1143:25)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:68:13-68:24)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2890:9-2890:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1147:15-1147:27)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:72:15-72:26)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2200:13-2200:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2201:15-2201:32)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:76:17-76:28)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2904:9-2904:18)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2205:17-2205:24)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1166:7-1166:19)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2646:9-2646:12)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1553:7-1553:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1169:9-1169:21)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2918:9-2918:18)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:99:9-99:20)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2668:7-2668:26)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2937:9-2937:23)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1792:7-1792:13)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:103:11-103:22)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1795:9-1795:15)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1194:7-1194:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:107:13-107:24)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2945:9-2945:16)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1798:11-1798:17)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:111:15-111:26)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1801:13-1801:19)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1580:9-1580:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1200:11-1200:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1581:11-1581:22)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2694:7-2694:10)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1804:15-1804:21)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1203:13-1203:25)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:115:17-115:28)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1584:13-1584:24)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1807:17-1807:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1206:15-1206:27)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1587:15-1587:26)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1590:17-1590:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1222:7-1222:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1402:7-1402:17)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:134:7-134:18)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1593:19-1593:30)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:138:9-138:20)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:1596:21-1596:32)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:142:11-142:22)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:146:13-146:24)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product32.cil.c:2748:7-2748:14)
[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
