./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/elevator_spec3_product32.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/elevator_spec3_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_spec3_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_spec3_product32.cil.c:79:3-98:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:126:3-145:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:276:3-297:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:333:3-358:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:418:5-438:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1703:3-1731:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1763:3-1806:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3397:5-3455:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3472:9-3530:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:61:1-103:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:104:1-150:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:165:1-174:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:205:1-250:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:251:1-306:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:307:1-366:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:369:1-471:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:472:1-517:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:518:1-563:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1560:1-1611:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1623:1-1633:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1634:1-1644:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1645:1-1655:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1656:1-1666:1)
[Warning][Deadcode] Function 'bigMacCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1667:1-1677:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1737:1-1814:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1815:1-1826:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1827:1-1838:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1839:1-1849:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1850:1-1866:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1952:1-1974:1)
[Warning][Deadcode] Function 'isBlocked' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1975:1-1983:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2028:1-2059:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2060:1-2071:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2072:1-2091:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2209:1-2248:1)
[Warning][Deadcode] Function 'anyStopRequested' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2249:1-2328:1)
[Warning][Deadcode] Function 'isIdle' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2329:1-2341:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3194:1-3364:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3365:1-3386:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3387:1-3545:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3557:1-3565:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:157-157)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__1' has dead code:
  on line 592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:592-592)
  on line 594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:594-594)
  on lines 596..597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:596-597)
  on line 603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:603-603)
  on line 605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:605-605)
  on lines 607..608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:607-608)
  on line 614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:614-614)
  on line 616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:616-616)
  on lines 618..619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:618-619)
  on line 625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:625-625)
  on line 627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:627-627)
  on lines 629..630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:629-630)
  on line 636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:636-636)
  on line 638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:638-638)
  on lines 640..641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:640-641)
  on line 669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:669-669)
  on line 680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:680-680)
  on line 691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:691-691)
  on line 699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:699-699)
  on lines 701..702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:701-702)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__2' has dead code:
  on line 737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:737-737)
  on line 739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:739-739)
  on line 741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:741-741)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2163-2163)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 2190..2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2190-2191)
  on line 2197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2197-2197)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1026-1026)
  on line 1029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1029-1029)
  on line 1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1032-1032)
  on line 1035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1035-1035)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1700-1700)
  on line 1703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1703-1703)
  on lines 1706..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1706-1707)
  on line 1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1709-1709)
  on line 1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1711-1711)
  on line 1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1721-1721)
  on lines 1723..1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1723-1724)
  on line 1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1727-1727)
  on line 1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1730-1730)
  on line 1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1734-1734)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 2807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2807-2807)
  on line 2813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2813-2813)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on lines 1991..1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1991-1992)
  on lines 1994..1995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1994-1995)
  on lines 1997..1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1997-1998)
  on lines 2000..2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2000-2001)
  on lines 2003..2004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2003-2004)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 2154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2154-2154)
[Warning][Deadcode] Function 'getCurrentHeading' has dead code:
  on line 2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2206-2206)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 842..844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:842-844)
  on lines 846..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:846-848)
  on lines 850..852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:850-852)
  on lines 854..856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:854-856)
  on lines 858..860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:858-860)
  on lines 862..863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:862-863)
  on line 870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:870-870)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 803..805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:803-805)
  on lines 807..809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:807-809)
  on lines 811..813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:811-813)
  on lines 815..817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:815-817)
  on lines 819..821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:819-821)
  on lines 823..824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:823-824)
  on line 831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:831-831)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on lines 2920..2921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2920-2921)
  on line 2923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2923-2923)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 764..766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:764-766)
  on lines 768..770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:768-770)
  on lines 772..774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:772-774)
  on lines 776..778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:776-778)
  on lines 780..782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:780-782)
  on lines 784..785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:784-785)
  on line 792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:792-792)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 1234..1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1234-1235)
  on lines 1237..1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1237-1238)
  on lines 1240..1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1240-1241)
  on lines 1243..1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1243-1244)
  on lines 1246..1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1246-1247)
  on lines 1249..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1249-1250)
  on lines 1261..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1261-1262)
  on lines 1264..1265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1264-1265)
  on lines 1267..1268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1267-1268)
  on lines 1270..1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1270-1271)
  on lines 1273..1274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1273-1274)
  on lines 1276..1277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1276-1277)
  on lines 1288..1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1288-1289)
  on lines 1291..1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1291-1292)
  on lines 1294..1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1294-1295)
  on lines 1297..1298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1297-1298)
  on lines 1300..1301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1300-1301)
  on lines 1303..1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1303-1304)
  on lines 1315..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1315-1316)
  on lines 1318..1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1318-1319)
  on lines 1321..1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1321-1322)
  on lines 1324..1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1324-1325)
  on lines 1327..1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1327-1328)
  on lines 1330..1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1330-1331)
  on lines 1345..1346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1345-1346)
  on lines 1348..1349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1348-1349)
  on lines 1351..1352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1351-1352)
  on lines 1354..1355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1354-1355)
  on lines 1357..1358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1357-1358)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2771..2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2771-2773)
  on lines 2775..2777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2775-2777)
  on lines 2779..2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2779-2781)
  on lines 2783..2785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2783-2785)
  on lines 2787..2788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2787-2788)
  on line 2794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2794-2794)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 3554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3554-3554)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 967..968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:967-968)
  on lines 971..972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:971-972)
  on lines 988..990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:988-990)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 1054..1056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1054-1056)
  on lines 1058..1060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1058-1060)
  on lines 1062..1064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1062-1064)
  on lines 1066..1068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1066-1068)
  on lines 1070..1072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1070-1072)
  on lines 1074..1076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1074-1076)
  on lines 1087..1089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1087-1089)
  on lines 1091..1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1091-1093)
  on lines 1095..1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1095-1097)
  on lines 1099..1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1099-1101)
  on lines 1103..1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1103-1105)
  on lines 1107..1109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1107-1109)
  on lines 1120..1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1120-1122)
  on lines 1124..1126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1124-1126)
  on lines 1128..1130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1128-1130)
  on lines 1132..1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1132-1134)
  on lines 1136..1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1136-1138)
  on lines 1140..1142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1140-1142)
  on lines 1153..1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1153-1155)
  on lines 1157..1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1157-1159)
  on lines 1161..1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1161-1163)
  on lines 1165..1167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1165-1167)
  on lines 1169..1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1169-1171)
  on lines 1173..1175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1173-1175)
  on lines 1224..1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1224-1226)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1537-1537)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 1902..1904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1902-1904)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on lines 2099..2100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2099-2100)
  on lines 2102..2103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2102-2103)
  on lines 2105..2106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2105-2106)
  on lines 2108..2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2108-2109)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2959..2962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2959-2962)
  on lines 2972..2975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2972-2975)
  on lines 2985..2988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2985-2988)
  on lines 2998..3001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2998-3001)
  on lines 3011..3014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3011-3014)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 1385..1386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1385-1386)
  on lines 1388..1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1388-1389)
  on lines 1391..1392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1391-1392)
  on lines 1394..1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1394-1395)
  on lines 1397..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1397-1398)
  on lines 1400..1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1400-1401)
  on lines 1412..1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1412-1413)
  on lines 1415..1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1415-1416)
  on lines 1418..1419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1418-1419)
  on lines 1421..1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1421-1422)
  on lines 1424..1425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1424-1425)
  on lines 1427..1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1427-1428)
  on lines 1439..1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1439-1440)
  on lines 1442..1443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1442-1443)
  on lines 1445..1446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1445-1446)
  on lines 1448..1449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1448-1449)
  on lines 1451..1452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1451-1452)
  on lines 1454..1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1454-1455)
  on lines 1466..1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1466-1467)
  on lines 1469..1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1469-1470)
  on lines 1472..1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1472-1473)
  on lines 1475..1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1475-1476)
  on lines 1478..1479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1478-1479)
  on lines 1481..1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1481-1482)
  on lines 1496..1497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1496-1497)
  on lines 1499..1500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1499-1500)
  on lines 1502..1503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1502-1503)
  on lines 1505..1506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1505-1506)
  on lines 1508..1509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1508-1509)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:998-998)
  on line 1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1001-1001)
  on line 1004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1004-1004)
  on line 1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1007-1007)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2125-2125)
  on line 2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2128-2128)
  on line 2131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2131-2131)
  on line 2134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2134-2134)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1881-1881)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 2909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2909-2909)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 2843..2844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2843-2844)
  on line 2850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2850-2850)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__twothirdsfull' has dead code:
  on lines 2866..2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2866-2868)
  on line 2870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2870-2870)
  on line 2878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2878-2878)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 2760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2760-2760)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on line 2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2359-2359)
  on lines 2361..2363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2361-2363)
  on lines 2367..2368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2367-2368)
  on line 2370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2370-2370)
  on lines 2372..2374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2372-2374)
  on lines 2383..2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2383-2387)
  on lines 2396..2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2396-2397)
  on line 2399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2399-2399)
  on lines 2401..2403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2401-2403)
  on lines 2412..2416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2412-2416)
  on lines 2425..2426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2425-2426)
  on line 2428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2428-2428)
  on lines 2430..2432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2430-2432)
  on lines 2441..2445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2441-2445)
  on lines 2454..2455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2454-2455)
  on line 2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2457-2457)
  on lines 2459..2461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2459-2461)
  on lines 2470..2474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2470-2474)
  on lines 2483..2484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2483-2484)
  on line 2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2486-2486)
  on lines 2488..2490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2488-2490)
  on lines 2499..2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2499-2503)
  on lines 2505..2506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2505-2506)
  on lines 2509..2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2509-2510)
  on lines 2513..2514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2513-2514)
  on lines 2527..2528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2527-2528)
  on lines 2538..2539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2538-2539)
  on lines 2561..2562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2561-2562)
  on line 2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2564-2564)
  on lines 2566..2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2566-2568)
  on lines 2577..2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2577-2581)
  on lines 2590..2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2590-2591)
  on line 2593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2593-2593)
  on lines 2595..2597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2595-2597)
  on lines 2606..2610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2606-2610)
  on lines 2619..2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2619-2620)
  on line 2622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2622-2622)
  on lines 2624..2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2624-2626)
  on lines 2635..2639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2635-2639)
  on lines 2648..2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2648-2649)
  on line 2651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2651-2651)
  on lines 2653..2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2653-2655)
  on lines 2664..2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2664-2668)
  on lines 2670..2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2670-2671)
  on lines 2674..2675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2674-2675)
  on lines 2678..2679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2678-2679)
  on line 2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2691-2691)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__twothirdsfull' has dead code:
  on line 2712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2712-2712)
  on line 2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2714-2714)
  on line 2716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2716-2716)
  on line 2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2719-2719)
  on line 2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2722-2722)
  on line 2731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2731-2731)
[Warning][Deadcode] Function 'test' has dead code:
  on line 1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1555-1555)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 3175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3175-3175)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 3046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3046-3046)
  on line 3048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3048-3048)
  on line 3050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3050-3050)
  on line 3060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3060-3060)
  on line 3062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3062-3062)
  on line 3064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3064-3064)
  on line 3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3074-3074)
  on line 3076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3076-3076)
  on line 3078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3078-3078)
  on line 3088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3088-3088)
  on line 3090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3090-3090)
  on line 3092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3092-3092)
  on line 3102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3102-3102)
  on line 3104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3104-3104)
  on line 3106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3106-3106)
  on line 3116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3116-3116)
  on line 3118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3118-3118)
  on line 3120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3120-3120)
  on line 3157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3157-3157)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:195-195)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 383
  dead: 1064 (530 in uncalled functions)
  total lines: 1447
[Warning][Deadcode][CWE-570] condition 'tmp___10' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3009:7-3009:15)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2124:7-2124:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2548:11-2548:29)
[Warning][Deadcode][CWE-570] condition 'expectedDirection == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:735:9-735:31)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2549:13-2549:31)
[Warning][Deadcode][CWE-571] condition 'floorButtons_0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2550:15-2550:29)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2127:9-2127:21)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1152:13-1152:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:966:9-966:21)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2130:11-2130:23)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1341:15-1341:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1342:17-1342:28)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:760:7-760:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2133:13-2133:25)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1894:7-1894:10)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:970:11-970:23)
[Warning][Deadcode][CWE-570] condition 'dir == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2357:7-2357:15)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2136:15-2136:27)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3044:9-3044:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:978:15-978:27)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3058:9-3058:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2806:9-2806:12)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2812:9-2812:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:997:7-997:19)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3072:9-3072:18)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1384:7-1384:17)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1000:9-1000:21)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1185:15-1185:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1003:11-1003:23)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3086:9-3086:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1006:13-1006:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:799:7-799:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1009:15-1009:27)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3100:9-3100:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2186:15-2186:27)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2842:9-2842:12)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1025:7-1025:19)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3114:9-3114:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1028:9-1028:21)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1411:9-1411:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1031:11-1031:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1206:27-1206:38)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1034:13-1034:25)
[Warning][Deadcode][CWE-570] condition 'tmp___10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:591:7-591:20)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2864:7-2864:26)
[Warning][Deadcode][CWE-571] condition 'p == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1988:7-1988:13)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1037:15-1037:27)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1053:7-1053:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1233:7-1233:17)
[Warning][Deadcode][CWE-571] condition 'tmp___7' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3150:11-3150:18)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:838:7-838:18)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1438:11-1438:21)
[Warning][Deadcode][CWE-570] condition 'weight > maximumWeight' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:3174:9-3174:31)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1260:9-1260:19)
[Warning][Deadcode][CWE-571] condition 'ofHeading == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2916:7-2916:21)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1086:9-1086:19)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1465:13-1465:23)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:653:9-653:31)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2944:7-2944:14)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:664:11-664:33)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2711:7-2711:15)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2957:7-2957:14)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1287:11-1287:21)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:668:13-668:20)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:675:13-675:35)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2970:7-2970:14)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1492:15-1492:25)
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:679:15-679:22)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1493:17-1493:28)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1119:11-1119:21)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:686:15-686:37)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:690:17-690:24)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2983:7-2983:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2096:7-2096:19)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2526:9-2526:28)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:1314:13-1314:23)
[Warning][Deadcode][CWE-570] condition 'currentFloorID___0 > 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:697:17-697:39)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2532:9-2532:27)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2996:7-2996:14)
[Warning][Deadcode][CWE-571] condition 'floorButtons_0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2767:7-2767:21)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2533:11-2533:28)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product32.cil.c:2537:13-2537:20)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
