./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_spec1_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_spec1_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_spec1_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_spec1_productSimulator.cil.c:204:3-225:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:261:3-286:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:346:5-366:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3066:5-3124:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3141:9-3199:9 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3256:3-3275:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3303:3-3322:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3472:3-3500:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3532:3-3575: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] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1588:3-1588:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2417:5-2417:40)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2419:5-2419:40)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1527:3-1527:24)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:133:1-178:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:179:1-234:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:235:1-294:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:297:1-399:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:400:1-445:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:446:1-491:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:748:1-789:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1406:1-1428:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1429:1-1451:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1755:1-1763:1)
[Warning][Deadcode] Function 'printState__before__overloaded' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2846:1-3016:1)
[Warning][Deadcode] Function 'printState__role__overloaded' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3017:1-3038:1)
[Warning][Deadcode] Function 'printState' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3039:1-3055:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3056:1-3214:1)
[Warning][Deadcode] Function 'isExecutiveFloor' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3226:1-3234:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3238:1-3280:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3281:1-3327:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3330:1-3381:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3382:1-3392:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3393:1-3403:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3415:1-3425:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3426:1-3436:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3448:1-3459:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3506:1-3583:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3584:1-3595:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3596:1-3607:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3608:1-3618:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3619:1-3635:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:498-498)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__2' has dead code:
  on line 546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:546-546)
  on lines 554..555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:554-555)
  on lines 557..558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:557-558)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__3' has dead code:
  on line 586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:586-586)
  on lines 588..589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:588-589)
  on line 631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:631-631)
  on lines 633..634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:633-634)
  on line 646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:646-646)
  on lines 648..649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:648-649)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__4' has dead code:
  on line 672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:672-672)
  on line 677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:677-677)
  on line 687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:687-687)
  on line 692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:692-692)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 1817..1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1817-1818)
  on lines 1821..1822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1821-1822)
  on lines 1843..1844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1843-1844)
  on lines 1850..1851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1850-1851)
  on lines 1861..1862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1861-1862)
  on lines 1865..1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1865-1866)
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1881-1881)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1718-1718)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on line 1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1752-1752)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:862-862)
  on lines 870..871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:870-871)
  on lines 873..874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:873-874)
[Warning][Deadcode] Function 'enterElevator__before__weight' has dead code:
  on line 1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1493-1493)
  on line 1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1496-1496)
  on line 1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1502-1502)
  on line 1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1505-1505)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1709-1709)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 3762..3763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3762-3763)
  on lines 3766..3767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3766-3767)
  on lines 3774..3775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3774-3775)
  on lines 3778..3779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3778-3779)
  on lines 3785..3786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3785-3786)
  on line 3793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3793-3793)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 3723..3724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3723-3724)
  on lines 3727..3728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3727-3728)
  on lines 3735..3736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3735-3736)
  on lines 3739..3740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3739-3740)
  on lines 3746..3747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3746-3747)
  on line 3754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3754-3754)
[Warning][Deadcode] Function 'getReverseHeading' has dead code:
  on line 2557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2557-2557)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 3684..3685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3684-3685)
  on lines 3688..3689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3688-3689)
  on lines 3696..3697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3696-3697)
  on lines 3700..3701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3700-3701)
  on lines 3707..3708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3707-3708)
  on line 3715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3715-3715)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 1070..1071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1070-1071)
  on lines 1073..1074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1073-1074)
  on lines 1076..1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1076-1077)
  on lines 1079..1080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1079-1080)
  on lines 1082..1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1082-1083)
  on lines 1085..1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1085-1086)
  on line 1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1098-1098)
  on line 1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1101-1101)
  on line 1104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1104-1104)
  on line 1107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1107-1107)
  on line 1110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1110-1110)
  on line 1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1125-1125)
  on line 1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1128-1128)
  on lines 1133..1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1133-1134)
  on lines 1136..1137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1136-1137)
  on lines 1139..1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1139-1140)
  on lines 1150..1152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1150-1152)
  on lines 1154..1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1154-1155)
  on lines 1157..1158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1157-1158)
  on lines 1160..1161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1160-1161)
  on lines 1163..1164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1163-1164)
  on lines 1166..1167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1166-1167)
  on lines 1177..1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1177-1179)
  on lines 1181..1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1181-1182)
  on lines 1184..1185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1184-1185)
  on lines 1187..1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1187-1188)
  on lines 1190..1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1190-1191)
  on lines 1193..1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1193-1194)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2366..2367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2366-2367)
  on lines 2374..2375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2374-2375)
  on lines 2382..2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2382-2383)
  on line 2392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2392-2392)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1485-1485)
[Warning][Deadcode] Function 'isBlocked__before__overloaded' has dead code:
  on line 1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1458-1458)
[Warning][Deadcode] Function 'isBlocked__role__overloaded' has dead code:
  on line 1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1467-1467)
[Warning][Deadcode] Function 'isEmpty' has dead code:
  on lines 1769..1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1769-1770)
  on lines 1773..1774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1773-1774)
  on lines 1781..1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1781-1782)
  on lines 1785..1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1785-1786)
  on line 1801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1801-1801)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 3223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3223-3223)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:822-822)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 1894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1894-1894)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on line 1062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1062-1062)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1373-1373)
[Warning][Deadcode] Function 'leaveElevator__before__weight' has dead code:
  on line 1554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1554-1554)
  on line 1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1557-1557)
  on line 1563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1563-1563)
  on line 1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1566-1566)
[Warning][Deadcode] Function 'main' has dead code:
  on line 3675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3675-3675)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1652-1652)
  on line 1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1658-1658)
  on lines 1663..1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1663-1664)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2580..2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2580-2583)
  on lines 2593..2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2593-2596)
  on lines 2619..2622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2619-2622)
  on lines 2632..2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2632-2635)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on line 1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1222-1222)
  on line 1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1225-1225)
  on lines 1230..1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1230-1231)
  on lines 1233..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1233-1234)
  on lines 1236..1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1236-1237)
  on line 1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1249-1249)
  on line 1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1252-1252)
  on line 1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1258-1258)
  on line 1261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1261-1261)
  on line 1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1276-1276)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1279-1279)
  on lines 1284..1285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1284-1285)
  on lines 1287..1288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1287-1288)
  on lines 1290..1291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1290-1291)
  on line 1303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1303-1303)
  on line 1306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1306-1306)
  on lines 1311..1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1311-1312)
  on lines 1314..1315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1314-1315)
  on lines 1317..1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1317-1318)
  on line 1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1330-1330)
  on line 1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1333-1333)
  on lines 1338..1339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1338-1339)
  on lines 1341..1342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1341-1342)
  on lines 1344..1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1344-1345)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 67 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:67-67)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2543-2543)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__before__executivefloor' has dead code:
  on line 2494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2494-2494)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__before__twothirdsfull' has dead code:
  on line 2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2448-2448)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__role__executivefloor' has dead code:
  on line 2508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2508-2508)
  on line 2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2510-2510)
  on line 2512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2512-2512)
  on line 2514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2514-2514)
  on lines 2516..2517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2516-2517)
  on line 2525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2525-2525)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__role__twothirdsfull' has dead code:
  on line 2476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2476-2476)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 2358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2358-2358)
[Warning][Deadcode] Function 'stopRequestedInDirection__before__executivefloor' has dead code:
  on line 2308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2308-2308)
[Warning][Deadcode] Function 'stopRequestedInDirection__before__twothirdsfull' has dead code:
  on lines 1929..1930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1929-1930)
  on lines 1942..1943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1942-1943)
  on lines 2000..2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2000-2001)
  on lines 2016..2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2016-2017)
  on lines 2045..2046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2045-2046)
  on lines 2058..2059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2058-2059)
  on lines 2065..2066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2065-2066)
  on lines 2094..2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2094-2095)
  on lines 2107..2108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2107-2108)
  on lines 2123..2124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2123-2124)
  on lines 2165..2166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2165-2166)
  on lines 2181..2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2181-2182)
  on lines 2210..2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2210-2211)
  on lines 2223..2224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2223-2224)
  on lines 2230..2231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2230-2231)
  on line 2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2247-2247)
[Warning][Deadcode] Function 'stopRequestedInDirection__role__executivefloor' has dead code:
  on lines 2325..2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2325-2328)
  on line 2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2330-2330)
  on line 2338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2338-2338)
[Warning][Deadcode] Function 'stopRequestedInDirection__role__twothirdsfull' has dead code:
  on line 2287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2287-2287)
[Warning][Deadcode] Function 'timeShift' has dead code:
  on line 2842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2842-2842)
[Warning][Deadcode] Function 'timeShift__before__overloaded' has dead code:
  on line 2680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2680-2680)
  on line 2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2682-2682)
  on line 2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2684-2684)
  on line 2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2694-2694)
  on line 2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2696-2696)
  on line 2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2698-2698)
  on line 2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2722-2722)
  on line 2724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2724-2724)
  on line 2726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2726-2726)
  on line 2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2736-2736)
  on line 2738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2738-2738)
  on line 2740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2740-2740)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:111-111)
  on line 123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:123-123)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 768
  dead: 775 (494 in uncalled functions)
  total lines: 1543
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1651:7-1651:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1657:11-1657:23)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2578:7-2578:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1660:13-1660:25)
[Warning][Deadcode][CWE-570] condition 'tmp___9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2093:13-2093:20)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2591:7-2591:14)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2105:13-2105:31)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2106:15-2106:29)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1221:9-1221:20)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2122:17-2122:24)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1224:11-1224:22)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2617:7-2617:14)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1227:13-1227:24)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2134:17-2134:35)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:861:7-861:19)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2630:7-2630:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:867:11-867:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1248:11-1248:22)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1251:13-1251:24)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2163:21-2163:39)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2164:23-2164:37)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1257:17-1257:28)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1260:19-1260:30)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1263:21-1263:32)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2678:9-2678:18)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2180:25-2180:32)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1275:13-1275:24)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2692:9-2692:18)
[Warning][Deadcode][CWE-570] condition 'persons_0 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1768:7-1768:21)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1278:15-1278:26)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1281:17-1281:28)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2192:25-2192:43)
[Warning][Deadcode][CWE-570] condition 'persons_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1772:9-1772:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:910:19-910:30)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_base' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:108:15-108:38)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2720:9-2720:18)
[Warning][Deadcode][CWE-570] condition 'persons_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1780:13-1780:27)
[Warning][Deadcode][CWE-570] condition 'tmp___5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2209:29-2209:36)
[Warning][Deadcode][CWE-570] condition 'persons_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1784:15-1784:29)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1302:15-1302:26)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2734:9-2734:18)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1305:17-1305:28)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2221:29-2221:47)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1308:19-1308:30)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2222:31-2222:45)
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1816:7-1816:14)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:943:21-943:32)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1820:9-1820:23)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3683:7-3683:18)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1329:17-1329:28)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1332:19-1332:30)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3687:9-3687:20)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1335:21-1335:32)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3695:13-3695:24)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3699:15-3699:26)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1842:17-1842:31)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3703:17-3703:28)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:976:23-976:34)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1849:19-1849:26)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3722:7-3722:18)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2323:7-2323:14)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3726:9-3726:20)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:545:7-545:17)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1860:23-1860:26)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1864:25-1864:39)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:551:11-551:21)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3734:13-3734:24)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3738:15-3738:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3742:17-3742:28)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1009:25-1009:36)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2365:7-2365:21)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:584:9-584:30)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3761:7-3761:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2373:11-2373:25)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3765:9-3765:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3472:10-3472:11)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1928:13-1928:20)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3476:9-3476:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2381:15-2381:29)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3480:11-3480:23)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3773:13-3773:24)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1940:13-1940:31)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1941:15-1941:29)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3777:15-3777:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3492:9-3492:12)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1492:7-1492:13)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1042:27-1042:38)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3781:17-3781:28)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1495:9-1495:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3472:10-3472:11)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:629:15-629:36)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1069:7-1069:17)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1501:13-1501:19)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3476:9-3476:23)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1504:15-1504:21)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3480:11-3480:23)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1969:17-1969:35)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1507:17-1507:23)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:644:17-644:38)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3492:9-3492:12)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:670:7-670:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3472:10-3472:11)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:675:9-675:30)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1097:11-1097:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3476:9-3476:23)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1553:7-1553:13)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1100:13-1100:24)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:685:13-685:34)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1998:21-1998:39)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1999:23-1999:37)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1556:9-1556:15)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1103:15-1103:26)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:690:15-690:36)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3492:9-3492:12)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1106:17-1106:28)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1562:13-1562:19)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1109:19-1109:30)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1565:15-1565:21)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1112:21-1112:32)
[Warning][Deadcode][CWE-570] condition 'tmp___1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2015:25-2015:32)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1568:17-1568:23)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1123:11-1123:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:3472:10-3472:11)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1124:13-1124:24)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1127:15-1127:26)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2027:25-2027:43)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:1130:17-1130:28)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2506:7-2506:10)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2044:29-2044:36)
[Warning][Deadcode][CWE-571] condition 'respectInLiftCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2056:29-2056:47)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_productSimulator.cil.c:2057:31-2057:45)
[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)
