./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/elevator_spec3_product19.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/elevator_spec3_product19.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:198:3-226:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:260:3-303:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:501:3-522:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:558:3-583:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:643:5-663:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2160:5-2218:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2235:9-2293:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2697:3-2716:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2744:3-2763:3 with factor 5
[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 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:51:1-102:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:116:1-126:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:127:1-137:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:138:1-148:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:149:1-159:1)
[Warning][Deadcode] Function 'bigMacCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:160:1-170:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:234:1-311:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:312:1-323:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:324:1-335:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:336:1-346:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:347:1-363:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:430:1-475:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:476:1-531:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:532:1-591:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:594:1-696:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:697:1-742:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:743:1-788:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:848:1-870:1)
[Warning][Deadcode] Function 'isBlocked' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:871:1-879:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:924:1-955:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:956:1-967:1)
[Warning][Deadcode] Function 'areDoorsOpen' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1033:1-1041:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1085:1-1124:1)
[Warning][Deadcode] Function 'anyStopRequested' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1125:1-1204:1)
[Warning][Deadcode] Function 'isIdle' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1205:1-1217:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1599:1-1632:1)
[Warning][Deadcode] Function 'printState' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1979:1-2149:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2150:1-2308:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2320:1-2328:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2449:1-2458:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2679:1-2721:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2722:1-2768:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2675-2675)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__1' has dead code:
  on line 2508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2508-2508)
  on line 2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2510-2510)
  on lines 2512..2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2512-2513)
  on line 2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2519-2519)
  on line 2521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2521-2521)
  on lines 2523..2524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2523-2524)
  on line 2530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2530-2530)
  on line 2532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2532-2532)
  on lines 2534..2535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2534-2535)
  on line 2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2541-2541)
  on line 2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2543-2543)
  on lines 2545..2546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2545-2546)
  on line 2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2552-2552)
  on line 2554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2554-2554)
  on lines 2556..2557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2556-2557)
  on line 2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2585-2585)
  on line 2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2596-2596)
  on line 2607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2607-2607)
  on line 2615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2615-2615)
  on lines 2617..2618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2617-2618)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__2' has dead code:
  on line 2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2653-2653)
  on line 2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2655-2655)
  on line 2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2657-2657)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1066..1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1066-1067)
  on line 1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1073-1073)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2916-2916)
  on line 2919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2919-2919)
  on line 2922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2922-2922)
  on line 2925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2925-2925)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:195-195)
  on line 198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:198-198)
  on lines 201..202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:201-202)
  on line 204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:204-204)
  on line 206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:206-206)
  on line 216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:216-216)
  on lines 218..219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:218-219)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:222-222)
  on line 225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:225-225)
  on line 229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:229-229)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 1643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1643-1643)
  on line 1649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1649-1649)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on lines 887..888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:887-888)
  on lines 890..891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:890-891)
  on lines 893..894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:893-894)
  on lines 896..897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:896-897)
  on lines 899..900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:899-900)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1030-1030)
[Warning][Deadcode] Function 'getCurrentHeading' has dead code:
  on line 1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1082-1082)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 2416..2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2416-2418)
  on lines 2420..2422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2420-2422)
  on lines 2424..2426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2424-2426)
  on lines 2428..2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2428-2430)
  on lines 2432..2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2432-2434)
  on lines 2436..2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2436-2437)
  on line 2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2444-2444)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 2377..2379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2377-2379)
  on lines 2381..2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2381-2383)
  on lines 2385..2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2385-2387)
  on lines 2389..2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2389-2391)
  on lines 2393..2395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2393-2395)
  on lines 2397..2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2397-2398)
  on line 2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2405-2405)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on lines 1728..1729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1728-1729)
  on line 1731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1731-1731)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 2338..2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2338-2340)
  on lines 2342..2344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2342-2344)
  on lines 2346..2348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2346-2348)
  on lines 2350..2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2350-2352)
  on lines 2354..2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2354-2356)
  on lines 2358..2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2358-2359)
  on line 2366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2366-2366)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 3124..3125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3124-3125)
  on lines 3127..3128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3127-3128)
  on lines 3130..3131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3130-3131)
  on lines 3133..3134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3133-3134)
  on lines 3136..3137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3136-3137)
  on lines 3139..3140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3139-3140)
  on lines 3151..3152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3151-3152)
  on lines 3154..3155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3154-3155)
  on lines 3157..3158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3157-3158)
  on lines 3160..3161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3160-3161)
  on lines 3163..3164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3163-3164)
  on lines 3166..3167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3166-3167)
  on lines 3178..3179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3178-3179)
  on lines 3181..3182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3181-3182)
  on lines 3184..3185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3184-3185)
  on lines 3187..3188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3187-3188)
  on lines 3190..3191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3190-3191)
  on lines 3193..3194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3193-3194)
  on lines 3205..3206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3205-3206)
  on lines 3208..3209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3208-3209)
  on lines 3211..3212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3211-3212)
  on lines 3214..3215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3214-3215)
  on lines 3217..3218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3217-3218)
  on lines 3220..3221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3220-3221)
  on lines 3235..3236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3235-3236)
  on lines 3238..3239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3238-3239)
  on lines 3241..3242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3241-3242)
  on lines 3244..3245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3244-3245)
  on lines 3247..3248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3247-3248)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 2317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2317-2317)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2857..2858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2857-2858)
  on lines 2861..2862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2861-2862)
  on lines 2878..2880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2878-2880)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2944..2946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2944-2946)
  on lines 2948..2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2948-2950)
  on lines 2952..2954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2952-2954)
  on lines 2956..2958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2956-2958)
  on lines 2960..2962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2960-2962)
  on lines 2964..2966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2964-2966)
  on lines 2977..2979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2977-2979)
  on lines 2981..2983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2981-2983)
  on lines 2985..2987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2985-2987)
  on lines 2989..2991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2989-2991)
  on lines 2993..2995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2993-2995)
  on lines 2997..2999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2997-2999)
  on lines 3010..3012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3010-3012)
  on lines 3014..3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3014-3016)
  on lines 3018..3020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3018-3020)
  on lines 3022..3024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3022-3024)
  on lines 3026..3028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3026-3028)
  on lines 3030..3032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3030-3032)
  on lines 3043..3045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3043-3045)
  on lines 3047..3049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3047-3049)
  on lines 3051..3053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3051-3053)
  on lines 3055..3057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3055-3057)
  on lines 3059..3061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3059-3061)
  on lines 3063..3065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3063-3065)
  on lines 3114..3116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3114-3116)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 3427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3427-3427)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 403..405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:403-405)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on lines 975..976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:975-976)
  on lines 978..979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:978-979)
  on lines 981..982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:981-982)
  on lines 984..985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:984-985)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1767..1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1767-1770)
  on lines 1780..1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1780-1783)
  on lines 1793..1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1793-1796)
  on lines 1806..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1806-1809)
  on lines 1819..1822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1819-1822)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 3275..3276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3275-3276)
  on lines 3278..3279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3278-3279)
  on lines 3281..3282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3281-3282)
  on lines 3284..3285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3284-3285)
  on lines 3287..3288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3287-3288)
  on lines 3290..3291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3290-3291)
  on lines 3302..3303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3302-3303)
  on lines 3305..3306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3305-3306)
  on lines 3308..3309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3308-3309)
  on lines 3311..3312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3311-3312)
  on lines 3314..3315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3314-3315)
  on lines 3317..3318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3317-3318)
  on lines 3329..3330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3329-3330)
  on lines 3332..3333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3332-3333)
  on lines 3335..3336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3335-3336)
  on lines 3338..3339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3338-3339)
  on lines 3341..3342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3341-3342)
  on lines 3344..3345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3344-3345)
  on lines 3356..3357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3356-3357)
  on lines 3359..3360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3359-3360)
  on lines 3362..3363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3362-3363)
  on lines 3365..3366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3365-3366)
  on lines 3368..3369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3368-3369)
  on lines 3371..3372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3371-3372)
  on lines 3386..3387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3386-3387)
  on lines 3389..3390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3389-3390)
  on lines 3392..3393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3392-3393)
  on lines 3395..3396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3395-3396)
  on lines 3398..3399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3398-3399)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2888-2888)
  on line 2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2891-2891)
  on line 2894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2894-2894)
  on line 2897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2897-2897)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1001-1001)
  on line 1004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1004-1004)
  on line 1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1007-1007)
  on line 1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1010-1010)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:379-379)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1717-1717)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__weight' has dead code:
  on lines 1679..1680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1679-1680)
  on line 1686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1686-1686)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1596-1596)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__weight' has dead code:
  on line 1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1235-1235)
  on lines 1237..1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1237-1239)
  on lines 1243..1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1243-1244)
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1246-1246)
  on lines 1248..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1248-1250)
  on lines 1259..1263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1259-1263)
  on lines 1272..1273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1272-1273)
  on line 1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1275-1275)
  on lines 1277..1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1277-1279)
  on lines 1288..1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1288-1292)
  on lines 1301..1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1301-1302)
  on line 1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1304-1304)
  on lines 1306..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1306-1308)
  on lines 1317..1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1317-1321)
  on lines 1330..1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1330-1331)
  on line 1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1333-1333)
  on lines 1335..1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1335-1337)
  on lines 1346..1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1346-1350)
  on lines 1359..1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1359-1360)
  on line 1362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1362-1362)
  on lines 1364..1366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1364-1366)
  on lines 1375..1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1375-1379)
  on lines 1381..1382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1381-1382)
  on lines 1385..1386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1385-1386)
  on lines 1389..1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1389-1390)
  on lines 1403..1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1403-1404)
  on lines 1414..1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1414-1415)
  on lines 1437..1438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1437-1438)
  on line 1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1440-1440)
  on lines 1442..1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1442-1444)
  on lines 1453..1457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1453-1457)
  on lines 1466..1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1466-1467)
  on line 1469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1469-1469)
  on lines 1471..1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1471-1473)
  on lines 1482..1486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1482-1486)
  on lines 1495..1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1495-1496)
  on line 1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1498-1498)
  on lines 1500..1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1500-1502)
  on lines 1511..1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1511-1515)
  on lines 1524..1525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1524-1525)
  on line 1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1527-1527)
  on lines 1529..1531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1529-1531)
  on lines 1540..1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1540-1544)
  on lines 1546..1547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1546-1547)
  on lines 1550..1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1550-1551)
  on lines 1554..1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1554-1555)
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1567-1567)
[Warning][Deadcode] Function 'test' has dead code:
  on line 420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:420-420)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 1857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1857-1857)
  on line 1859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1859-1859)
  on line 1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1861-1861)
  on line 1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1871-1871)
  on line 1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1873-1873)
  on line 1875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1875-1875)
  on line 1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1885-1885)
  on line 1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1887-1887)
  on line 1889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1889-1889)
  on line 1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1899-1899)
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1901-1901)
  on line 1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1903-1903)
  on line 1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1913-1913)
  on line 1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1915-1915)
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1917-1917)
  on line 1927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1927-1927)
  on line 1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1929-1929)
  on line 1931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1931-1931)
  on line 1968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1968-1968)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2479-2479)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 352
  dead: 1042 (536 in uncalled functions)
  total lines: 1394
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2595:15-2595:22)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2373:7-2373:18)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1752:7-1752:14)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2602:15-2602:37)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3204:13-3204:23)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2606:17-2606:24)
[Warning][Deadcode][CWE-571] condition 'p == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:884:7-884:13)
[Warning][Deadcode][CWE-570] condition 'currentFloorID___0 > 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2613:17-2613:39)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1765:7-1765:14)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1778:7-1778:14)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3042:13-3042:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2856:9-2856:21)
[Warning][Deadcode][CWE-570] condition 'expectedDirection == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2651:9-2651:31)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3231:15-3231:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3232:17-3232:28)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1791:7-1791:14)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2860:11-2860:23)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2412:7-2412:18)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1804:7-1804:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2868:15-2868:27)
[Warning][Deadcode][CWE-570] condition 'tmp___10' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1817:7-1817:15)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2887:7-2887:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3274:7-3274:17)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2890:9-2890:21)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3075:15-3075:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2893:11-2893:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2896:13-2896:25)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:395:7-395:10)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2899:15-2899:27)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1855:9-1855:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:972:7-972:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2915:7-2915:19)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1402:9-1402:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2918:9-2918:21)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1869:9-1869:18)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1408:9-1408:27)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1409:11-1409:28)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3301:9-3301:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2921:11-2921:23)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1413:13-1413:20)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3096:27-3096:38)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2924:13-2924:25)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1883:9-1883:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2927:15-2927:27)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1000:7-1000:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1424:11-1424:29)
[Warning][Deadcode][CWE-570] condition 'tmp___10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2507:7-2507:20)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1897:9-1897:18)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1425:13-1425:31)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2943:7-2943:17)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1642:9-1642:12)
[Warning][Deadcode][CWE-571] condition 'floorButtons_0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1426:15-1426:29)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1003:9-1003:21)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3123:7-3123:17)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1648:9-1648:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1006:11-1006:23)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1911:9-1911:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1009:13-1009:25)
[Warning][Deadcode][CWE-570] condition 'dir == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1233:7-1233:15)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3328:11-3328:21)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1012:15-1012:27)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1925:9-1925:18)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3150:9-3150:19)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1678:9-1678:12)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2976:9-2976:19)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2334:7-2334:18)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3355:13-3355:23)
[Warning][Deadcode][CWE-571] condition 'tmp___7' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1961:11-1961:18)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2569:9-2569:31)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1062:15-1062:27)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3177:11-3177:21)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2580:11-2580:33)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2584:13-2584:20)
[Warning][Deadcode][CWE-571] condition 'ofHeading == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:1724:7-1724:21)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3382:15-3382:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3383:17-3383:28)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:2591:13-2591:35)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product19.cil.c:3009:11-3009:21)
[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)
