./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_spec2_product26.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_spec2_product26.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:198:3-226:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:260:3-303:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1791:5-1849:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1866:9-1924:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2148:3-2169:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2205:3-2230:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2290:5-2310:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3342:3-3361:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3389:3-3408:3 with factor 5
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:51:1-102:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:105:1-115:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:116:1-126:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:127:1-137:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:138:1-148:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:149:1-159:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:172:1-183:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:234:1-311:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:312:1-323:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:324:1-335:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:336:1-346:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:347:1-363:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:446:1-468:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:469:1-491:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:545:1-576:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:577:1-588:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:589:1-608:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:722:1-730:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:731:1-770:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1216:1-1249:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1306:1-1319:1)
[Warning][Deadcode] Function 'printState__wrappee__empty' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1588:1-1758:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1759:1-1780:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1781:1-1939:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2077:1-2122:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2123:1-2178:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2179:1-2238:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2241:1-2343:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2344:1-2389:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2390:1-2435:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2438:1-2447:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2508:1-2549:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3324:1-3366:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3367:1-3413:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3320-3320)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__2' has dead code:
  on line 3156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3156-3156)
  on line 3159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3159-3159)
  on line 3162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3162-3162)
  on lines 3167..3168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3167-3168)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__3' has dead code:
  on line 3194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3194-3194)
  on line 3196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3196-3196)
  on lines 3198..3199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3198-3199)
  on line 3211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3211-3211)
  on lines 3213..3214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3213-3214)
  on line 3224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3224-3224)
  on line 3226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3226-3226)
  on lines 3228..3229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3228-3229)
  on line 3239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3239-3239)
  on line 3241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3241-3241)
  on lines 3243..3244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3243-3244)
  on line 3254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3254-3254)
  on line 3256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3256-3256)
  on lines 3258..3259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3258-3259)
[Warning][Deadcode] Function '__utac_acc__Specification2_spec__4' has dead code:
  on line 3282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3282-3282)
  on line 3287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3287-3287)
  on line 3292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3292-3292)
  on line 3300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3300-3300)
  on line 3302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3302-3302)
  on line 3311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3311-3311)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 784..785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:784-785)
  on lines 788..789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:788-789)
  on lines 799..800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:799-800)
  on lines 806..807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:806-807)
  on lines 810..811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:810-811)
  on lines 817..818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:817-818)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:825-825)
  on lines 827..829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:827-829)
  on lines 831..833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:831-833)
  on lines 846..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:846-848)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:685-685)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 696..698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:696-698)
  on lines 700..702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:700-702)
  on lines 704..706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:704-706)
  on lines 708..710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:708-710)
  on lines 712..713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:712-713)
  on line 719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:719-719)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 2618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2618-2618)
  on lines 2623..2624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2623-2624)
  on lines 2626..2627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2626-2627)
  on lines 2629..2630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2629-2630)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:219-219)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1260-1260)
  on lines 1265..1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1265-1266)
  on line 1274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1274-1274)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:506-506)
  on line 509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:509-509)
  on line 512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:512-512)
  on line 515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:515-515)
  on line 518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:518-518)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:676-676)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 2024..2025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2024-2025)
  on lines 2028..2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2028-2029)
  on lines 2032..2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2032-2033)
  on lines 2036..2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2036-2037)
  on lines 2040..2041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2040-2041)
  on lines 2047..2048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2047-2048)
  on line 2055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2055-2055)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 1985..1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1985-1986)
  on lines 1989..1990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1989-1990)
  on lines 1993..1994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1993-1994)
  on lines 1997..1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1997-1998)
  on lines 2001..2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2001-2002)
  on lines 2008..2009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2008-2009)
  on line 2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2016-2016)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 1946..1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1946-1947)
  on lines 1950..1951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1950-1951)
  on lines 1954..1955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1954-1955)
  on lines 1958..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1958-1959)
  on lines 1962..1963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1962-1963)
  on lines 1969..1970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1969-1970)
  on line 1977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1977-1977)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 2826..2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2826-2827)
  on lines 2829..2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2829-2830)
  on lines 2832..2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2832-2833)
  on lines 2835..2836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2835-2836)
  on lines 2838..2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2838-2839)
  on lines 2841..2842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2841-2842)
  on line 2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2854-2854)
  on line 2857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2857-2857)
  on line 2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2860-2860)
  on line 2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2863-2863)
  on line 2866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2866-2866)
  on lines 2879..2881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2879-2881)
  on lines 2883..2884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2883-2884)
  on lines 2886..2887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2886-2887)
  on lines 2889..2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2889-2890)
  on lines 2892..2893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2892-2893)
  on lines 2895..2896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2895-2896)
  on lines 2906..2908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2906-2908)
  on lines 2910..2911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2910-2911)
  on lines 2913..2914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2913-2914)
  on lines 2916..2917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2916-2917)
  on lines 2919..2920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2919-2920)
  on lines 2922..2923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2922-2923)
  on lines 2933..2935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2933-2935)
  on lines 2937..2938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2937-2938)
  on lines 2940..2941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2940-2941)
  on lines 2943..2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2943-2944)
  on lines 2946..2947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2946-2947)
  on lines 2949..2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2949-2950)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:498-498)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 2570..2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2570-2572)
  on lines 2580..2582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2580-2582)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:861-861)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 2646..2648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2646-2648)
  on lines 2650..2652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2650-2652)
  on lines 2654..2656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2654-2656)
  on lines 2658..2660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2658-2660)
  on lines 2662..2664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2662-2664)
  on lines 2666..2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2666-2668)
  on lines 2711..2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2711-2714)
  on lines 2716..2718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2716-2718)
  on lines 2720..2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2720-2722)
  on lines 2724..2726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2724-2726)
  on lines 2728..2730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2728-2730)
  on lines 2732..2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2732-2734)
  on lines 2744..2747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2744-2747)
  on lines 2749..2751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2749-2751)
  on lines 2753..2755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2753-2755)
  on lines 2757..2759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2757-2759)
  on lines 2761..2763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2761-2763)
  on lines 2765..2767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2765-2767)
  on lines 2777..2780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2777-2780)
  on lines 2782..2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2782-2784)
  on lines 2786..2788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2786-2788)
  on lines 2790..2792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2790-2792)
  on lines 2794..2796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2794-2796)
  on lines 2798..2800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2798-2800)
  on lines 2816..2818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2816-2818)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 3129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3129-3129)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 407..409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:407-409)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:619-619)
  on line 622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:622-622)
  on line 625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:625-625)
  on lines 630..631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:630-631)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 1340..1343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1340-1343)
  on lines 1353..1356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1353-1356)
  on lines 1366..1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1366-1369)
  on lines 1379..1382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1379-1382)
  on lines 1392..1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1392-1395)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 2977..2978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2977-2978)
  on lines 2980..2981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2980-2981)
  on lines 2983..2984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2983-2984)
  on lines 2986..2987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2986-2987)
  on lines 2989..2990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2989-2990)
  on lines 2992..2993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2992-2993)
  on line 3005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3005-3005)
  on line 3008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3008-3008)
  on line 3011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3011-3011)
  on line 3014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3014-3014)
  on line 3017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3017-3017)
  on lines 3030..3032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3030-3032)
  on lines 3034..3035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3034-3035)
  on lines 3037..3038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3037-3038)
  on lines 3040..3041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3040-3041)
  on lines 3043..3044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3043-3044)
  on lines 3046..3047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3046-3047)
  on lines 3057..3059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3057-3059)
  on lines 3061..3062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3061-3062)
  on lines 3064..3065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3064-3065)
  on lines 3067..3068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3067-3068)
  on lines 3070..3071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3070-3071)
  on lines 3073..3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3073-3074)
  on lines 3084..3086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3084-3086)
  on lines 3088..3089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3088-3089)
  on lines 3091..3092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3091-3092)
  on lines 3094..3095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3094-3095)
  on lines 3097..3098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3097-3098)
  on lines 3100..3101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3100-3101)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 2590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2590-2590)
  on lines 2595..2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2595-2596)
  on lines 2598..2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2598-2599)
  on lines 2601..2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2601-2602)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:647-647)
  on lines 652..653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:652-653)
  on lines 655..656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:655-656)
  on lines 658..659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:658-659)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:383-383)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on lines 1296..1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1296-1297)
  on line 1303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1303-1303)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 884..885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:884-885)
  on line 890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:890-890)
  on line 892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:892-892)
  on lines 894..896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:894-896)
  on lines 906..909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:906-909)
  on lines 934..938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:934-938)
  on lines 947..948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:947-948)
  on line 950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:950-950)
  on lines 952..954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:952-954)
  on lines 963..967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:963-967)
  on lines 976..977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:976-977)
  on line 979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:979-979)
  on lines 981..983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:981-983)
  on lines 992..996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:992-996)
  on lines 1005..1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1005-1006)
  on line 1008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1008-1008)
  on lines 1010..1012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1010-1012)
  on lines 1021..1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1021-1025)
  on lines 1027..1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1027-1028)
  on lines 1031..1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1031-1032)
  on lines 1035..1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1035-1036)
  on lines 1048..1050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1048-1050)
  on lines 1054..1055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1054-1055)
  on line 1057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1057-1057)
  on lines 1059..1061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1059-1061)
  on lines 1070..1074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1070-1074)
  on lines 1083..1084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1083-1084)
  on line 1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1086-1086)
  on lines 1088..1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1088-1090)
  on lines 1099..1103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1099-1103)
  on lines 1112..1113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1112-1113)
  on line 1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1115-1115)
  on lines 1117..1119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1117-1119)
  on lines 1128..1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1128-1132)
  on lines 1141..1142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1141-1142)
  on line 1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1144-1144)
  on lines 1146..1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1146-1148)
  on lines 1157..1161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1157-1161)
  on lines 1170..1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1170-1171)
  on line 1173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1173-1173)
  on lines 1175..1177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1175-1177)
  on lines 1186..1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1186-1190)
  on lines 1192..1193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1192-1193)
  on lines 1196..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1196-1197)
  on lines 1200..1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1200-1201)
  on line 1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1213-1213)
[Warning][Deadcode] Function 'timeShift__wrappee__empty' has dead code:
  on line 1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1440-1440)
  on line 1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1442-1442)
  on line 1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1444-1444)
  on line 1454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1454-1454)
  on line 1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1456-1456)
  on line 1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1458-1458)
  on line 1468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1468-1468)
  on line 1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1470-1470)
  on line 1472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1472-1472)
  on line 1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1482-1482)
  on line 1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1484-1484)
  on line 1486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1486-1486)
  on line 1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1496-1496)
  on line 1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1498-1498)
  on line 1500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1500-1500)
  on line 1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1510-1510)
  on line 1512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1512-1512)
  on line 1514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1514-1514)
  on lines 1541..1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1541-1542)
  on line 1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1544-1544)
  on lines 1546..1547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1546-1547)
  on line 1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1551-1551)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2468-2468)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 311
  dead: 1080 (564 in uncalled functions)
  total lines: 1391
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2031:11-2031:22)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2589:7-2589:19)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:202:9-202:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3193:7-3193:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2976:7-2976:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2592:9-2592:21)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2035:13-2035:24)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:206:11-206:23)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:783:7-783:14)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1438:9-1438:18)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2039:15-2039:26)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:787:9-787:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:218:9-218:12)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1452:9-1452:18)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2043:17-2043:28)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3208:9-3208:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3209:11-3209:30)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:198:10-198:11)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2617:7-2617:19)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1466:9-1466:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:798:13-798:27)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2620:9-2620:21)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:202:9-202:23)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3223:11-3223:21)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3003:9-3003:19)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3004:11-3004:22)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:206:11-206:23)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1480:9-1480:18)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:805:15-805:22)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3007:13-3007:24)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:218:9-218:12)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:809:17-809:31)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3010:15-3010:26)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1494:9-1494:18)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3238:13-3238:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3013:17-3013:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2645:7-2645:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2825:7-2825:17)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:816:19-816:26)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:618:7-618:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3016:19-3016:30)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:198:10-198:11)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1508:9-1508:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:621:9-621:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3019:21-3019:32)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1255:7-1255:26)
[Warning][Deadcode][CWE-571] condition 'floorButtons_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:820:21-820:35)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3253:15-3253:25)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:202:9-202:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:624:11-624:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1259:9-1259:12)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:206:11-206:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:627:13-627:25)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1527:9-1527:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3280:7-3280:26)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1271:7-1271:26)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1535:9-1535:16)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3285:9-3285:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:646:7-646:19)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2852:9-2852:19)
[Warning][Deadcode][CWE-570] condition 'floorButtons_spc2_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3290:11-3290:30)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2853:11-2853:22)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:649:9-649:21)
[Warning][Deadcode][CWE-571] condition 'floorButtons_spc2_3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3295:13-3295:32)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2856:13-2856:24)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:399:7-399:10)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2678:9-2678:19)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2859:15-2859:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1295:9-1295:12)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:879:7-879:15)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2862:17-2862:28)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1945:7-1945:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:883:9-883:12)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2865:19-2865:30)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1949:9-1949:20)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2868:21-2868:32)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:889:9-889:27)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1953:11-1953:22)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:692:7-692:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1957:13-1957:24)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2699:21-2699:32)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:905:11-905:29)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1338:7-1338:14)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1961:15-1961:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1965:17-1965:28)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:918:13-918:31)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1351:7-1351:14)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:919:15-919:32)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:923:17-923:24)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1984:7-1984:18)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1364:7-1364:14)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1988:9-1988:20)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1992:11-1992:22)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:505:7-505:13)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1377:7-1377:14)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1996:13-1996:24)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:508:9-508:15)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:511:11-511:17)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2000:15-2000:26)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:514:13-514:19)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1390:7-1390:14)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2004:17-2004:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3155:7-3155:17)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:517:15-517:21)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3158:9-3158:19)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:520:17-520:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2566:13-2566:25)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3161:11-3161:21)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:1403:7-1403:15)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2023:7-2023:18)
[Warning][Deadcode][CWE-571] condition 'floor == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:3164:13-3164:23)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:2027:9-2027:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec2_product26.cil.c:198:10-198:11)
[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)
