./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/elevator_spec1_product26.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/elevator_spec1_product26.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_spec1_product26.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_spec1_product26.cil.c:1443:5-1501:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1518:9-1576:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1670:3-1691:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1727:3-1752:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1812:5-1832:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2018:3-2037:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2065:3-2084:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2534:3-2562:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2594:3-2637:3 with factor 1
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:103:1-125:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:126:1-148:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:202:1-233:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:234:1-245:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:246:1-265:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:374:1-382:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:383:1-422:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:868:1-901:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:958:1-971:1)
[Warning][Deadcode] Function 'printState__wrappee__empty' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1240:1-1410:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1411:1-1432:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1433:1-1591:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1599:1-1644:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1645:1-1700:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1701:1-1760:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1763:1-1865:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1866:1-1911:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1912:1-1957:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1963:1-1972:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2000:1-2042:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2043:1-2089:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2392:1-2443:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2444:1-2454:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2455:1-2465:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2477:1-2487:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2488:1-2498:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2510:1-2521:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2568:1-2645:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2646:1-2657:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2658:1-2669:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2670:1-2680:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2681:1-2697:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2786:1-2827:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2746-2746)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__2' has dead code:
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2232-2232)
  on lines 2240..2241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2240-2241)
  on lines 2243..2244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2243-2244)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__3' has dead code:
  on line 2270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2270-2270)
  on line 2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2272-2272)
  on lines 2274..2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2274-2275)
  on line 2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2300-2300)
  on line 2302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2302-2302)
  on lines 2304..2305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2304-2305)
  on line 2315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2315-2315)
  on line 2317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2317-2317)
  on lines 2319..2320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2319-2320)
  on line 2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2330-2330)
  on line 2332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2332-2332)
  on lines 2334..2335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2334-2335)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__4' has dead code:
  on line 2358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2358-2358)
  on line 2363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2363-2363)
  on line 2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2371-2371)
  on line 2373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2373-2373)
  on line 2376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2376-2376)
  on line 2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2378-2378)
  on line 2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2387-2387)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 436..437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:436-437)
  on lines 440..441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:440-441)
  on lines 451..452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:451-452)
  on lines 461..463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:461-463)
  on line 466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:466-466)
  on lines 468..470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:468-470)
  on lines 472..474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:472-474)
  on line 477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:477-477)
  on lines 479..481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:479-481)
  on lines 483..485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:483-485)
  on lines 498..500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:498-500)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:337-337)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 348..350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:348-350)
  on lines 352..354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:352-354)
  on lines 356..358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:356-358)
  on lines 360..362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:360-362)
  on lines 364..365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:364-365)
  on line 371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:371-371)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2900-2900)
  on lines 2908..2909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2908-2909)
  on lines 2911..2912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2911-2912)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 2555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2555-2555)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:912-912)
  on lines 917..918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:917-918)
  on line 926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:926-926)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:163-163)
  on line 166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:166-166)
  on line 169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:169-169)
  on line 172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:172-172)
  on line 175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:175-175)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:328-328)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 2174..2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2174-2175)
  on lines 2178..2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2178-2179)
  on lines 2182..2183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2182-2183)
  on lines 2186..2187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2186-2187)
  on lines 2190..2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2190-2191)
  on lines 2197..2198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2197-2198)
  on line 2205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2205-2205)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 2135..2136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2135-2136)
  on lines 2139..2140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2139-2140)
  on lines 2147..2148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2147-2148)
  on lines 2151..2152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2151-2152)
  on lines 2158..2159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2158-2159)
  on line 2166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2166-2166)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 2096..2097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2096-2097)
  on lines 2100..2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2100-2101)
  on lines 2104..2105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2104-2105)
  on lines 2108..2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2108-2109)
  on lines 2112..2113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2112-2113)
  on lines 2119..2120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2119-2120)
  on line 2127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2127-2127)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 3108..3109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3108-3109)
  on lines 3111..3112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3111-3112)
  on lines 3114..3115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3114-3115)
  on lines 3117..3118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3117-3118)
  on lines 3120..3121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3120-3121)
  on lines 3123..3124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3123-3124)
  on line 3136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3136-3136)
  on line 3139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3139-3139)
  on line 3142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3142-3142)
  on line 3145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3145-3145)
  on line 3148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3148-3148)
  on line 3163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3163-3163)
  on line 3166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3166-3166)
  on lines 3171..3172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3171-3172)
  on lines 3174..3175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3174-3175)
  on lines 3177..3178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3177-3178)
  on lines 3188..3190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3188-3190)
  on lines 3192..3193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3192-3193)
  on lines 3195..3196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3195-3196)
  on lines 3198..3199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3198-3199)
  on lines 3201..3202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3201-3202)
  on lines 3204..3205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3204-3205)
  on lines 3215..3217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3215-3217)
  on lines 3219..3220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3219-3220)
  on lines 3222..3223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3222-3223)
  on lines 3225..3226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3225-3226)
  on lines 3228..3229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3228-3229)
  on lines 3231..3232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3231-3232)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:155-155)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2844..2846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2844-2846)
  on lines 2848..2850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2848-2850)
  on lines 2858..2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2858-2860)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:513-513)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2928..2930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2928-2930)
  on lines 2932..2934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2932-2934)
  on lines 2936..2938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2936-2938)
  on lines 2940..2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2940-2942)
  on lines 2944..2946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2944-2946)
  on lines 2948..2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2948-2950)
  on lines 2993..2996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2993-2996)
  on lines 2998..3000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2998-3000)
  on lines 3002..3004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3002-3004)
  on lines 3006..3008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3006-3008)
  on lines 3010..3012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3010-3012)
  on lines 3014..3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3014-3016)
  on lines 3026..3029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3026-3029)
  on lines 3031..3033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3031-3033)
  on lines 3035..3037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3035-3037)
  on lines 3039..3041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3039-3041)
  on lines 3043..3045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3043-3045)
  on lines 3047..3049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3047-3049)
  on lines 3059..3062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3059-3062)
  on lines 3064..3066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3064-3066)
  on lines 3068..3070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3068-3070)
  on lines 3072..3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3072-3074)
  on lines 3076..3078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3076-3078)
  on lines 3080..3082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3080-3082)
  on lines 3098..3100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3098-3100)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 3411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3411-3411)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 2735..2737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2735-2737)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:271-271)
  on line 274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:274-274)
  on line 277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:277-277)
  on lines 282..283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:282-283)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 992..995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:992-995)
  on lines 1005..1008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1005-1008)
  on lines 1018..1021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1018-1021)
  on lines 1031..1034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1031-1034)
  on lines 1044..1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1044-1047)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 3259..3260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3259-3260)
  on lines 3262..3263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3262-3263)
  on lines 3265..3266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3265-3266)
  on lines 3268..3269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3268-3269)
  on lines 3271..3272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3271-3272)
  on lines 3274..3275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3274-3275)
  on line 3287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3287-3287)
  on line 3290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3290-3290)
  on line 3293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3293-3293)
  on line 3296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3296-3296)
  on line 3299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3299-3299)
  on lines 3312..3314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3312-3314)
  on lines 3316..3317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3316-3317)
  on lines 3319..3320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3319-3320)
  on lines 3322..3323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3322-3323)
  on lines 3325..3326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3325-3326)
  on lines 3328..3329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3328-3329)
  on lines 3339..3341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3339-3341)
  on lines 3343..3344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3343-3344)
  on lines 3346..3347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3346-3347)
  on lines 3349..3350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3349-3350)
  on lines 3352..3353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3352-3353)
  on lines 3355..3356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3355-3356)
  on lines 3366..3368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3366-3368)
  on lines 3370..3371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3370-3371)
  on lines 3373..3374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3373-3374)
  on lines 3376..3377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3376-3377)
  on lines 3379..3380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3379-3380)
  on lines 3382..3383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3382-3383)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2868-2868)
  on lines 2873..2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2873-2874)
  on lines 2876..2877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2876-2877)
  on lines 2879..2880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2879-2880)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:299-299)
  on lines 304..305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:304-305)
  on lines 307..308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:307-308)
  on lines 310..311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:310-311)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2714-2714)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on lines 948..949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:948-949)
  on line 955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:955-955)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 536..537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:536-537)
  on line 542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:542-542)
  on line 544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:544-544)
  on lines 546..548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:546-548)
  on lines 558..561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:558-561)
  on lines 586..590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:586-590)
  on lines 599..600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:599-600)
  on line 602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:602-602)
  on lines 604..606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:604-606)
  on lines 615..619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:615-619)
  on lines 628..629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:628-629)
  on line 631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:631-631)
  on lines 633..635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:633-635)
  on lines 644..648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:644-648)
  on lines 657..658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:657-658)
  on line 660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:660-660)
  on lines 662..664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:662-664)
  on lines 673..677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:673-677)
  on lines 679..680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:679-680)
  on lines 683..684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:683-684)
  on lines 687..688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:687-688)
  on lines 700..702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:700-702)
  on lines 706..707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:706-707)
  on line 709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:709-709)
  on lines 711..713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:711-713)
  on lines 722..726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:722-726)
  on lines 735..736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:735-736)
  on line 738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:738-738)
  on lines 740..742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:740-742)
  on lines 751..755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:751-755)
  on lines 764..765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:764-765)
  on line 767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:767-767)
  on lines 769..771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:769-771)
  on lines 780..784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:780-784)
  on lines 793..794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:793-794)
  on line 796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:796-796)
  on lines 798..800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:798-800)
  on lines 809..813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:809-813)
  on lines 822..823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:822-823)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:825-825)
  on lines 827..829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:827-829)
  on lines 838..842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:838-842)
  on lines 844..845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:844-845)
  on lines 848..849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:848-849)
  on lines 852..853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:852-853)
  on line 865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:865-865)
[Warning][Deadcode] Function 'timeShift__wrappee__empty' has dead code:
  on line 1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1092-1092)
  on line 1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1094-1094)
  on line 1096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1096-1096)
  on line 1106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1106-1106)
  on line 1108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1108-1108)
  on line 1110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1110-1110)
  on line 1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1120-1120)
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1122-1122)
  on line 1124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1124-1124)
  on line 1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1134-1134)
  on line 1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1136-1136)
  on line 1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1138-1138)
  on line 1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1148-1148)
  on line 1150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1150-1150)
  on line 1152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1152-1152)
  on line 1162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1162-1162)
  on line 1164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1164-1164)
  on line 1166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1166-1166)
  on lines 1193..1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1193-1194)
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1196-1196)
  on lines 1198..1199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1198-1199)
  on line 1203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1203-1203)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1993-1993)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 320
  dead: 1073 (561 in uncalled functions)
  total lines: 1393
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:439:9-439:23)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1104:9-1104:18)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1118:9-1118:18)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2231:7-2231:17)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:450:13-450:27)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1132:9-1132:18)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2237:11-2237:21)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:457:15-457:22)
[Warning][Deadcode][CWE-571] condition 'floorID == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2840:11-2840:23)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1146:9-1146:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:270:7-270:19)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1160:9-1160:18)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2269:7-2269:17)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:907:7-907:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:273:9-273:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2534:10-2534:11)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:911:9-911:12)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:276:11-276:23)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2538:9-2538:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2867:7-2867:19)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:279:13-279:25)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1179:9-1179:23)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2542:11-2542:23)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2284:9-2284:19)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:923:7-923:26)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2870:9-2870:21)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1187:9-1187:16)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3258:7-3258:17)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:298:7-298:19)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2554:9-2554:12)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:301:9-301:21)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2299:11-2299:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2095:7-2095:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2534:10-2534:11)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2099:9-2099:20)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:947:9-947:12)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:531:7-531:15)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2538:9-2538:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2899:7-2899:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2103:11-2103:22)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2314:13-2314:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:535:9-535:12)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2542:11-2542:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2107:13-2107:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3285:9-3285:19)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:541:9-541:27)
[Warning][Deadcode][CWE-571] condition 'floorID == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2905:11-2905:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3286:11-3286:22)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2554:9-2554:12)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2111:15-2111:26)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3289:13-3289:24)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2329:15-2329:25)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:344:7-344:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2115:17-2115:28)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3292:15-3292:26)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2534:10-2534:11)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:990:7-990:14)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3295:17-3295:28)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:557:11-557:29)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2927:7-2927:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3107:7-3107:17)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2538:9-2538:23)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2356:7-2356:28)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3298:19-3298:30)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2134:7-2134:18)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2542:11-2542:23)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2361:9-2361:30)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3301:21-3301:32)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1003:7-1003:14)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:570:13-570:31)
[Warning][Deadcode][CWE-571] condition 'landingButtons_spc1_2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2366:11-2366:32)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2138:9-2138:20)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:571:15-571:32)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:575:17-575:24)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1016:7-1016:14)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2146:13-2146:24)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2727:7-2727:10)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2150:15-2150:26)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3135:11-3135:22)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1029:7-1029:14)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3138:13-3138:24)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2154:17-2154:28)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2960:9-2960:19)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:162:7-162:13)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3141:15-3141:26)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:165:9-165:15)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3144:17-3144:28)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:168:11-168:17)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2173:7-2173:18)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1042:7-1042:14)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3147:19-3147:30)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:171:13-171:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3150:21-3150:32)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2177:9-2177:20)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:174:15-174:21)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3161:11-3161:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3162:13-3162:24)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:177:17-177:23)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2181:11-2181:22)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1055:7-1055:15)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3165:15-3165:26)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2185:13-2185:24)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:3168:17-3168:28)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2981:21-2981:32)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2189:15-2189:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:2193:17-2193:28)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:435:7-435:14)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product26.cil.c:1090:9-1090:18)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
