./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_spec3_product24.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_spec3_product24.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_product24.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_product24.cil.c:217:3-245:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:278:3-321:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:569:3-588:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:616:3-635:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2121:5-2179:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2196:9-2254:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3216:3-3237:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3273:3-3298:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3358:5-3378:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:70:1-121:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:135:1-145:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:146:1-156:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:157:1-167:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:168:1-178:1)
[Warning][Deadcode] Function 'bigMacCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:179:1-189:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:252:1-329:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:330:1-341:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:342:1-353:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:354:1-364:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:365:1-381:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:551:1-593:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:594:1-640:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:694:1-716:1)
[Warning][Deadcode] Function 'isBlocked' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:717:1-725:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:770:1-801:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:802:1-813:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:931:1-970:1)
[Warning][Deadcode] Function 'anyStopRequested' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:971:1-1050:1)
[Warning][Deadcode] Function 'isIdle' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1051:1-1063:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1918:1-2088:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2089:1-2110:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2111:1-2269:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2281:1-2289:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3145:1-3190:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3191:1-3246:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3247:1-3306:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3309:1-3411:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3412:1-3457:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3458:1-3503:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3506:1-3515:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3545-3545)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__1' has dead code:
  on line 2977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2977-2977)
  on line 2979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2979-2979)
  on lines 2981..2982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2981-2982)
  on line 2988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2988-2988)
  on line 2990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2990-2990)
  on lines 2992..2993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2992-2993)
  on line 2999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2999-2999)
  on line 3001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3001-3001)
  on lines 3003..3004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3003-3004)
  on line 3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3010-3010)
  on line 3012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3012-3012)
  on lines 3014..3015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3014-3015)
  on line 3021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3021-3021)
  on line 3023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3023-3023)
  on lines 3025..3026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3025-3026)
  on line 3054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3054-3054)
  on line 3065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3065-3065)
  on line 3076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3076-3076)
  on line 3084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3084-3084)
  on lines 3086..3087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3086-3087)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__2' has dead code:
  on line 3122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3122-3122)
  on line 3124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3124-3124)
  on line 3126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3126-3126)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:885-885)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 912..913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:912-913)
  on line 919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:919-919)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2437-2437)
  on line 2440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2440-2440)
  on line 2443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2443-2443)
  on line 2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2446-2446)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:214-214)
  on line 217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:217-217)
  on lines 220..221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:220-221)
  on line 223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:223-223)
  on line 225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:225-225)
  on line 235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:235-235)
  on lines 237..238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:237-238)
  on line 241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:241-241)
  on line 244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:244-244)
  on line 248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:248-248)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 1529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1529-1529)
  on line 1535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1535-1535)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on lines 733..734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:733-734)
  on lines 736..737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:736-737)
  on lines 739..740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:739-740)
  on lines 742..743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:742-743)
  on lines 745..746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:745-746)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:876-876)
[Warning][Deadcode] Function 'getCurrentHeading' has dead code:
  on line 928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:928-928)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 514..516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:514-516)
  on lines 518..520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:518-520)
  on lines 522..524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:522-524)
  on lines 526..528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:526-528)
  on lines 530..532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:530-532)
  on lines 534..535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:534-535)
  on line 542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:542-542)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 475..477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:475-477)
  on lines 479..481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:479-481)
  on lines 483..485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:483-485)
  on lines 487..489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:487-489)
  on lines 491..493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:491-493)
  on lines 495..496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:495-496)
  on line 503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:503-503)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on lines 1642..1643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1642-1643)
  on line 1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1645-1645)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 436..438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:436-438)
  on lines 440..442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:440-442)
  on lines 444..446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:444-446)
  on lines 448..450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:448-450)
  on lines 452..454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:452-454)
  on lines 456..457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:456-457)
  on line 464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:464-464)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 2645..2646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2645-2646)
  on lines 2648..2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2648-2649)
  on lines 2651..2652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2651-2652)
  on lines 2654..2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2654-2655)
  on lines 2657..2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2657-2658)
  on lines 2660..2661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2660-2661)
  on lines 2672..2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2672-2673)
  on lines 2675..2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2675-2676)
  on lines 2678..2679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2678-2679)
  on lines 2681..2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2681-2682)
  on lines 2684..2685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2684-2685)
  on lines 2687..2688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2687-2688)
  on lines 2699..2700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2699-2700)
  on lines 2702..2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2702-2703)
  on lines 2705..2706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2705-2706)
  on lines 2708..2709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2708-2709)
  on lines 2711..2712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2711-2712)
  on lines 2714..2715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2714-2715)
  on lines 2726..2727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2726-2727)
  on lines 2729..2730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2729-2730)
  on lines 2732..2733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2732-2733)
  on lines 2735..2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2735-2736)
  on lines 2738..2739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2738-2739)
  on lines 2741..2742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2741-2742)
  on lines 2756..2757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2756-2757)
  on lines 2759..2760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2759-2760)
  on lines 2762..2763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2762-2763)
  on lines 2765..2766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2765-2766)
  on lines 2768..2769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2768-2769)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 1493..1495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1493-1495)
  on lines 1497..1499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1497-1499)
  on lines 1501..1503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1501-1503)
  on lines 1505..1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1505-1507)
  on lines 1509..1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1509-1510)
  on line 1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1516-1516)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 2278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2278-2278)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2378..2379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2378-2379)
  on lines 2382..2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2382-2383)
  on lines 2399..2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2399-2401)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2465..2467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2465-2467)
  on lines 2469..2471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2469-2471)
  on lines 2473..2475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2473-2475)
  on lines 2477..2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2477-2479)
  on lines 2481..2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2481-2483)
  on lines 2485..2487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2485-2487)
  on lines 2498..2500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2498-2500)
  on lines 2502..2504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2502-2504)
  on lines 2506..2508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2506-2508)
  on lines 2510..2512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2510-2512)
  on lines 2514..2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2514-2516)
  on lines 2518..2520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2518-2520)
  on lines 2531..2533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2531-2533)
  on lines 2535..2537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2535-2537)
  on lines 2539..2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2539-2541)
  on lines 2543..2545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2543-2545)
  on lines 2547..2549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2547-2549)
  on lines 2551..2553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2551-2553)
  on lines 2564..2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2564-2566)
  on lines 2568..2570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2568-2570)
  on lines 2572..2574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2572-2574)
  on lines 2576..2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2576-2578)
  on lines 2580..2582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2580-2582)
  on lines 2584..2586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2584-2586)
  on lines 2635..2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2635-2637)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 2948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2948-2948)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 420..422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:420-422)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on lines 821..822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:821-822)
  on lines 824..825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:824-825)
  on lines 827..828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:827-828)
  on lines 830..831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:830-831)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1681..1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1681-1684)
  on lines 1694..1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1694-1697)
  on lines 1707..1710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1707-1710)
  on lines 1720..1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1720-1723)
  on lines 1733..1736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1733-1736)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 2796..2797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2796-2797)
  on lines 2799..2800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2799-2800)
  on lines 2802..2803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2802-2803)
  on lines 2805..2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2805-2806)
  on lines 2808..2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2808-2809)
  on lines 2811..2812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2811-2812)
  on lines 2823..2824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2823-2824)
  on lines 2826..2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2826-2827)
  on lines 2829..2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2829-2830)
  on lines 2832..2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2832-2833)
  on lines 2835..2836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2835-2836)
  on lines 2838..2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2838-2839)
  on lines 2850..2851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2850-2851)
  on lines 2853..2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2853-2854)
  on lines 2856..2857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2856-2857)
  on lines 2859..2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2859-2860)
  on lines 2862..2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2862-2863)
  on lines 2865..2866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2865-2866)
  on lines 2877..2878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2877-2878)
  on lines 2880..2881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2880-2881)
  on lines 2883..2884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2883-2884)
  on lines 2886..2887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2886-2887)
  on lines 2889..2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2889-2890)
  on lines 2892..2893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2892-2893)
  on lines 2907..2908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2907-2908)
  on lines 2910..2911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2910-2911)
  on lines 2913..2914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2913-2914)
  on lines 2916..2917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2916-2917)
  on lines 2919..2920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2919-2920)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2409-2409)
  on line 2412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2412-2412)
  on line 2415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2415-2415)
  on line 2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2418-2418)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:847-847)
  on line 850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:850-850)
  on line 853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:853-853)
  on line 856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:856-856)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:396-396)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1631-1631)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__twothirdsfull' has dead code:
  on lines 1588..1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1588-1590)
  on line 1592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1592-1592)
  on line 1600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1600-1600)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__weight' has dead code:
  on lines 1565..1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1565-1566)
  on line 1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1572-1572)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1482-1482)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__twothirdsfull' has dead code:
  on line 1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1434-1434)
  on line 1436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1436-1436)
  on line 1438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1438-1438)
  on line 1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1441-1441)
  on line 1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1444-1444)
  on line 1453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1453-1453)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__weight' has dead code:
  on line 1081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1081-1081)
  on lines 1083..1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1083-1085)
  on lines 1089..1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1089-1090)
  on line 1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1092-1092)
  on lines 1094..1096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1094-1096)
  on lines 1105..1109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1105-1109)
  on lines 1118..1119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1118-1119)
  on line 1121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1121-1121)
  on lines 1123..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1123-1125)
  on lines 1134..1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1134-1138)
  on lines 1147..1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1147-1148)
  on line 1150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1150-1150)
  on lines 1152..1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1152-1154)
  on lines 1163..1167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1163-1167)
  on lines 1176..1177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1176-1177)
  on line 1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1179-1179)
  on lines 1181..1183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1181-1183)
  on lines 1192..1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1192-1196)
  on lines 1205..1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1205-1206)
  on line 1208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1208-1208)
  on lines 1210..1212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1210-1212)
  on lines 1221..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1221-1225)
  on lines 1227..1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1227-1228)
  on lines 1231..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1231-1232)
  on lines 1235..1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1235-1236)
  on lines 1249..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1249-1250)
  on lines 1260..1261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1260-1261)
  on lines 1283..1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1283-1284)
  on line 1286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1286-1286)
  on lines 1288..1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1288-1290)
  on lines 1299..1303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1299-1303)
  on lines 1312..1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1312-1313)
  on line 1315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1315-1315)
  on lines 1317..1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1317-1319)
  on lines 1328..1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1328-1332)
  on lines 1341..1342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1341-1342)
  on line 1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1344-1344)
  on lines 1346..1348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1346-1348)
  on lines 1357..1361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1357-1361)
  on lines 1370..1371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1370-1371)
  on line 1373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1373-1373)
  on lines 1375..1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1375-1377)
  on lines 1386..1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1386-1390)
  on lines 1392..1393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1392-1393)
  on lines 1396..1397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1396-1397)
  on lines 1400..1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1400-1401)
  on line 1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1413-1413)
[Warning][Deadcode] Function 'test' has dead code:
  on line 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:64-64)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1899-1899)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 1768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1768-1768)
  on line 1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1770-1770)
  on line 1772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1772-1772)
  on line 1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1782-1782)
  on line 1784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1784-1784)
  on line 1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1786-1786)
  on line 1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1796-1796)
  on line 1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1798-1798)
  on line 1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1800-1800)
  on line 1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1810-1810)
  on line 1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1812-1812)
  on line 1814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1814-1814)
  on line 1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1824-1824)
  on line 1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1826-1826)
  on line 1828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1828-1828)
  on line 1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1838-1838)
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1840-1840)
  on line 1842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1842-1842)
  on line 1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1879-1879)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3536-3536)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 383
  dead: 1055 (521 in uncalled functions)
  total lines: 1438
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3071:15-3071:37)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3075:17-3075:24)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2849:11-2849:21)
[Warning][Deadcode][CWE-570] condition 'currentFloorID___0 > 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3082:17-3082:39)
[Warning][Deadcode][CWE-571] condition 'tmp___7' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1872:11-1872:18)
[Warning][Deadcode][CWE-571] condition 'p == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:730:7-730:13)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2671:9-2671:19)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2497:9-2497:19)
[Warning][Deadcode][CWE-570] condition 'expectedDirection == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3120:9-3120:31)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2876:13-2876:23)
[Warning][Deadcode][CWE-570] condition 'weight > maximumWeight' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1898:9-1898:31)
[Warning][Deadcode][CWE-571] condition 'ofHeading == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1638:7-1638:21)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2698:11-2698:21)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1666:7-1666:14)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2903:15-2903:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2904:17-2904:28)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1433:7-1433:15)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1679:7-1679:14)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2530:11-2530:21)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1692:7-1692:14)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2725:13-2725:23)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1705:7-1705:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:818:7-818:19)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1248:9-1248:28)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:412:7-412:10)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1254:9-1254:27)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1718:7-1718:14)
[Warning][Deadcode][CWE-571] condition 'floorButtons_0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1489:7-1489:21)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1255:11-1255:28)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2563:13-2563:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2377:9-2377:21)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1259:13-1259:20)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:432:7-432:18)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2752:15-2752:25)
[Warning][Deadcode][CWE-570] condition 'tmp___10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2976:7-2976:20)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2753:17-2753:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2381:11-2381:23)
[Warning][Deadcode][CWE-570] condition 'tmp___10' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1731:7-1731:15)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:846:7-846:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1270:11-1270:29)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1271:13-1271:31)
[Warning][Deadcode][CWE-571] condition 'floorButtons_0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1272:15-1272:29)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:849:9-849:21)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:852:11-852:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2389:15-2389:27)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:855:13-855:25)
[Warning][Deadcode][CWE-570] condition 'dir == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1079:7-1079:15)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:858:15-858:27)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1766:9-1766:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2408:7-2408:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2795:7-2795:17)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2411:9-2411:21)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2596:15-2596:25)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1780:9-1780:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2414:11-2414:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1528:9-1528:12)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:471:7-471:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2417:13-2417:25)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1534:9-1534:28)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1794:9-1794:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2420:15-2420:27)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2436:7-2436:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3038:9-3038:31)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1808:9-1808:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2439:9-2439:21)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2822:9-2822:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2442:11-2442:23)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1822:9-1822:18)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3049:11-3049:33)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2617:27-2617:38)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2445:13-2445:25)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:908:15-908:27)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1564:9-1564:12)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3053:13-3053:20)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2448:15-2448:27)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1836:9-1836:18)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3060:13-3060:35)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2464:7-2464:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:2644:7-2644:17)
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:3064:15-3064:22)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:510:7-510:18)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product24.cil.c:1586:7-1586:26)
[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
