./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_spec1_product30.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_spec1_product30.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_product30.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_product30.cil.c:87:3-106:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:134:3-153:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:237:3-258:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:294:3-319:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:379:5-399:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:724:3-752:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:784:3-827:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3153:5-3211:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3228:9-3286:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:69:1-111:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:112:1-158:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:166:1-211:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:212:1-267:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:268:1-327:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:330:1-432:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:433:1-478:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:479:1-524:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:546:1-555:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:581:1-632:1)
[Warning][Deadcode] Function 'bobCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:633:1-643:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:644:1-654:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:666:1-676:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:677:1-687:1)
[Warning][Deadcode] Function 'threeTS' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:699:1-710:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:758:1-835:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:836:1-847:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:848:1-859:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:860:1-870:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:871:1-887:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:975:1-1016:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1746:1-1768:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1769:1-1791:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1845:1-1876:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__weight' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1877:1-1888:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1889:1-1908:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2017:1-2025:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2026:1-2065:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2668:1-2681:1)
[Warning][Deadcode] Function 'printState__wrappee__twothirdsfull' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2950:1-3120:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3121:1-3142:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3143:1-3301:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:54-54)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__2' has dead code:
  on line 3325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3325-3325)
  on lines 3333..3334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3333-3334)
  on lines 3336..3337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3336-3337)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__3' has dead code:
  on line 3363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3363-3363)
  on line 3365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3365-3365)
  on lines 3367..3368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3367-3368)
  on line 3393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3393-3393)
  on line 3395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3395-3395)
  on lines 3397..3398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3397-3398)
  on line 3408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3408-3408)
  on line 3410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3410-3410)
  on lines 3412..3413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3412-3413)
  on line 3423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3423-3423)
  on line 3425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3425-3425)
  on lines 3427..3428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3427-3428)
[Warning][Deadcode] Function '__utac_acc__Specification1_spec__4' has dead code:
  on line 3451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3451-3451)
  on line 3456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3456-3456)
  on line 3464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3464-3464)
  on line 3466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3466-3466)
  on line 3469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3469-3469)
  on line 3471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3471-3471)
  on line 3480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3480-3480)
[Warning][Deadcode] Function 'anyStopRequested' has dead code:
  on lines 2079..2080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2079-2080)
  on lines 2083..2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2083-2084)
  on lines 2094..2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2094-2095)
  on lines 2104..2106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2104-2106)
  on line 2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2109-2109)
  on lines 2111..2113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2111-2113)
  on lines 2115..2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2115-2117)
  on line 2120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2120-2120)
  on lines 2122..2124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2122-2124)
  on lines 2126..2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2126-2128)
  on lines 2141..2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2141-2143)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1980-1980)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1991..1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1991-1993)
  on lines 1995..1997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1995-1997)
  on lines 1999..2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1999-2001)
  on lines 2003..2005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2003-2005)
  on lines 2007..2008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2007-2008)
  on line 2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2014-2014)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1090-1090)
  on lines 1098..1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1098-1099)
  on lines 1101..1102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1101-1102)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:745-745)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 2594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2594-2594)
  on lines 2599..2600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2599-2600)
  on line 2608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2608-2608)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1806-1806)
  on line 1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1809-1809)
  on line 1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1812-1812)
  on line 1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1815-1815)
  on line 1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1818-1818)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1971-1971)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 1690..1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1690-1691)
  on lines 1694..1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1694-1695)
  on lines 1698..1699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1698-1699)
  on lines 1702..1703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1702-1703)
  on lines 1706..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1706-1707)
  on lines 1713..1714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1713-1714)
  on line 1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1721-1721)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 1651..1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1651-1652)
  on lines 1655..1656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1655-1656)
  on lines 1663..1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1663-1664)
  on lines 1667..1668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1667-1668)
  on lines 1674..1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1674-1675)
  on line 1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1682-1682)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 1612..1613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1612-1613)
  on lines 1616..1617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1616-1617)
  on lines 1620..1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1620-1621)
  on lines 1624..1625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1624-1625)
  on lines 1628..1629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1628-1629)
  on lines 1635..1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1635-1636)
  on line 1643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1643-1643)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 1298..1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1298-1299)
  on lines 1301..1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1301-1302)
  on lines 1304..1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1304-1305)
  on lines 1307..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1307-1308)
  on lines 1310..1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1310-1311)
  on lines 1313..1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1313-1314)
  on line 1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1326-1326)
  on line 1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1329-1329)
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1332-1332)
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1335-1335)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1338-1338)
  on line 1353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1353-1353)
  on line 1356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1356-1356)
  on lines 1361..1362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1361-1362)
  on lines 1364..1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1364-1365)
  on lines 1367..1368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1367-1368)
  on lines 1378..1380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1378-1380)
  on lines 1382..1383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1382-1383)
  on lines 1385..1386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1385-1386)
  on lines 1388..1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1388-1389)
  on lines 1391..1392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1391-1392)
  on lines 1394..1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1394-1395)
  on lines 1405..1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1405-1407)
  on lines 1409..1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1409-1410)
  on lines 1412..1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1412-1413)
  on lines 1415..1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1415-1416)
  on lines 1418..1419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1418-1419)
  on lines 1421..1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1421-1422)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' has dead code:
  on lines 2555..2556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2555-2556)
  on lines 2559..2560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2559-2560)
  on lines 2563..2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2563-2564)
  on lines 2567..2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2567-2568)
  on lines 2571..2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2571-2572)
  on line 2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2581-2581)
[Warning][Deadcode] Function 'isBlocked' has dead code:
  on line 1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1798-1798)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 1033..1035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1033-1035)
  on lines 1037..1039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1037-1039)
  on lines 1047..1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1047-1049)
[Warning][Deadcode] Function 'isIdle' has dead code:
  on line 2156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2156-2156)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 1118..1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1118-1120)
  on lines 1122..1124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1122-1124)
  on lines 1126..1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1126-1128)
  on lines 1130..1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1130-1132)
  on lines 1134..1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1134-1136)
  on lines 1138..1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1138-1140)
  on lines 1183..1186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1183-1186)
  on lines 1188..1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1188-1190)
  on lines 1192..1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1192-1194)
  on lines 1196..1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1196-1198)
  on lines 1200..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1200-1202)
  on lines 1204..1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1204-1206)
  on lines 1216..1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1216-1219)
  on lines 1221..1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1221-1223)
  on lines 1225..1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1225-1227)
  on lines 1229..1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1229-1231)
  on lines 1233..1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1233-1235)
  on lines 1237..1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1237-1239)
  on lines 1249..1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1249-1252)
  on lines 1254..1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1254-1256)
  on lines 1258..1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1258-1260)
  on lines 1262..1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1262-1264)
  on lines 1266..1268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1266-1268)
  on lines 1270..1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1270-1272)
  on lines 1288..1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1288-1290)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1601-1601)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 927..929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:927-929)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1914-1914)
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1917-1917)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1920-1920)
  on lines 1925..1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1925-1926)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2702..2705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2702-2705)
  on lines 2715..2718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2715-2718)
  on lines 2728..2731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2728-2731)
  on lines 2741..2744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2741-2744)
  on lines 2754..2757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2754-2757)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 1449..1450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1449-1450)
  on lines 1452..1453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1452-1453)
  on lines 1455..1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1455-1456)
  on lines 1458..1459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1458-1459)
  on lines 1461..1462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1461-1462)
  on lines 1464..1465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1464-1465)
  on line 1477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1477-1477)
  on line 1480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1480-1480)
  on line 1483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1483-1483)
  on line 1486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1486-1486)
  on line 1489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1489-1489)
  on lines 1502..1504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1502-1504)
  on lines 1506..1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1506-1507)
  on lines 1509..1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1509-1510)
  on lines 1512..1513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1512-1513)
  on lines 1515..1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1515-1516)
  on lines 1518..1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1518-1519)
  on lines 1529..1531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1529-1531)
  on lines 1533..1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1533-1534)
  on lines 1536..1537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1536-1537)
  on lines 1539..1540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1539-1540)
  on lines 1542..1543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1542-1543)
  on lines 1545..1546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1545-1546)
  on lines 1556..1558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1556-1558)
  on lines 1560..1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1560-1561)
  on lines 1563..1564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1563-1564)
  on lines 1566..1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1566-1567)
  on lines 1569..1570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1569-1570)
  on lines 1572..1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1572-1573)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 1057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1057-1057)
  on lines 1062..1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1062-1063)
  on lines 1065..1066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1065-1066)
  on lines 1068..1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1068-1069)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1942-1942)
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1947-1948)
  on lines 1950..1951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1950-1951)
  on lines 1953..1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1953-1954)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:906-906)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on lines 2653..2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2653-2655)
  on line 2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2657-2657)
  on line 2665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2665-2665)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__empty' has dead code:
  on lines 2630..2631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2630-2631)
  on line 2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2637-2637)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on line 2528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2528-2528)
  on line 2530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2530-2530)
  on line 2532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2532-2532)
  on line 2535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2535-2535)
  on line 2538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2538-2538)
  on line 2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2547-2547)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__empty' has dead code:
  on lines 2179..2180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2179-2180)
  on line 2185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2185-2185)
  on line 2187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2187-2187)
  on lines 2189..2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2189-2191)
  on lines 2201..2204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2201-2204)
  on lines 2229..2233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2229-2233)
  on lines 2242..2243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2242-2243)
  on line 2245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2245-2245)
  on lines 2247..2249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2247-2249)
  on lines 2258..2262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2258-2262)
  on lines 2271..2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2271-2272)
  on line 2274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2274-2274)
  on lines 2276..2278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2276-2278)
  on lines 2287..2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2287-2291)
  on lines 2300..2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2300-2301)
  on line 2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2303-2303)
  on lines 2305..2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2305-2307)
  on lines 2316..2320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2316-2320)
  on lines 2322..2323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2322-2323)
  on lines 2326..2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2326-2327)
  on lines 2330..2331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2330-2331)
  on lines 2343..2345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2343-2345)
  on lines 2349..2350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2349-2350)
  on line 2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2352-2352)
  on lines 2354..2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2354-2356)
  on lines 2365..2369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2365-2369)
  on lines 2378..2379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2378-2379)
  on line 2381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2381-2381)
  on lines 2383..2385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2383-2385)
  on lines 2394..2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2394-2398)
  on lines 2407..2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2407-2408)
  on line 2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2410-2410)
  on lines 2412..2414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2412-2414)
  on lines 2423..2427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2423-2427)
  on lines 2436..2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2436-2437)
  on line 2439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2439-2439)
  on lines 2441..2443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2441-2443)
  on lines 2452..2456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2452-2456)
  on lines 2465..2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2465-2466)
  on line 2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2468-2468)
  on lines 2470..2472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2470-2472)
  on lines 2481..2485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2481-2485)
  on lines 2487..2488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2487-2488)
  on lines 2491..2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2491-2492)
  on lines 2495..2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2495-2496)
  on line 2508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2508-2508)
[Warning][Deadcode] Function 'timeShift__wrappee__twothirdsfull' has dead code:
  on line 2802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2802-2802)
  on line 2804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2804-2804)
  on line 2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2806-2806)
  on line 2816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2816-2816)
  on line 2818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2818-2818)
  on line 2820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2820-2820)
  on line 2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2830-2830)
  on line 2832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2832-2832)
  on line 2834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2834-2834)
  on line 2844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2844-2844)
  on line 2846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2846-2846)
  on line 2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2848-2848)
  on line 2858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2858-2858)
  on line 2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2860-2860)
  on line 2862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2862-2862)
  on line 2872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2872-2872)
  on line 2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2874-2874)
  on line 2876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2876-2876)
  on lines 2903..2904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2903-2904)
  on line 2906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2906-2906)
  on lines 2908..2909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2908-2909)
  on line 2913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2913-2913)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:576-576)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 343
  dead: 1077 (543 in uncalled functions)
  total lines: 1420
[Warning][Deadcode][CWE-570] condition 'tmp___3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2078:7-2078:14)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2739:7-2739:14)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1059:9-1059:21)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:728:9-728:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2082:9-2082:23)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1448:7-1448:17)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:732:11-732:23)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3392:11-3392:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1650:7-1650:18)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2752:7-2752:14)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:744:9-744:12)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1654:9-1654:20)
[Warning][Deadcode][CWE-570] condition 'overload' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2527:7-2527:15)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2093:13-2093:27)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3407:13-3407:23)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2765:7-2765: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_product30.cil.c:724:10-724:11)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1089:7-1089:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1662:13-1662:24)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2100:15-2100:22)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:728:9-728:23)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1666:15-1666:26)
[Warning][Deadcode][CWE-570] condition 'floor == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3422:15-3422:25)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1475:9-1475:19)
[Warning][Deadcode][CWE-571] condition 'floorID == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1095:11-1095:23)
[Warning][Deadcode][CWE-571] condition 'tmp___0 != 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:732:11-732:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2554:7-2554:21)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1476:11-1476:22)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1670:17-1670:28)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1479:13-1479:24)
[Warning][Deadcode][CWE-570] condition 'floorButtons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2558:9-2558:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:744:9-744:12)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1913:7-1913:19)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2800:9-2800:18)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1482:15-1482:26)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3449:7-3449:28)
[Warning][Deadcode][CWE-570] condition 'floorButtons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2562:11-2562:25)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1916:9-1916:21)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1485:17-1485:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1117:7-1117:17)
[Warning][Deadcode][CWE-570] condition 'landingButtons_spc1_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3454:9-3454:30)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1689:7-1689:18)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1297:7-1297:17)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1919:11-1919:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:724:10-724:11)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2814:9-2814:18)
[Warning][Deadcode][CWE-570] condition 'floorButtons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2566:13-2566:27)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1488:19-1488:30)
[Warning][Deadcode][CWE-571] condition 'landingButtons_spc1_2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3459:11-3459:32)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1922:13-1922:25)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1693:9-1693:20)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1491:21-1491:32)
[Warning][Deadcode][CWE-571] condition 'i < __cil_tmp4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:728:9-728:23)
[Warning][Deadcode][CWE-570] condition 'floorButtons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2570:15-2570:29)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2828:9-2828:18)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1697:11-1697:22)
[Warning][Deadcode][CWE-570] condition 'tmp___0 != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:732:11-732:23)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1941:7-1941:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1701:13-1701:24)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2842:9-2842:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1944:9-1944:21)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2589:7-2589:26)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1705:15-1705:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2593:9-2593:12)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2856:9-2856:18)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1709:17-1709:28)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1325:11-1325:22)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2174:7-2174:15)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1328:13-1328:24)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:919:7-919:10)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1150:9-1150:19)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2605:7-2605:26)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2178:9-2178:12)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2870:9-2870:18)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1331:15-1331:26)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2184:9-2184:27)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1334:17-1334:28)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1337:19-1337:30)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2889:9-2889:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1987:7-1987:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1340:21-1340:32)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1351:11-1351:21)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2629:9-2629:12)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2200:11-2200:29)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1352:13-1352:24)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2897:9-2897:16)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1355:15-1355:26)
[Warning][Deadcode][CWE-571] condition 'person == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1358:17-1358:28)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1171:21-1171:32)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2213:13-2213:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2214:15-2214:32)
[Warning][Deadcode][CWE-570] condition 'weight > __cil_tmp5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2651:7-2651:26)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2218:17-2218:24)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3324:7-3324:17)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1805:7-1805:13)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1808:9-1808:15)
[Warning][Deadcode][CWE-571] condition 'floor == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3330:11-3330:21)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2700:7-2700:14)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1811:11-1811:17)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1611:7-1611:18)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1814:13-1814:19)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1817:15-1817:21)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1615:9-1615:20)
[Warning][Deadcode][CWE-571] condition 'floorID == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1029:11-1029:23)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2713:7-2713:14)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1820:17-1820:23)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1619:11-1619:22)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3362:7-3362:17)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1623:13-1623:24)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:2726:7-2726:14)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1627:15-1627:26)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:3377:9-3377:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:724:10-724:11)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1631:17-1631:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec1_product30.cil.c:1056:7-1056:19)
[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
