./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/elevator_spec3_productSimulator.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/elevator_spec3_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_spec3_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_spec3_productSimulator.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:268:5-288:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1119:3-1138:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1166:3-1185:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2892:5-2950:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2967:9-3025:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3394:3-3422:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3454:3-3497:3 with factor 1
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1409:3-1409:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2238:5-2238:40)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2240:5-2240:40)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1348:3-1348:24)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1101:1-1143:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1144:1-1190:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1250:1-1272:1)
[Warning][Deadcode] Function 'printState__before__overloaded' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2672:1-2842:1)
[Warning][Deadcode] Function 'printState__role__overloaded' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2843:1-2864:1)
[Warning][Deadcode] Function 'printState' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2865:1-2881:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2882:1-3040:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3052:1-3060:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3252:1-3303:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3315:1-3325:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3326:1-3336:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3337:1-3347:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3348:1-3358:1)
[Warning][Deadcode] Function 'bigMacCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3359:1-3369:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3428:1-3505:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3506:1-3517:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3518:1-3529:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3530:1-3540:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3541:1-3557:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1197-1197)
[Warning][Deadcode] Function '__utac_acc__Specification3_spec__1' has dead code:
  on line 3655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3655-3655)
  on line 3666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3666-3666)
  on line 3677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3677-3677)
  on line 3688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3688-3688)
  on line 3716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3716-3716)
  on line 3727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3727-3727)
  on line 3738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3738-3738)
  on line 3749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3749-3749)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 1638..1639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1638-1639)
  on lines 1649..1650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1649-1650)
  on lines 1653..1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1653-1654)
  on lines 1660..1661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1660-1661)
  on lines 1664..1665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1664-1665)
  on lines 1671..1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1671-1672)
  on lines 1675..1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1675-1676)
  on lines 1686..1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1686-1687)
  on line 1702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1702-1702)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1539-1539)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on line 1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1573-1573)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:575-575)
  on line 578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:578-578)
  on line 581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:581-581)
  on line 584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:584-584)
[Warning][Deadcode] Function 'enterElevator__before__weight' has dead code:
  on lines 1316..1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1316-1317)
  on lines 1319..1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1319-1320)
  on lines 1322..1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1322-1323)
  on lines 1325..1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1325-1326)
  on lines 1328..1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1328-1329)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1530-1530)
[Warning][Deadcode] Function 'getCurrentHeading' has dead code:
  on line 1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1582-1582)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 3219..3221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3219-3221)
  on lines 3223..3225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3223-3225)
  on lines 3227..3229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3227-3229)
  on lines 3231..3233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3231-3233)
  on lines 3235..3237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3235-3237)
  on lines 3239..3240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3239-3240)
  on line 3247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3247-3247)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 3180..3182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3180-3182)
  on lines 3184..3186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3184-3186)
  on lines 3188..3190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3188-3190)
  on lines 3192..3194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3192-3194)
  on lines 3196..3198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3196-3198)
  on lines 3200..3201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3200-3201)
  on line 3208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3208-3208)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on line 2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2378-2378)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 3141..3143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3141-3143)
  on lines 3145..3147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3145-3147)
  on lines 3149..3151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3149-3151)
  on lines 3153..3155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3153-3155)
  on lines 3157..3159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3157-3159)
  on lines 3161..3162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3161-3162)
  on line 3169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3169-3169)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 783..784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:783-784)
  on lines 786..787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:786-787)
  on lines 789..790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:789-790)
  on lines 792..793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:792-793)
  on lines 795..796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:795-796)
  on lines 798..799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:798-799)
  on lines 810..811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:810-811)
  on lines 813..814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:813-814)
  on lines 816..817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:816-817)
  on lines 819..820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:819-820)
  on lines 822..823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:822-823)
  on lines 825..826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:825-826)
  on lines 837..838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:837-838)
  on lines 840..841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:840-841)
  on lines 843..844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:843-844)
  on lines 846..847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:846-847)
  on lines 849..850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:849-850)
  on lines 852..853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:852-853)
  on lines 864..865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:864-865)
  on lines 867..868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:867-868)
  on lines 870..871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:870-871)
  on lines 873..874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:873-874)
  on lines 876..877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:876-877)
  on lines 879..880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:879-880)
  on lines 894..895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:894-895)
  on lines 897..898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:897-898)
  on lines 900..901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:900-901)
  on lines 903..904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:903-904)
  on lines 906..907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:906-907)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2191..2192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2191-2192)
  on lines 2195..2196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2195-2196)
  on lines 2199..2200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2199-2200)
  on lines 2203..2204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2203-2204)
  on line 2213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2213-2213)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 1306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1306-1306)
[Warning][Deadcode] Function 'isBlocked__before__overloaded' has dead code:
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1279-1279)
[Warning][Deadcode] Function 'isBlocked__role__overloaded' has dead code:
  on line 1288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1288-1288)
[Warning][Deadcode] Function 'isEmpty' has dead code:
  on lines 1590..1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1590-1591)
  on lines 1594..1595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1594-1595)
  on lines 1598..1599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1598-1599)
  on lines 1602..1603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1602-1603)
  on lines 1606..1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1606-1607)
  on lines 1610..1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1610-1611)
  on line 1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1622-1622)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 3049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3049-3049)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on line 539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:539-539)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1715-1715)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on line 775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:775-775)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1086-1086)
[Warning][Deadcode] Function 'leaveElevator__before__weight' has dead code:
  on lines 1377..1378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1377-1378)
  on lines 1380..1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1380-1381)
  on lines 1383..1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1383-1384)
  on lines 1386..1387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1386-1387)
  on lines 1389..1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1389-1390)
[Warning][Deadcode] Function 'main' has dead code:
  on line 3596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3596-3596)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on lines 1475..1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1475-1476)
  on lines 1478..1479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1478-1479)
  on lines 1481..1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1481-1482)
  on lines 1484..1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1484-1485)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2414..2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2414-2417)
  on lines 2427..2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2427-2430)
  on lines 2440..2443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2440-2443)
  on lines 2453..2456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2453-2456)
  on lines 2466..2469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2466-2469)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 937..938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:937-938)
  on lines 940..941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:940-941)
  on lines 943..944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:943-944)
  on lines 946..947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:946-947)
  on lines 949..950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:949-950)
  on lines 964..965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:964-965)
  on lines 967..968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:967-968)
  on lines 970..971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:970-971)
  on lines 973..974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:973-974)
  on lines 976..977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:976-977)
  on lines 991..992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:991-992)
  on lines 994..995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:994-995)
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:997-998)
  on lines 1000..1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1000-1001)
  on lines 1003..1004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1003-1004)
  on lines 1018..1019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1018-1019)
  on lines 1021..1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1021-1022)
  on lines 1024..1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1024-1025)
  on lines 1027..1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1027-1028)
  on lines 1030..1031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1030-1031)
  on lines 1045..1046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1045-1046)
  on lines 1048..1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1048-1049)
  on lines 1051..1052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1051-1052)
  on lines 1054..1055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1054-1055)
  on lines 1057..1058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1057-1058)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 3073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3073-3073)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 2364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2364-2364)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__before__executivefloor' has dead code:
  on line 2315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2315-2315)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__before__twothirdsfull' has dead code:
  on line 2269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2269-2269)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__role__executivefloor' has dead code:
  on line 2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2346-2346)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__role__twothirdsfull' has dead code:
  on line 2297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2297-2297)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2179-2179)
[Warning][Deadcode] Function 'stopRequestedInDirection__before__executivefloor' has dead code:
  on line 2129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2129-2129)
[Warning][Deadcode] Function 'stopRequestedInDirection__before__twothirdsfull' has dead code:
  on lines 1750..1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1750-1751)
  on lines 1779..1780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1779-1780)
  on lines 1792..1793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1792-1793)
  on lines 1808..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1808-1809)
  on lines 1821..1822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1821-1822)
  on lines 1837..1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1837-1838)
  on lines 1850..1851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1850-1851)
  on lines 1879..1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1879-1880)
  on lines 1886..1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1886-1887)
  on lines 1915..1916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1915-1916)
  on lines 1944..1945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1944-1945)
  on lines 1957..1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1957-1958)
  on lines 1973..1974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1973-1974)
  on lines 1986..1987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1986-1987)
  on lines 2002..2003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2002-2003)
  on lines 2015..2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2015-2016)
  on lines 2044..2045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2044-2045)
  on lines 2051..2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2051-2052)
  on line 2068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2068-2068)
[Warning][Deadcode] Function 'stopRequestedInDirection__role__executivefloor' has dead code:
  on line 2159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2159-2159)
[Warning][Deadcode] Function 'stopRequestedInDirection__role__twothirdsfull' has dead code:
  on line 2108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2108-2108)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2668-2668)
[Warning][Deadcode] Function 'timeShift__before__overloaded' has dead code:
  on line 2515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2515-2515)
  on line 2517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2517-2517)
  on line 2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2519-2519)
  on line 2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2529-2529)
  on line 2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2531-2531)
  on line 2533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2533-2533)
  on line 2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2543-2543)
  on line 2545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2545-2545)
  on line 2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2547-2547)
  on line 2557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2557-2557)
  on line 2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2559-2559)
  on line 2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2561-2561)
  on line 2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2571-2571)
  on line 2573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2573-2573)
  on line 2575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2575-2575)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3117-3117)
  on line 3129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3129-3129)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 762
  dead: 780 (439 in uncalled functions)
  total lines: 1542
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3137:7-3137:18)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1778:17-1778:24)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1790:17-1790:35)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1791:19-1791:33)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:722:25-722:36)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1807:21-1807:28)
[Warning][Deadcode][CWE-571] condition 'p == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1374:7-1374:13)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1819:21-1819:39)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1820:23-1820:37)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3176:7-3176:18)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1836:25-1836:32)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:755:27-755:38)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1848:25-1848:43)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1849:27-1849:41)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:782:7-782:17)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3215:7-3215:18)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1439:7-1439:10)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1877:29-1877:47)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1878:31-1878:45)
[Warning][Deadcode][CWE-570] condition 'floor == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:809:9-809:19)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1472:7-1472:19)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1914:13-1914:20)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:836:11-836:21)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2412:7-2412:14)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1926:13-1926:31)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2425:7-2425:14)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1943:17-1943:24)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2438:7-2438:14)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:863:13-863:23)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1955:17-1955:35)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1956:19-1956:33)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2451:7-2451:14)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3654:13-3654:20)
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1972:21-1972:28)
[Warning][Deadcode][CWE-570] condition 'tmp___10' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2464:7-2464:15)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3665:15-3665:22)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:890:15-890:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:891:17-891:28)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1984:21-1984:39)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1985:23-1985:37)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3676:17-3676:24)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3687:19-3687:26)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2001:25-2001:32)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2513:9-2513:18)
[Warning][Deadcode][CWE-570] condition 'persons_0 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1589:7-1589:21)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2013:25-2013:43)
[Warning][Deadcode][CWE-570] condition 'persons_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1593:9-1593:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2014:27-2014:41)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2527:9-2527:18)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:934:9-934:20)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3715:13-3715:20)
[Warning][Deadcode][CWE-570] condition 'persons_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1597:11-1597:25)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2541:9-2541:18)
[Warning][Deadcode][CWE-570] condition 'persons_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1601:13-1601:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3394:10-3394:11)
[Warning][Deadcode][CWE-570] condition 'tmp___7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3726:15-3726:22)
[Warning][Deadcode][CWE-570] condition 'persons_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1605:15-1605:29)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3398:9-3398:23)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2555:9-2555:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:574:7-574:19)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3402:11-3402:23)
[Warning][Deadcode][CWE-570] condition 'persons_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1609:17-1609:31)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3737:17-3737:24)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2042:29-2042:47)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:577:9-577:21)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2043:31-2043:45)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2569:9-2569:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3414:9-3414:12)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:580:11-580:23)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:961:11-961:22)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:583:13-583:25)
[Warning][Deadcode][CWE-570] condition 'tmp___5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3748:19-3748:26)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1637:7-1637:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:586:15-586:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3394:10-3394:11)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3398:9-3398:23)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3402:11-3402:23)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1648:11-1648:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3414:9-3414:12)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1652:13-1652:27)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:988:13-988:24)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1659:15-1659:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3394:10-3394:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1663:17-1663:31)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3398:9-3398:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:623:19-623:30)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3402:11-3402:23)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1670:19-1670:26)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1674:21-1674:35)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1015:15-1015:26)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3394:10-3394:11)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1685:25-1685:39)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:656:21-656:32)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1042:17-1042:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2190:9-2190:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2194:11-2194:25)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2198:13-2198:27)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1749:13-1749:20)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:2202:15-2202:29)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_base' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:3114:15-3114:38)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1761:13-1761:31)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:689:23-689:34)
[Warning][Deadcode][CWE-571] condition 'p == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec3_productSimulator.cil.c:1313:7-1313:13)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
