./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_spec14_product28.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_spec14_product28.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_product28.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_product28.cil.c:1683:5-1741:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1758:9-1816:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2016:3-2044:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2076:3-2119:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2248:3-2267:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2295:3-2314:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:3059:3-3080:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:3116:3-3141:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:3201:5-3221:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:53:1-62:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:284:1-306:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:307:1-329:1)
[Warning][Deadcode] Function 'isBlocked' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:330:1-338:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:383:1-414:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:415:1-426:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:427:1-446:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:555:1-563:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:564:1-603:1)
[Warning][Deadcode] Function 'anyStopRequested' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:604:1-683:1)
[Warning][Deadcode] Function 'isIdle' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:684:1-696:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1078:1-1111:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1199:1-1212:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1480:1-1650:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1651:1-1672:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1673:1-1831:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1873:1-1924:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1937:1-1947:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1948:1-1958:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1959:1-1969:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1970:1-1980:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2050:1-2127:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2128:1-2139:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2140:1-2151:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2152:1-2162:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2163:1-2179:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2230:1-2272:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2273:1-2319:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2357:1-2398:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2988:1-3033:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:3034:1-3089:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:3090:1-3149:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:3152:1-3254:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:3255:1-3300:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:3301:1-3346:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2226-2226)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:518-518)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 529..531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:529-531)
  on lines 533..535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:533-535)
  on lines 537..539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:537-539)
  on lines 541..543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:541-543)
  on lines 545..546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:545-546)
  on line 552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:552-552)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2467-2467)
  on line 2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2473-2473)
  on line 2476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2476-2476)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 2013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2013-2013)
  on line 2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2016-2016)
  on lines 2019..2020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2019-2020)
  on line 2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2022-2022)
  on line 2024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2024-2024)
  on line 2034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2034-2034)
  on lines 2036..2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2036-2037)
  on line 2040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2040-2040)
  on line 2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2043-2043)
  on line 2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2047-2047)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1122-1122)
  on lines 1127..1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1127-1128)
  on line 1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1136-1136)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:344-344)
  on line 347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:347-347)
  on line 350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:350-350)
  on line 353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:353-353)
  on line 356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:356-356)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:509-509)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 218..219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:218-219)
  on lines 222..223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:222-223)
  on lines 226..227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:226-227)
  on lines 230..231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:230-231)
  on lines 234..235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:234-235)
  on lines 241..242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:241-242)
  on line 249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:249-249)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 183..184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:183-184)
  on lines 187..188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:187-188)
  on lines 191..192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:191-192)
  on lines 195..196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:195-196)
  on lines 202..203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:202-203)
  on line 210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:210-210)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 140..141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:140-141)
  on lines 144..145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:144-145)
  on lines 148..149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:148-149)
  on lines 152..153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:152-153)
  on lines 156..157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:156-157)
  on lines 163..164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:163-164)
  on line 171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:171-171)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 2675..2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2675-2676)
  on lines 2678..2679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2678-2679)
  on lines 2681..2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2681-2682)
  on lines 2684..2685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2684-2685)
  on lines 2687..2688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2687-2688)
  on lines 2690..2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2690-2691)
  on line 2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2703-2703)
  on line 2706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2706-2706)
  on line 2709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2709-2709)
  on line 2712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2712-2712)
  on line 2715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2715-2715)
  on lines 2729..2730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2729-2730)
  on lines 2732..2733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2732-2733)
  on lines 2735..2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2735-2736)
  on lines 2738..2739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2738-2739)
  on lines 2741..2742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2741-2742)
  on lines 2744..2745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2744-2745)
  on lines 2756..2757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2756-2757)
  on lines 2759..2760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2759-2760)
  on lines 2762..2763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2762-2763)
  on lines 2765..2766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2765-2766)
  on lines 2768..2769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2768-2769)
  on lines 2771..2772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2771-2772)
  on lines 2786..2787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2786-2787)
  on lines 2789..2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2789-2790)
  on lines 2792..2793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2792-2793)
  on lines 2795..2796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2795-2796)
  on lines 2798..2799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2798-2799)
[Warning][Deadcode] Function 'isExecutiveFloor' has dead code:
  on line 1849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1849-1849)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1840-1840)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2412..2413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2412-2413)
  on lines 2416..2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2416-2417)
  on lines 2429..2431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2429-2431)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2495..2497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2495-2497)
  on lines 2499..2501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2499-2501)
  on lines 2503..2505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2503-2505)
  on lines 2507..2509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2507-2509)
  on lines 2511..2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2511-2513)
  on lines 2515..2517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2515-2517)
  on lines 2560..2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2560-2563)
  on lines 2565..2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2565-2567)
  on lines 2569..2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2569-2571)
  on lines 2573..2575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2573-2575)
  on lines 2577..2579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2577-2579)
  on lines 2581..2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2581-2583)
  on lines 2593..2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2593-2596)
  on lines 2598..2600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2598-2600)
  on lines 2602..2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2602-2604)
  on lines 2606..2608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2606-2608)
  on lines 2610..2612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2610-2612)
  on lines 2614..2616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2614-2616)
  on lines 2626..2629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2626-2629)
  on lines 2631..2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2631-2633)
  on lines 2635..2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2635-2637)
  on lines 2639..2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2639-2641)
  on lines 2643..2645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2643-2645)
  on lines 2647..2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2647-2649)
  on lines 2665..2667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2665-2667)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 2978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2978-2978)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 2215..2217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2215-2217)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:452-452)
  on line 455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:455-455)
  on line 458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:458-458)
  on lines 463..464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:463-464)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1233..1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1233-1236)
  on lines 1246..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1246-1249)
  on lines 1259..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1259-1262)
  on lines 1272..1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1272-1275)
  on lines 1285..1288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1285-1288)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 2826..2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2826-2827)
  on lines 2829..2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2829-2830)
  on lines 2832..2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2832-2833)
  on lines 2835..2836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2835-2836)
  on lines 2838..2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2838-2839)
  on lines 2841..2842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2841-2842)
  on line 2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2854-2854)
  on line 2857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2857-2857)
  on line 2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2860-2860)
  on line 2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2863-2863)
  on line 2866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2866-2866)
  on lines 2879..2881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2879-2881)
  on lines 2883..2884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2883-2884)
  on lines 2886..2887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2886-2887)
  on lines 2889..2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2889-2890)
  on lines 2892..2893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2892-2893)
  on lines 2895..2896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2895-2896)
  on lines 2906..2908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2906-2908)
  on lines 2910..2911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2910-2911)
  on lines 2913..2914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2913-2914)
  on lines 2916..2917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2916-2917)
  on lines 2919..2920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2919-2920)
  on lines 2922..2923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2922-2923)
  on lines 2933..2935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2933-2935)
  on lines 2937..2938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2937-2938)
  on lines 2940..2941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2940-2941)
  on lines 2943..2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2943-2944)
  on lines 2946..2947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2946-2947)
  on lines 2949..2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2949-2950)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2439-2439)
  on lines 2444..2445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2444-2445)
  on lines 2447..2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2447-2448)
  on lines 2450..2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2450-2451)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:480-480)
  on lines 485..486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:485-486)
  on lines 488..489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:488-489)
  on lines 491..492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:491-492)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 2194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2194-2194)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1179-1179)
  on line 1181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1181-1181)
  on line 1183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1183-1183)
  on line 1185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1185-1185)
  on lines 1187..1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1187-1188)
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1196-1196)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 1158..1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1158-1159)
  on line 1165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1165-1165)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 1062..1065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1062-1065)
  on line 1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1067-1067)
  on line 1075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1075-1075)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on lines 717..718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:717-718)
  on line 723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:723-723)
  on line 725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:725-725)
  on lines 727..729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:727-729)
  on lines 739..742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:739-742)
  on lines 767..771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:767-771)
  on lines 780..781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:780-781)
  on line 783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:783-783)
  on lines 785..787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:785-787)
  on lines 796..800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:796-800)
  on lines 809..810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:809-810)
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:812-812)
  on lines 814..816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:814-816)
  on lines 825..829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:825-829)
  on lines 838..839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:838-839)
  on line 841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:841-841)
  on lines 843..845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:843-845)
  on lines 854..858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:854-858)
  on lines 860..861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:860-861)
  on lines 864..865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:864-865)
  on lines 868..869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:868-869)
  on lines 881..883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:881-883)
  on lines 887..888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:887-888)
  on line 890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:890-890)
  on lines 892..894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:892-894)
  on lines 903..907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:903-907)
  on lines 916..917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:916-917)
  on line 919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:919-919)
  on lines 921..923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:921-923)
  on lines 932..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:932-936)
  on lines 945..946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:945-946)
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:948-948)
  on lines 950..952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:950-952)
  on lines 961..965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:961-965)
  on lines 974..975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:974-975)
  on line 977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:977-977)
  on lines 979..981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:979-981)
  on lines 990..994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:990-994)
  on lines 1003..1004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1003-1004)
  on line 1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1006-1006)
  on lines 1008..1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1008-1010)
  on lines 1019..1023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1019-1023)
  on lines 1025..1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1025-1026)
  on lines 1029..1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1029-1030)
  on lines 1033..1034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1033-1034)
  on line 1046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1046-1046)
[Warning][Deadcode] Function 'test' has dead code:
  on line 1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1867-1867)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1333-1333)
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1335-1335)
  on line 1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1337-1337)
  on line 1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1347-1347)
  on line 1349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1349-1349)
  on line 1351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1351-1351)
  on line 1361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1361-1361)
  on line 1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1363-1363)
  on line 1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1365-1365)
  on line 1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1375-1375)
  on line 1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1377-1377)
  on line 1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1379-1379)
  on line 1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1389-1389)
  on line 1391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1391-1391)
  on line 1393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1393-1393)
  on line 1403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1403-1403)
  on line 1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1405-1405)
  on line 1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1407-1407)
  on lines 1434..1435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1434-1435)
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1437-1437)
  on lines 1439..1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1439-1440)
  on line 1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1444-1444)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 83 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:83-83)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 288
  dead: 1081 (602 in uncalled functions)
  total lines: 1369
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:198:17-198:28)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2862:17-2862:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2494:7-2494:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2674:7-2674:17)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1331:9-1331:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:451:7-451:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2865:19-2865:30)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:454:9-454:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2868:21-2868:32)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:217:7-217:18)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1345:9-1345:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:457:11-457:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:460:13-460:25)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:221:9-221:20)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1359:9-1359:18)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:225:11-225:22)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:479:7-479:19)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1117:7-1117:26)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:229:13-229:24)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1373:9-1373:18)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2702:11-2702:22)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:482:9-482:21)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1121:9-1121:12)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:233:15-233:26)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2705:13-2705:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2527:9-2527:19)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1387:9-1387:18)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2708:15-2708:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:237:17-237:28)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1133:7-1133:26)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:712:7-712:15)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2711:17-2711:28)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1401:9-1401:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:716:9-716:12)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2714:19-2714:30)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2717:21-2717:32)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:722:9-722:27)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2728:11-2728:21)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1420:9-1420:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1157:9-1157:12)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:525:7-525:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2548:21-2548:32)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1428:9-1428:16)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:738:11-738:29)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1177:7-1177:10)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:751:13-751:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:752:15-752:32)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2755:13-2755:23)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:756:17-756:24)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:343:7-343:13)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:111:9-111:16)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2207:7-2207:10)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:346:9-346:15)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:117:11-117:18)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1231:7-1231:14)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2782:15-2782:25)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:349:11-349:17)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2783:17-2783:28)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:139:7-139:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2411:11-2411:23)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:352:13-352:19)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:355:15-355:21)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:143:9-143:20)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2415:13-2415:25)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1244:7-1244:14)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:358:17-358:23)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:147:11-147:22)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2419:15-2419:27)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:151:13-151:24)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1257:7-1257:14)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:155:15-155:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2438:7-2438:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2825:7-2825:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2441:9-2441:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:159:17-159:28)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1270:7-1270:14)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1283:7-1283:14)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1060:7-1060:14)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:182:9-182:20)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2466:7-2466:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:186:11-186:22)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:1296:7-1296:15)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2852:9-2852:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2472:11-2472:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2853:11-2853:22)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:190:13-190:24)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2475:13-2475:25)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2856:13-2856:24)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:194:15-194:26)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2478:15-2478:27)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product28.cil.c:2859:15-2859:26)
[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)
