./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_spec14_productSimulator.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_spec14_productSimulator.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_spec14_productSimulator.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_spec14_productSimulator.cil.c:914:3-933:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:961:3-980:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1202:3-1230:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1262:3-1305:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3101:5-3159:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3176:9-3234:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3348:3-3369:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3405:3-3430:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3490:5-3510:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1623:3-1623:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2452:5-2452:40)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2454:5-2454:40)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1562:3-1562:24)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:265:1-306:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:896:1-938:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:939:1-985:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1059:1-1110:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1122:1-1132:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1133:1-1143:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1144:1-1154:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1155:1-1165:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1236:1-1313:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1314:1-1325:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1326:1-1337:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1338:1-1348:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1349:1-1365:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1441:1-1463:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1464:1-1486:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1790:1-1798:1)
[Warning][Deadcode] Function 'printState__before__overloaded' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2881:1-3051:1)
[Warning][Deadcode] Function 'printState__role__overloaded' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3052:1-3073:1)
[Warning][Deadcode] Function 'printState' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3074:1-3090:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3091:1-3249:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3277:1-3322:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3323:1-3378:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3379:1-3438:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3441:1-3543:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3544:1-3589:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3590:1-3635:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3642-3642)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 1852..1853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1852-1853)
  on lines 1863..1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1863-1864)
  on lines 1867..1868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1867-1868)
  on lines 1874..1875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1874-1875)
  on lines 1878..1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1878-1879)
  on lines 1885..1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1885-1886)
  on lines 1900..1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1900-1901)
  on line 1916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1916-1916)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1753-1753)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1787-1787)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:375-375)
  on line 381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:381-381)
  on line 384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:384-384)
[Warning][Deadcode] Function 'enterElevator__before__weight' has dead code:
  on line 1531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1531-1531)
  on line 1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1534-1534)
  on line 1537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1537-1537)
  on line 1540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1540-1540)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1744-1744)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 191..192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:191-192)
  on lines 195..196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:195-196)
  on lines 199..200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:199-200)
  on lines 203..204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:203-204)
  on lines 210..211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:210-211)
  on line 218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:218-218)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 152..153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:152-153)
  on lines 156..157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:156-157)
  on lines 160..161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:160-161)
  on lines 164..165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:164-165)
  on lines 171..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:171-172)
  on line 179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:179-179)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on line 2592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2592-2592)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 113..114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:113-114)
  on lines 117..118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:117-118)
  on lines 121..122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:121-122)
  on lines 125..126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:125-126)
  on lines 132..133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:132-133)
  on line 140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:140-140)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 583..584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:583-584)
  on lines 586..587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:586-587)
  on lines 589..590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:589-590)
  on lines 592..593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:592-593)
  on lines 595..596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:595-596)
  on lines 598..599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:598-599)
  on line 611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:611-611)
  on line 614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:614-614)
  on line 617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:617-617)
  on line 620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:620-620)
  on line 623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:623-623)
  on lines 637..638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:637-638)
  on lines 640..641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:640-641)
  on lines 643..644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:643-644)
  on lines 646..647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:646-647)
  on lines 649..650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:649-650)
  on lines 652..653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:652-653)
  on lines 664..665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:664-665)
  on lines 667..668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:667-668)
  on lines 670..671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:670-671)
  on lines 673..674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:673-674)
  on lines 676..677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:676-677)
  on lines 679..680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:679-680)
  on lines 694..695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:694-695)
  on lines 697..698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:697-698)
  on lines 700..701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:700-701)
  on lines 703..704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:703-704)
  on lines 706..707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:706-707)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2405..2406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2405-2406)
  on lines 2409..2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2409-2410)
  on lines 2417..2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2417-2418)
  on line 2427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2427-2427)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 1520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1520-1520)
[Warning][Deadcode] Function 'isBlocked__before__overloaded' has dead code:
  on line 1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1493-1493)
[Warning][Deadcode] Function 'isBlocked__role__overloaded' has dead code:
  on line 1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1502-1502)
[Warning][Deadcode] Function 'isEmpty' has dead code:
  on lines 1808..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1808-1809)
  on lines 1812..1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1812-1813)
  on lines 1816..1817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1816-1817)
  on lines 1820..1821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1820-1821)
  on line 1836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1836-1836)
[Warning][Deadcode] Function 'isExecutiveFloor' has dead code:
  on line 3267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3267-3267)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 3258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:3258-3258)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on line 339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:339-339)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1929-1929)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on line 575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:575-575)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:886-886)
[Warning][Deadcode] Function 'leaveElevator__before__weight' has dead code:
  on line 1592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1592-1592)
  on line 1595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1595-1595)
  on line 1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1598-1598)
  on line 1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1601-1601)
[Warning][Deadcode] Function 'main' has dead code:
  on line 1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1404-1404)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1690-1690)
  on line 1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1693-1693)
  on lines 1698..1699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1698-1699)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2628..2631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2628-2631)
  on lines 2641..2644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2641-2644)
  on lines 2654..2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2654-2657)
  on lines 2667..2670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2667-2670)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 737..738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:737-738)
  on lines 740..741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:740-741)
  on lines 743..744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:743-744)
  on lines 746..747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:746-747)
  on lines 749..750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:749-750)
  on line 765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:765-765)
  on line 768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:768-768)
  on line 771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:771-771)
  on line 774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:774-774)
  on lines 791..792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:791-792)
  on lines 794..795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:794-795)
  on lines 797..798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:797-798)
  on lines 800..801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:800-801)
  on lines 803..804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:803-804)
  on lines 818..819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:818-819)
  on lines 821..822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:821-822)
  on lines 824..825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:824-825)
  on lines 827..828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:827-828)
  on lines 830..831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:830-831)
  on lines 845..846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:845-846)
  on lines 848..849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:848-849)
  on lines 851..852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:851-852)
  on lines 854..855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:854-855)
  on lines 857..858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:857-858)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:998-998)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 2574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2574-2574)
  on line 2576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2576-2576)
  on line 2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2578-2578)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__before__executivefloor' has dead code:
  on line 2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2529-2529)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__before__twothirdsfull' has dead code:
  on line 2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2483-2483)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__role__executivefloor' has dead code:
  on line 2560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2560-2560)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__role__twothirdsfull' has dead code:
  on line 2511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2511-2511)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 2388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2388-2388)
  on line 2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2391-2391)
  on line 2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2393-2393)
[Warning][Deadcode] Function 'stopRequestedInDirection__before__executivefloor' has dead code:
  on line 2343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2343-2343)
[Warning][Deadcode] Function 'stopRequestedInDirection__before__twothirdsfull' has dead code:
  on lines 1964..1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1964-1965)
  on lines 2006..2007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2006-2007)
  on lines 2022..2023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2022-2023)
  on lines 2035..2036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2035-2036)
  on lines 2051..2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2051-2052)
  on lines 2093..2094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2093-2094)
  on lines 2100..2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2100-2101)
  on lines 2129..2130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2129-2130)
  on lines 2158..2159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2158-2159)
  on lines 2171..2172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2171-2172)
  on lines 2187..2188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2187-2188)
  on lines 2200..2201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2200-2201)
  on lines 2216..2217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2216-2217)
  on lines 2258..2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2258-2259)
  on lines 2265..2266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2265-2266)
  on line 2282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2282-2282)
[Warning][Deadcode] Function 'stopRequestedInDirection__role__executivefloor' has dead code:
  on line 2373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2373-2373)
[Warning][Deadcode] Function 'stopRequestedInDirection__role__twothirdsfull' has dead code:
  on line 2322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2322-2322)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 2877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2877-2877)
[Warning][Deadcode] Function 'timeShift__before__overloaded' has dead code:
  on line 2729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2729-2729)
  on line 2731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2731-2731)
  on line 2733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2733-2733)
  on line 2743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2743-2743)
  on line 2745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2745-2745)
  on line 2747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2747-2747)
  on line 2757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2757-2757)
  on line 2759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2759-2759)
  on line 2761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2761-2761)
  on line 2771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2771-2771)
  on line 2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2773-2773)
  on line 2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2775-2775)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1054-1054)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 741
  dead: 751 (487 in uncalled functions)
  total lines: 1492
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:788:13-788:24)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2727:9-2727:18)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2227:25-2227:43)
[Warning][Deadcode][CWE-570] condition 'persons_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1807:9-1807:23)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2741:9-2741:18)
[Warning][Deadcode][CWE-570] condition 'persons_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1811:11-1811:25)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:423:19-423:30)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2755:9-2755:18)
[Warning][Deadcode][CWE-570] condition 'persons_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1815:13-1815:27)
[Warning][Deadcode][CWE-570] condition 'persons_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1819:15-1819:29)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2769:9-2769:18)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:815:15-815:26)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2256:29-2256:47)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2257:31-2257:45)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1851:7-1851:14)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:456:21-456:32)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:842:17-842:28)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1862:11-1862:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1866:13-1866:27)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1873:15-1873:22)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1877:17-1877:31)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1884:19-1884:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:489:23-489:34)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:112:9-112:20)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1899:25-1899:39)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_executivefloor' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2380:7-2380:40)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:116:11-116:22)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:120:13-120:24)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:124:15-124:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:522:25-522:36)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2404:9-2404:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:128:17-128:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2408:11-2408:25)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1963:13-1963:20)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2416:15-2416:29)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:155:11-155:22)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1975:13-1975:31)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:159:13-159:24)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:555:27-555:38)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1530:9-1530:15)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:163:15-163:26)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1533:11-1533:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1202:10-1202:11)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:167:17-167:28)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1536:13-1536:19)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:582:7-582:17)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1539:15-1539:21)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1206:9-1206:23)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2004:17-2004:35)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1542:17-1542:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2005:19-2005:33)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1222:9-1222:12)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:190:9-190:20)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:194:11-194:22)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2021:21-2021:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1202:10-1202:11)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:198:13-198:24)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:610:11-610:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1206:9-1206:23)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:202:15-202:26)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2033:21-2033:39)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:613:13-613:24)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2034:23-2034:37)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1591:9-1591:15)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:616:15-616:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:206:17-206:28)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1594:11-1594:17)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1222:9-1222:12)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:619:17-619:28)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1597:13-1597:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:622:19-622:30)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1600:15-1600:21)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2050:25-2050:32)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:625:21-625:32)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1603:17-1603:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1202:10-1202:11)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:636:11-636:21)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1206:9-1206:23)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2062:25-2062:43)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:663:13-663:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1202:10-1202:11)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2091:29-2091:47)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_executivefloor' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2567:7-2567:40)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2092:31-2092:45)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1689:9-1689:21)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1692:11-1692:23)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:690:15-690:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:691:17-691:28)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:1695:13-1695:25)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2128:13-2128:20)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2626:7-2626:14)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2140:13-2140:31)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2639:7-2639:14)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2157:17-2157:24)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:734:9-734:20)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2652:7-2652:14)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2169:17-2169:35)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2170:19-2170:33)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2665:7-2665:14)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:374:7-374:19)
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2186:21-2186:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:380:11-380:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:383:13-383:25)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:764:13-764:24)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:386:15-386:27)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2198:21-2198:39)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:767:15-767:26)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2199:23-2199:37)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:770:17-770:28)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:773:19-773:30)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:776:21-776:32)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_productSimulator.cil.c:2215:25-2215:32)
[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)
