./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_product11.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_product11.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_product11.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_product11.cil.c:135:3-156:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:192:3-217:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:277:5-297:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:451:3-470:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:498:3-517:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:977:3-1005:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1037:3-1080:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2557:5-2615:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2632:9-2690:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:64:1-109:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:110:1-165:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:166:1-225:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:228:1-330:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:331:1-376:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:377:1-422:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:433:1-475:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:476:1-522:1)
[Warning][Deadcode] Function 'getWeight' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:526:1-564:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:834:1-885:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:897:1-907:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:908:1-918:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:919:1-929:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:930:1-940:1)
[Warning][Deadcode] Function 'bigMacCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:941:1-951:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1011:1-1088:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1089:1-1100:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1101:1-1112:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1113:1-1123:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1124:1-1140:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1251:1-1273:1)
[Warning][Deadcode] Function 'isBlocked' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1274:1-1282:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1315:1-1346:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1347:1-1366:1)
[Warning][Deadcode] Function 'areDoorsOpen' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1432:1-1440:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1484:1-1523:1)
[Warning][Deadcode] Function 'anyStopRequested' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1524:1-1603:1)
[Warning][Deadcode] Function 'isIdle' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1604:1-1616:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1998:1-2031:1)
[Warning][Deadcode] Function 'printState' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2376:1-2546:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2547:1-2705:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2717:1-2725:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3389:1-3398:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:54-54)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__1' has dead code:
  on line 671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:671-671)
  on line 673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:673-673)
  on lines 675..676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:675-676)
  on line 682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:682-682)
  on line 684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:684-684)
  on lines 686..687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:686-687)
  on line 693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:693-693)
  on line 695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:695-695)
  on lines 697..698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:697-698)
  on line 704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:704-704)
  on line 706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:706-706)
  on lines 708..709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:708-709)
  on line 715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:715-715)
  on line 717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:717-717)
  on lines 719..720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:719-720)
  on line 748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:748-748)
  on line 759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:759-759)
  on line 770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:770-770)
  on line 778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:778-778)
  on lines 780..781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:780-781)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__2' has dead code:
  on line 816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:816-816)
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:818-818)
  on line 820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:820-820)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1465..1466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1465-1466)
  on line 1472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1472-1472)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2873-2873)
  on line 2876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2876-2876)
  on line 2879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2879-2879)
  on line 2882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2882-2882)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:974-974)
  on line 977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:977-977)
  on lines 980..981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:980-981)
  on line 983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:983-983)
  on line 985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:985-985)
  on line 995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:995-995)
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:997-998)
  on line 1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1001-1001)
  on line 1004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1004-1004)
  on line 1008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1008-1008)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2042-2042)
  on line 2048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2048-2048)
[Warning][Deadcode] Function 'enterElevator' has dead code:
  on lines 1290..1291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1290-1291)
  on lines 1293..1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1293-1294)
  on lines 1296..1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1296-1297)
  on lines 1299..1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1299-1300)
  on lines 1302..1303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1302-1303)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1429-1429)
[Warning][Deadcode] Function 'getCurrentHeading' has dead code:
  on line 1481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1481-1481)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 612..614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:612-614)
  on lines 616..618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:616-618)
  on lines 620..622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:620-622)
  on lines 624..626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:624-626)
  on lines 628..630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:628-630)
  on lines 632..633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:632-633)
  on line 640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:640-640)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 573..575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:573-575)
  on lines 577..579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:577-579)
  on lines 581..583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:581-583)
  on lines 585..587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:585-587)
  on lines 589..591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:589-591)
  on lines 593..594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:593-594)
  on line 601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:601-601)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on lines 2127..2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2127-2128)
  on line 2130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2130-2130)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 3081..3082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3081-3082)
  on lines 3084..3085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3084-3085)
  on lines 3087..3088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3087-3088)
  on lines 3090..3091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3090-3091)
  on lines 3093..3094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3093-3094)
  on lines 3096..3097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3096-3097)
  on lines 3108..3109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3108-3109)
  on lines 3111..3112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3111-3112)
  on lines 3114..3115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3114-3115)
  on lines 3117..3118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3117-3118)
  on lines 3120..3121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3120-3121)
  on lines 3123..3124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3123-3124)
  on lines 3135..3136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3135-3136)
  on lines 3138..3139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3138-3139)
  on lines 3141..3142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3141-3142)
  on lines 3144..3145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3144-3145)
  on lines 3147..3148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3147-3148)
  on lines 3150..3151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3150-3151)
  on lines 3162..3163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3162-3163)
  on lines 3165..3166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3165-3166)
  on lines 3168..3169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3168-3169)
  on lines 3171..3172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3171-3172)
  on lines 3174..3175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3174-3175)
  on lines 3177..3178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3177-3178)
  on lines 3192..3193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3192-3193)
  on lines 3195..3196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3195-3196)
  on lines 3198..3199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3198-3199)
  on lines 3201..3202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3201-3202)
  on lines 3204..3205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3204-3205)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2714-2714)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2814..2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2814-2815)
  on lines 2818..2819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2818-2819)
  on lines 2835..2837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2835-2837)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2901..2903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2901-2903)
  on lines 2905..2907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2905-2907)
  on lines 2909..2911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2909-2911)
  on lines 2913..2915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2913-2915)
  on lines 2917..2919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2917-2919)
  on lines 2921..2923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2921-2923)
  on lines 2934..2936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2934-2936)
  on lines 2938..2940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2938-2940)
  on lines 2942..2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2942-2944)
  on lines 2946..2948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2946-2948)
  on lines 2950..2952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2950-2952)
  on lines 2954..2956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2954-2956)
  on lines 2967..2969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2967-2969)
  on lines 2971..2973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2971-2973)
  on lines 2975..2977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2975-2977)
  on lines 2979..2981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2979-2981)
  on lines 2983..2985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2983-2985)
  on lines 2987..2989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2987-2989)
  on lines 3000..3002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3000-3002)
  on lines 3004..3006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3004-3006)
  on lines 3008..3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3008-3010)
  on lines 3012..3014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3012-3014)
  on lines 3016..3018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3016-3018)
  on lines 3020..3022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3020-3022)
  on lines 3071..3073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3071-3073)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 3384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3384-3384)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 1180..1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1180-1182)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on lines 1374..1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1374-1375)
  on lines 1377..1378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1377-1378)
  on lines 1380..1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1380-1381)
  on lines 1383..1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1383-1384)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2166..2169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2166-2169)
  on lines 2179..2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2179-2182)
  on lines 2192..2195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2192-2195)
  on lines 2205..2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2205-2208)
  on lines 2218..2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2218-2221)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 3232..3233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3232-3233)
  on lines 3235..3236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3235-3236)
  on lines 3238..3239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3238-3239)
  on lines 3241..3242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3241-3242)
  on lines 3244..3245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3244-3245)
  on lines 3247..3248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3247-3248)
  on lines 3259..3260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3259-3260)
  on lines 3262..3263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3262-3263)
  on lines 3265..3266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3265-3266)
  on lines 3268..3269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3268-3269)
  on lines 3271..3272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3271-3272)
  on lines 3274..3275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3274-3275)
  on lines 3286..3287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3286-3287)
  on lines 3289..3290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3289-3290)
  on lines 3292..3293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3292-3293)
  on lines 3295..3296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3295-3296)
  on lines 3298..3299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3298-3299)
  on lines 3301..3302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3301-3302)
  on lines 3313..3314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3313-3314)
  on lines 3316..3317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3316-3317)
  on lines 3319..3320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3319-3320)
  on lines 3322..3323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3322-3323)
  on lines 3325..3326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3325-3326)
  on lines 3328..3329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3328-3329)
  on lines 3343..3344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3343-3344)
  on lines 3346..3347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3346-3347)
  on lines 3349..3350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3349-3350)
  on lines 3352..3353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3352-3353)
  on lines 3355..3356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3355-3356)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2845-2845)
  on line 2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2848-2848)
  on line 2851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2851-2851)
  on line 2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2854-2854)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1400-1400)
  on line 1403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1403-1403)
  on line 1406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1406-1406)
  on line 1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1409-1409)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 1156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1156-1156)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 2116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2116-2116)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 2078..2079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2078-2079)
  on line 2085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2085-2085)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 1995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1995-1995)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on line 1634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1634-1634)
  on lines 1636..1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1636-1638)
  on lines 1642..1643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1642-1643)
  on line 1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1645-1645)
  on lines 1647..1649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1647-1649)
  on lines 1658..1662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1658-1662)
  on lines 1671..1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1671-1672)
  on line 1674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1674-1674)
  on lines 1676..1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1676-1678)
  on lines 1687..1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1687-1691)
  on lines 1700..1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1700-1701)
  on line 1703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1703-1703)
  on lines 1705..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1705-1707)
  on lines 1716..1720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1716-1720)
  on lines 1729..1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1729-1730)
  on line 1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1732-1732)
  on lines 1734..1736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1734-1736)
  on lines 1745..1749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1745-1749)
  on lines 1758..1759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1758-1759)
  on line 1761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1761-1761)
  on lines 1763..1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1763-1765)
  on lines 1774..1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1774-1778)
  on lines 1780..1781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1780-1781)
  on lines 1784..1785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1784-1785)
  on lines 1788..1789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1788-1789)
  on lines 1802..1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1802-1803)
  on lines 1813..1814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1813-1814)
  on lines 1836..1837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1836-1837)
  on line 1839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1839-1839)
  on lines 1841..1843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1841-1843)
  on lines 1852..1856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1852-1856)
  on lines 1865..1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1865-1866)
  on line 1868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1868-1868)
  on lines 1870..1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1870-1872)
  on lines 1881..1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1881-1885)
  on lines 1894..1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1894-1895)
  on line 1897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1897-1897)
  on lines 1899..1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1899-1901)
  on lines 1910..1914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1910-1914)
  on lines 1923..1924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1923-1924)
  on line 1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1926-1926)
  on lines 1928..1930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1928-1930)
  on lines 1939..1943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1939-1943)
  on lines 1945..1946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1945-1946)
  on lines 1949..1950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1949-1950)
  on lines 1953..1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1953-1954)
  on line 1966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1966-1966)
[Warning][Deadcode] Function 'test' has dead code:
  on line 1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1197-1197)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2254-2254)
  on line 2256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2256-2256)
  on line 2258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2258-2258)
  on line 2268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2268-2268)
  on line 2270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2270-2270)
  on line 2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2272-2272)
  on line 2282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2282-2282)
  on line 2284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2284-2284)
  on line 2286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2286-2286)
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2296-2296)
  on line 2298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2298-2298)
  on line 2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2300-2300)
  on line 2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2310-2310)
  on line 2312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2312-2312)
  on line 2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2314-2314)
  on line 2324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2324-2324)
  on line 2326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2326-2326)
  on line 2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2328-2328)
  on line 2365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2365-2365)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3419-3419)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 343
  dead: 1050 (562 in uncalled functions)
  total lines: 1393
[Warning][Deadcode][CWE-570] condition 'tmp___10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:670:7-670:20)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2151:7-2151:14)
[Warning][Deadcode][CWE-571] condition 'p == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1287:7-1287:13)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2164:7-2164:14)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2999:13-2999:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2813:9-2813:21)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3188:15-3188:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3189:17-3189:28)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2177:7-2177:14)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2817:11-2817:23)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2190:7-2190:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2825:15-2825:27)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2203:7-2203:14)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2844:7-2844:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:732:9-732:31)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3231:7-3231:17)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2847:9-2847:21)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3032:15-3032:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2850:11-2850:23)
[Warning][Deadcode][CWE-570] condition 'tmp___10' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2216:7-2216:15)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:743:11-743:33)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2853:13-2853:25)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:747:13-747:20)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2856:15-2856:27)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:754:13-754:35)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2872:7-2872:19)
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:758:15-758:22)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2875:9-2875:21)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3258:9-3258:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2878:11-2878:23)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2252:9-2252:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1371:7-1371:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID___0 > 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:765:15-765:37)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3053:27-3053:38)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2881:13-2881:25)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1801:9-1801:28)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:769:17-769:24)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2884:15-2884:27)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2266:9-2266:18)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1807:9-1807:27)
[Warning][Deadcode][CWE-570] condition 'currentFloorID___0 > 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:776:17-776:39)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1808:11-1808:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2900:7-2900:17)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:569:7-569:18)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3080:7-3080:17)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1812:13-1812:20)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2280:9-2280:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1399:7-1399:19)
[Warning][Deadcode][CWE-571] condition 'currentFloorID > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1823:11-1823:29)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2294:9-2294:18)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1824:13-1824:31)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3285:11-3285:21)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2041:9-2041:12)
[Warning][Deadcode][CWE-571] condition 'floorButtons_0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1825:15-1825:29)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1402:9-1402:21)
[Warning][Deadcode][CWE-570] condition 'expectedDirection == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:814:9-814:31)
[Warning][Deadcode][CWE-570] condition 'currentFloorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2047:9-2047:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1405:11-1405:23)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2308:9-2308:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1408:13-1408:25)
[Warning][Deadcode][CWE-570] condition 'dir == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1632:7-1632:15)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1411:15-1411:27)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1172:7-1172:10)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3107:9-3107:19)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2322:9-2322:18)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2933:9-2933:19)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3312:13-3312:23)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:608:7-608:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2077:9-2077:12)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3134:11-3134:21)
[Warning][Deadcode][CWE-571] condition 'tmp___7' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2358:11-2358:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:1461:15-1461:27)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3339:15-3339:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3340:17-3340:28)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2966:11-2966:21)
[Warning][Deadcode][CWE-571] condition 'ofHeading == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:2123:7-2123:21)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_product11.cil.c:3161:13-3161:23)
[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)
