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


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:268:5-288:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:445:3-464:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:492:3-511:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:703:3-731:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:763:3-806:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3028:5-3086:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3103:9-3161: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'spec1' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:427:1-469:1)
[Warning][Deadcode] Function 'spec14' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:470:1-516:1)
[Warning][Deadcode] Function 'get_nondetMinMax07' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:560:1-611:1)
[Warning][Deadcode] Function 'aliceCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:623:1-633:1)
[Warning][Deadcode] Function 'angelinaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:634:1-644:1)
[Warning][Deadcode] Function 'chuckCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:645:1-655:1)
[Warning][Deadcode] Function 'monicaCall' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:656:1-666:1)
[Warning][Deadcode] Function 'randomSequenceOfActions' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:737:1-814:1)
[Warning][Deadcode] Function 'runTest_Simple' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:815:1-826:1)
[Warning][Deadcode] Function 'Specification1' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:827:1-838:1)
[Warning][Deadcode] Function 'Specification2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:839:1-849:1)
[Warning][Deadcode] Function 'Specification3' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:850:1-866:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:913:1-922:1)
[Warning][Deadcode] Function 'initFloors' is uncalled: 36 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1003:1-1044:1)
[Warning][Deadcode] Function 'initTopDown' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1649:1-1671:1)
[Warning][Deadcode] Function 'initBottomUp' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1672:1-1694:1)
[Warning][Deadcode] Function 'isBlocked' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1695:1-1703:1)
[Warning][Deadcode] Function 'leaveElevator__wrappee__base' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1748:1-1779:1)
[Warning][Deadcode] Function 'leaveElevator' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1780:1-1791:1)
[Warning][Deadcode] Function 'getCurrentHeading' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1900:1-1908:1)
[Warning][Deadcode] Function 'isEmpty' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1909:1-1948:1)
[Warning][Deadcode] Function 'anyStopRequested' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1949:1-2028:1)
[Warning][Deadcode] Function 'isIdle' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2029:1-2041:1)
[Warning][Deadcode] Function 'isAnyLiftButtonPressed' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2423:1-2456:1)
[Warning][Deadcode] Function 'getReverseHeading' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2544:1-2557:1)
[Warning][Deadcode] Function 'printState__wrappee__executivefloor' is uncalled: 60 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2825:1-2995:1)
[Warning][Deadcode] Function 'printState' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2996:1-3017:1)
[Warning][Deadcode] Function 'existInLiftCallsInDirection' is uncalled: 70 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3018:1-3176:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3321-3321)
[Warning][Deadcode] Function 'areDoorsOpen' has dead code:
  on line 1863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1863-1863)
[Warning][Deadcode] Function 'buttonForFloorIsPressed' has dead code:
  on lines 1874..1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1874-1876)
  on lines 1878..1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1878-1880)
  on lines 1882..1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1882-1884)
  on lines 1886..1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1886-1888)
  on lines 1890..1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1890-1891)
  on line 1897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1897-1897)
[Warning][Deadcode] Function 'callOnFloor' has dead code:
  on line 1113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1113-1113)
  on line 1119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1119-1119)
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1122-1122)
[Warning][Deadcode] Function 'cleanup' has dead code:
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:700-700)
  on line 703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:703-703)
  on lines 706..707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:706-707)
  on line 709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:709-709)
  on line 711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:711-711)
  on line 721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:721-721)
  on lines 723..724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:723-724)
  on line 727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:727-727)
  on line 730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:730-730)
  on line 734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:734-734)
[Warning][Deadcode] Function 'continueInDirection' has dead code:
  on line 2467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2467-2467)
  on lines 2472..2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2472-2473)
  on line 2481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2481-2481)
[Warning][Deadcode] Function 'enterElevator__wrappee__base' has dead code:
  on line 1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1709-1709)
  on line 1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1712-1712)
  on line 1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1715-1715)
  on line 1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1718-1718)
  on line 1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1721-1721)
[Warning][Deadcode] Function 'getCurrentFloorID' has dead code:
  on line 1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1854-1854)
[Warning][Deadcode] Function 'getDestination' has dead code:
  on lines 3281..3282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3281-3282)
  on lines 3285..3286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3285-3286)
  on lines 3289..3290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3289-3290)
  on lines 3293..3294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3293-3294)
  on lines 3297..3298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3297-3298)
  on lines 3304..3305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3304-3305)
  on line 3312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3312-3312)
[Warning][Deadcode] Function 'getOrigin' has dead code:
  on lines 3246..3247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3246-3247)
  on lines 3250..3251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3250-3251)
  on lines 3254..3255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3254-3255)
  on lines 3258..3259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3258-3259)
  on lines 3265..3266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3265-3266)
  on line 3273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3273-3273)
[Warning][Deadcode] Function 'getWeight' has dead code:
  on lines 3203..3204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3203-3204)
  on lines 3207..3208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3207-3208)
  on lines 3211..3212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3211-3212)
  on lines 3215..3216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3215-3216)
  on lines 3219..3220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3219-3220)
  on lines 3226..3227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3226-3227)
  on line 3234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3234-3234)
[Warning][Deadcode] Function 'initPersonOnFloor' has dead code:
  on lines 1321..1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1321-1322)
  on lines 1324..1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1324-1325)
  on lines 1327..1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1327-1328)
  on lines 1330..1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1330-1331)
  on lines 1333..1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1333-1334)
  on lines 1336..1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1336-1337)
  on line 1349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1349-1349)
  on line 1352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1352-1352)
  on line 1355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1355-1355)
  on line 1358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1358-1358)
  on line 1361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1361-1361)
  on lines 1375..1376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1375-1376)
  on lines 1378..1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1378-1379)
  on lines 1381..1382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1381-1382)
  on lines 1384..1385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1384-1385)
  on lines 1387..1388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1387-1388)
  on lines 1390..1391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1390-1391)
  on lines 1402..1403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1402-1403)
  on lines 1405..1406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1405-1406)
  on lines 1408..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1408-1409)
  on lines 1411..1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1411-1412)
  on lines 1414..1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1414-1415)
  on lines 1417..1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1417-1418)
  on lines 1432..1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1432-1433)
  on lines 1435..1436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1435-1436)
  on lines 1438..1439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1438-1439)
  on lines 1441..1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1441-1442)
  on lines 1444..1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1444-1445)
[Warning][Deadcode] Function 'isExecutiveFloor' has dead code:
  on line 3194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3194-3194)
[Warning][Deadcode] Function 'isExecutiveFloorCalling' has dead code:
  on line 3185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3185-3185)
[Warning][Deadcode] Function 'isFloorCalling' has dead code:
  on lines 1058..1059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1058-1059)
  on lines 1062..1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1062-1063)
  on lines 1075..1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1075-1077)
[Warning][Deadcode] Function 'isPersonOnFloor' has dead code:
  on lines 1141..1143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1141-1143)
  on lines 1145..1147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1145-1147)
  on lines 1149..1151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1149-1151)
  on lines 1153..1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1153-1155)
  on lines 1157..1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1157-1159)
  on lines 1161..1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1161-1163)
  on lines 1206..1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1206-1209)
  on lines 1211..1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1211-1213)
  on lines 1215..1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1215-1217)
  on lines 1219..1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1219-1221)
  on lines 1223..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1223-1225)
  on lines 1227..1229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1227-1229)
  on lines 1239..1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1239-1242)
  on lines 1244..1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1244-1246)
  on lines 1248..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1248-1250)
  on lines 1252..1254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1252-1254)
  on lines 1256..1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1256-1258)
  on lines 1260..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1260-1262)
  on lines 1272..1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1272-1275)
  on lines 1277..1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1277-1279)
  on lines 1281..1283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1281-1283)
  on lines 1285..1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1285-1287)
  on lines 1289..1291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1289-1291)
  on lines 1293..1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1293-1295)
  on lines 1311..1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1311-1313)
[Warning][Deadcode] Function 'isTopFloor' has dead code:
  on line 1624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1624-1624)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 906..908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:906-908)
[Warning][Deadcode] Function 'pressInLiftFloorButton' has dead code:
  on line 1797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1797-1797)
  on line 1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1800-1800)
  on line 1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1803-1803)
  on lines 1808..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1808-1809)
[Warning][Deadcode] Function 'processWaitingOnFloor' has dead code:
  on lines 2578..2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2578-2581)
  on lines 2591..2594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2591-2594)
  on lines 2604..2607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2604-2607)
  on lines 2617..2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2617-2620)
  on lines 2630..2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2630-2633)
[Warning][Deadcode] Function 'removePersonFromFloor' has dead code:
  on lines 1472..1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1472-1473)
  on lines 1475..1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1475-1476)
  on lines 1478..1479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1478-1479)
  on lines 1481..1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1481-1482)
  on lines 1484..1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1484-1485)
  on lines 1487..1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1487-1488)
  on line 1500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1500-1500)
  on line 1503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1503-1503)
  on line 1506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1506-1506)
  on line 1509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1509-1509)
  on line 1512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1512-1512)
  on lines 1525..1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1525-1527)
  on lines 1529..1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1529-1530)
  on lines 1532..1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1532-1533)
  on lines 1535..1536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1535-1536)
  on lines 1538..1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1538-1539)
  on lines 1541..1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1541-1542)
  on lines 1552..1554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1552-1554)
  on lines 1556..1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1556-1557)
  on lines 1559..1560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1559-1560)
  on lines 1562..1563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1562-1563)
  on lines 1565..1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1565-1566)
  on lines 1568..1569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1568-1569)
  on lines 1579..1581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1579-1581)
  on lines 1583..1584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1583-1584)
  on lines 1586..1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1586-1587)
  on lines 1589..1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1589-1590)
  on lines 1592..1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1592-1593)
  on lines 1595..1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1595-1596)
[Warning][Deadcode] Function 'resetCallOnFloor' has dead code:
  on line 1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1085-1085)
  on lines 1090..1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1090-1091)
  on lines 1093..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1093-1094)
  on lines 1096..1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1096-1097)
[Warning][Deadcode] Function 'resetFloorButton' has dead code:
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1825-1825)
  on lines 1830..1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1830-1831)
  on lines 1833..1834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1833-1834)
  on lines 1836..1837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1836-1837)
[Warning][Deadcode] Function 'runTest' has dead code:
  on line 882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:882-882)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor' has dead code:
  on line 2524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2524-2524)
  on line 2526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2526-2526)
  on line 2528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2528-2528)
  on line 2530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2530-2530)
  on lines 2532..2533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2532-2533)
  on line 2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2541-2541)
[Warning][Deadcode] Function 'stopRequestedAtCurrentFloor__wrappee__weight' has dead code:
  on lines 2503..2504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2503-2504)
  on line 2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2510-2510)
[Warning][Deadcode] Function 'stopRequestedInDirection' has dead code:
  on lines 2407..2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2407-2410)
  on line 2412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2412-2412)
  on line 2420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2420-2420)
[Warning][Deadcode] Function 'stopRequestedInDirection__wrappee__weight' has dead code:
  on lines 2062..2063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2062-2063)
  on line 2068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2068-2068)
  on line 2070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2070-2070)
  on lines 2072..2074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2072-2074)
  on lines 2084..2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2084-2087)
  on lines 2112..2116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2112-2116)
  on lines 2125..2126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2125-2126)
  on line 2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2128-2128)
  on lines 2130..2132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2130-2132)
  on lines 2141..2145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2141-2145)
  on lines 2154..2155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2154-2155)
  on line 2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2157-2157)
  on lines 2159..2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2159-2161)
  on lines 2170..2174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2170-2174)
  on lines 2183..2184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2183-2184)
  on line 2186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2186-2186)
  on lines 2188..2190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2188-2190)
  on lines 2199..2203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2199-2203)
  on lines 2205..2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2205-2206)
  on lines 2209..2210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2209-2210)
  on lines 2213..2214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2213-2214)
  on lines 2226..2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2226-2228)
  on lines 2232..2233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2232-2233)
  on line 2235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2235-2235)
  on lines 2237..2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2237-2239)
  on lines 2248..2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2248-2252)
  on lines 2261..2262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2261-2262)
  on line 2264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2264-2264)
  on lines 2266..2268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2266-2268)
  on lines 2277..2281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2277-2281)
  on lines 2290..2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2290-2291)
  on line 2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2293-2293)
  on lines 2295..2297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2295-2297)
  on lines 2306..2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2306-2310)
  on lines 2319..2320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2319-2320)
  on line 2322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2322-2322)
  on lines 2324..2326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2324-2326)
  on lines 2335..2339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2335-2339)
  on lines 2348..2349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2348-2349)
  on line 2351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2351-2351)
  on lines 2353..2355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2353-2355)
  on lines 2364..2368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2364-2368)
  on lines 2370..2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2370-2371)
  on lines 2374..2375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2374-2375)
  on lines 2378..2379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2378-2379)
  on line 2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2391-2391)
[Warning][Deadcode] Function 'test' has dead code:
  on line 957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:957-957)
[Warning][Deadcode] Function 'timeShift__wrappee__executivefloor' has dead code:
  on line 2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2678-2678)
  on line 2680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2680-2680)
  on line 2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2682-2682)
  on line 2692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2692-2692)
  on line 2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2694-2694)
  on line 2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2696-2696)
  on line 2706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2706-2706)
  on line 2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2708-2708)
  on line 2710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2710-2710)
  on line 2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2720-2720)
  on line 2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2722-2722)
  on line 2724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2724-2724)
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2734-2734)
  on line 2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2736-2736)
  on line 2738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2738-2738)
  on line 2748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2748-2748)
  on line 2750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2750-2750)
  on line 2752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2752-2752)
  on lines 2779..2780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2779-2780)
  on line 2782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2782-2782)
  on lines 2784..2785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2784-2785)
  on line 2789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2789-2789)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:943-943)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 288
  dead: 1072 (593 in uncalled functions)
  total lines: 1360
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3202:7-3202:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1084:7-1084:19)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3206:9-3206:20)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1471:7-1471:17)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1087:9-1087:21)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2576:7-2576:14)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3210:11-3210:22)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3214:13-3214:24)
[Warning][Deadcode][CWE-570] condition 'p == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1708:7-1708:13)
[Warning][Deadcode][CWE-570] condition 'tmp___2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2589:7-2589:14)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3218:15-3218:26)
[Warning][Deadcode][CWE-570] condition 'p == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1711:9-1711:15)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1112:7-1112:19)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3222:17-3222:28)
[Warning][Deadcode][CWE-570] condition 'p == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1714:11-1714:17)
[Warning][Deadcode][CWE-570] condition 'p == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1717:13-1717:19)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1498:9-1498:19)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1118:11-1118:23)
[Warning][Deadcode][CWE-570] condition 'tmp___4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2602:7-2602:14)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1499:11-1499:22)
[Warning][Deadcode][CWE-570] condition 'p == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1720:15-1720:21)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1121:13-1121:25)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1502:13-1502:24)
[Warning][Deadcode][CWE-571] condition 'p == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1723:17-1723:23)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1124:15-1124:27)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1505:15-1505:26)
[Warning][Deadcode][CWE-570] condition 'tmp___6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2615:7-2615:14)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3245:9-3245:20)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1508:17-1508:28)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1140:7-1140:17)
[Warning][Deadcode][CWE-570] condition 'floor == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1320:7-1320:17)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:538:9-538:16)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3249:11-3249:22)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1511:19-1511:30)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:544:11-544:18)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1514:21-1514:32)
[Warning][Deadcode][CWE-570] condition 'tmp___8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2628:7-2628:14)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3253:13-3253:24)
[Warning][Deadcode][CWE-570] condition 'tmp___0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2405:7-2405:14)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:898:7-898:10)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3257:15-3257:26)
[Warning][Deadcode][CWE-571] condition 'tmp___10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2641:7-2641:15)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3261:17-3261:28)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1348:11-1348:22)
[Warning][Deadcode][CWE-570] condition 'person == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3280:7-3280:18)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1351:13-1351:24)
[Warning][Deadcode][CWE-571] condition 'floor == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1173:9-1173:19)
[Warning][Deadcode][CWE-570] condition 'person == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3284:9-3284:20)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1354:15-1354:26)
[Warning][Deadcode][CWE-570] condition 'persons_0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2676:9-2676:18)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1796:7-1796:19)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1357:17-1357:28)
[Warning][Deadcode][CWE-570] condition 'person == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3288:11-3288:22)
[Warning][Deadcode][CWE-570] condition 'floorID == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1799:9-1799:21)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1360:19-1360:30)
[Warning][Deadcode][CWE-570] condition 'persons_1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2690:9-2690:18)
[Warning][Deadcode][CWE-570] condition 'person == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3292:13-3292:24)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1802:11-1802:23)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1363:21-1363:32)
[Warning][Deadcode][CWE-571] condition 'floorID == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1805:13-1805:25)
[Warning][Deadcode][CWE-570] condition 'person == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3296:15-3296:26)
[Warning][Deadcode][CWE-570] condition 'floor == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1374:11-1374:21)
[Warning][Deadcode][CWE-570] condition 'persons_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2704:9-2704:18)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:3300:17-3300:28)
[Warning][Deadcode][CWE-570] condition 'floorID == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1824:7-1824:19)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2462:7-2462:26)
[Warning][Deadcode][CWE-571] condition 'person == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1194:21-1194:32)
[Warning][Deadcode][CWE-570] condition 'persons_3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2718:9-2718:18)
[Warning][Deadcode][CWE-571] condition 'floorID == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1827:9-1827:21)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2466:9-2466:12)
[Warning][Deadcode][CWE-570] condition 'persons_4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2732:9-2732:18)
[Warning][Deadcode][CWE-571] condition 'currentHeading == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2478:7-2478:26)
[Warning][Deadcode][CWE-571] condition 'dir == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2057:7-2057:15)
[Warning][Deadcode][CWE-570] condition 'floor == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1401:13-1401:23)
[Warning][Deadcode][CWE-570] condition 'persons_5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2746:9-2746:18)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2061:9-2061:12)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2067:9-2067:27)
[Warning][Deadcode][CWE-571] condition 'doorState == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2765:9-2765:23)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2502:9-2502:12)
[Warning][Deadcode][CWE-571] condition 'floorID == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1870:7-1870:19)
[Warning][Deadcode][CWE-571] condition 'tmp___8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2773:9-2773:16)
[Warning][Deadcode][CWE-570] condition 'currentFloorID < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2083:11-2083:29)
[Warning][Deadcode][CWE-571] condition 'floor == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1428:15-1428:25)
[Warning][Deadcode][CWE-571] condition 'person == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1429:17-1429:28)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2522:7-2522:10)
[Warning][Deadcode][CWE-570] condition 'floorID == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1057:11-1057:23)
[Warning][Deadcode][CWE-571] condition 'currentFloorID < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2096:13-2096:31)
[Warning][Deadcode][CWE-571] condition 'respectFloorCalls' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2097:15-2097:32)
[Warning][Deadcode][CWE-570] condition 'floorID == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1061:13-1061:25)
[Warning][Deadcode][CWE-571] condition 'tmp___3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:2101:17-2101:24)
[Warning][Deadcode][CWE-571] condition 'floorID == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/elevator_spec14_product20.cil.c:1065:15-1065:27)
[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
