./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/Problem19_label11.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/Problem19_label11.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/eca-rers2012/Problem19_label11.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/eca-rers2012/Problem19_label11.c:9794:5-9803:5 with factor 6
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid

[Info] runtime: 00:00:11.560
[Info] vars: 115232, evals: 103256

[Info] |called|=25

Memory statistics: total=23643.75MB, max=265.50MB, minor=23626.00MB, major=338.23MB, promoted=320.48MB
    minor collections=11274  major collections=16 compactions=0


[Info] runtime: 00:00:21.640
[Info] vars: 181950, evals: 169941

[Info] |called|=18

Memory statistics: total=49000.41MB, max=351.13MB, minor=48973.17MB, major=537.09MB, promoted=509.85MB
    minor collections=23363  major collections=18 compactions=0


[Info] runtime: 00:00:31.691
[Info] vars: 227350, evals: 215329

[Info] |called|=30

Memory statistics: total=74117.14MB, max=464.37MB, minor=74089.01MB, major=683.85MB, promoted=655.73MB
    minor collections=35340  major collections=19 compactions=0


[Info] runtime: 00:00:41.750
[Info] vars: 232693, evals: 220665

[Info] |called|=0

Memory statistics: total=97923.18MB, max=534.03MB, minor=97887.66MB, major=892.30MB, promoted=856.78MB
    minor collections=46690  major collections=20 compactions=0

[Warning][Deadcode] Function 'calculate_output' has dead code:
  on lines 229..232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:229-232)
  on lines 246..249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:246-249)
  on lines 325..328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:325-328)
  on lines 338..340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:338-340)
  on lines 350..354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:350-354)
  on lines 378..382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:378-382)
  on lines 601..604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:601-604)
  on lines 631..634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:631-634)
  on lines 722..723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:722-723)
  on lines 803..807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:803-807)
  on lines 824..826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:824-826)
  on lines 851..854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:851-854)
  on lines 1071..1075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1071-1075)
  on lines 1137..1141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1137-1141)
  on lines 1165..1168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1165-1168)
  on lines 1205..1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1205-1209)
  on lines 1255..1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1255-1258)
  on lines 1275..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1275-1276)
  on lines 1306..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1306-1308)
  on lines 1331..1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1331-1333)
  on lines 1371..1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1371-1374)
  on lines 1550..1554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1550-1554)
  on lines 1570..1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1570-1573)
  on lines 1592..1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1592-1596)
  on lines 1608..1609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1608-1609)
  on lines 1715..1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1715-1718)
  on lines 1742..1745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1742-1745)
[Warning][Deadcode] Function 'calculate_output2' has dead code:
  on lines 1987..1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1987-1989)
  on lines 2034..2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2034-2037)
  on lines 2165..2167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2165-2167)
  on lines 2217..2220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2217-2220)
  on lines 2413..2416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2413-2416)
  on lines 2519..2521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2519-2521)
  on lines 2550..2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2550-2552)
  on lines 2615..2618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2615-2618)
  on lines 2641..2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2641-2643)
  on line 2727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2727-2727)
  on lines 2871..2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2871-2874)
  on lines 2890..2893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2890-2893)
  on lines 2924..2926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2924-2926)
  on lines 2981..2983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2981-2983)
  on lines 3009..3011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3009-3011)
  on lines 3244..3247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3244-3247)
  on lines 3264..3267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3264-3267)
  on lines 3334..3337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3334-3337)
[Warning][Deadcode] Function 'calculate_output3' has dead code:
  on lines 3488..3491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3488-3491)
  on lines 3515..3519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3515-3519)
  on lines 3550..3553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3550-3553)
  on lines 3570..3572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3570-3572)
  on lines 3679..3683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3679-3683)
  on lines 3750..3752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3750-3752)
  on lines 3851..3853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3851-3853)
  on lines 3891..3893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3891-3893)
  on lines 3928..3931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3928-3931)
  on lines 3980..3983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3980-3983)
  on lines 4020..4023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4020-4023)
  on lines 4147..4149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4147-4149)
  on lines 4237..4240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4237-4240)
  on lines 4262..4266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4262-4266)
  on lines 4319..4322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4319-4322)
  on lines 4373..4374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4373-4374)
  on lines 4397..4400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4397-4400)
  on lines 4416..4420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4416-4420)
  on lines 4477..4480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4477-4480)
  on lines 4509..4511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4509-4511)
  on lines 4567..4569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4567-4569)
  on lines 4599..4602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4599-4602)
  on lines 4613..4616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4613-4616)
  on lines 4644..4647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4644-4647)
  on lines 4672..4675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4672-4675)
  on lines 4713..4715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4713-4715)
  on lines 4808..4810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4808-4810)
  on lines 4886..4890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4886-4890)
  on lines 4948..4950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4948-4950)
  on lines 4996..4997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4996-4997)
  on lines 5059..5062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5059-5062)
[Warning][Deadcode] Function 'calculate_output4' has dead code:
  on line 5148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5148-5148)
  on lines 5176..5179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5176-5179)
  on lines 5200..5203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5200-5203)
  on lines 5214..5217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5214-5217)
  on lines 5301..5304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5301-5304)
  on lines 5410..5413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5410-5413)
  on lines 5476..5478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5476-5478)
  on lines 5501..5503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5501-5503)
  on line 5602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5602-5602)
  on lines 5682..5685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5682-5685)
  on lines 5782..5784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5782-5784)
  on lines 5825..5828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5825-5828)
  on lines 5851..5853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5851-5853)
  on lines 5903..5906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5903-5906)
  on lines 5945..5948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5945-5948)
  on lines 6041..6044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6041-6044)
  on lines 6128..6131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6128-6131)
  on lines 6183..6184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6183-6184)
  on lines 6275..6279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6275-6279)
  on lines 6372..6375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6372-6375)
  on lines 6393..6396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6393-6396)
  on lines 6461..6464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6461-6464)
  on lines 6496..6498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6496-6498)
  on lines 6529..6531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6529-6531)
  on lines 6667..6669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6667-6669)
[Warning][Deadcode] Function 'calculate_output5' has dead code:
  on lines 6725..6728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6725-6728)
  on lines 6754..6757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6754-6757)
  on lines 6793..6794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6793-6794)
  on lines 6863..6867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6863-6867)
  on lines 6878..6881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6878-6881)
  on lines 6912..6915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6912-6915)
  on lines 6951..6954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6951-6954)
  on lines 7106..7109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7106-7109)
  on lines 7156..7159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7156-7159)
  on lines 7262..7264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7262-7264)
  on lines 7343..7344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7343-7344)
  on lines 7398..7402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7398-7402)
  on lines 7519..7521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7519-7521)
  on lines 7532..7535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7532-7535)
  on lines 7571..7574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7571-7574)
  on lines 7606..7609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7606-7609)
  on lines 7635..7639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7635-7639)
  on lines 7763..7767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7763-7767)
  on lines 7792..7794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7792-7794)
  on lines 7938..7941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7938-7941)
  on lines 8012..8015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8012-8015)
  on lines 8032..8035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8032-8035)
  on lines 8082..8084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8082-8084)
  on lines 8165..8168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8165-8168)
  on lines 8316..8319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8316-8319)
[Warning][Deadcode] Function 'calculate_output6' has dead code:
  on lines 8412..8415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8412-8415)
  on lines 8426..8428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8426-8428)
  on lines 8460..8463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8460-8463)
  on lines 8559..8563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8559-8563)
  on lines 8612..8613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8612-8613)
  on lines 8624..8626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8624-8626)
  on lines 8675..8679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8675-8679)
  on lines 8710..8714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8710-8714)
  on lines 8820..8823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8820-8823)
  on lines 8828..8830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8828-8830)
  on lines 9067..9070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9067-9070)
  on lines 9102..9105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9102-9105)
  on lines 9123..9125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9123-9125)
  on lines 9215..9219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9215-9219)
  on lines 9229..9232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9229-9232)
  on lines 9243..9245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9243-9245)
  on lines 9281..9285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9281-9285)
  on lines 9349..9351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9349-9351)
[Warning][Deadcode] Function 'main' has dead code:
  on line 9804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9804-9804)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 7484
  dead: 534
  total lines: 8018
[Warning][Deadcode][CWE-570] condition 'a8 == 7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2870:11-2870:17)
[Warning][Deadcode][CWE-570] condition 'a9 == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:228:11-228:17)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2889:11-2889:21)
[Warning][Deadcode][CWE-570] condition '-178 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:245:14-245:44)
[Warning][Deadcode][CWE-570] condition 'a27 <= -78' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2923:11-2923:23)
[Warning][Deadcode][CWE-570] condition '13 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5600:14-5600:41)
[Warning][Deadcode][CWE-570] condition '-78 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2980:14-2980:42)
[Warning][Deadcode][CWE-570] condition 'a9 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:324:11-324:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:337:11-337:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3008:11-3008:17)
[Warning][Deadcode][CWE-570] condition 'a14 <= -148' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:349:11-349:24)
[Warning][Deadcode][CWE-570] condition 'a9 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8315:11-8315:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5681:11-5681:17)
[Warning][Deadcode][CWE-570] condition '182 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:377:11-377:21)
[Warning][Deadcode][CWE-570] condition '13 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8411:14-8411:41)
[Warning][Deadcode][CWE-570] condition 'a21 <= -178' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8425:11-8425:24)
[Warning][Deadcode][CWE-571] condition '-78 < a27' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5781:14-5781:42)
[Warning][Deadcode][CWE-570] condition '100 >= a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5781:14-5781:42)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8453:11-8453:23)
[Warning][Deadcode][CWE-570] condition 'a9 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5824:11-5824:17)
[Warning][Deadcode][CWE-570] condition 'a9 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5850:11-5850:17)
[Warning][Deadcode][CWE-571] condition 'a8 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5896:11-5896:17)
[Warning][Deadcode][CWE-570] condition '182 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8558:11-8558:21)
[Warning][Deadcode][CWE-570] condition '100 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3243:14-3243:42)
[Warning][Deadcode][CWE-570] condition '5 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:600:11-600:19)
[Warning][Deadcode][CWE-570] condition '-148 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3263:14-3263:42)
[Warning][Deadcode][CWE-570] condition 'a9 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5944:11-5944:17)
[Warning][Deadcode][CWE-571] condition '-148 < a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8603:14-8603:42)
[Warning][Deadcode][CWE-571] condition '13 >= a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8603:14-8603:42)
[Warning][Deadcode][CWE-570] condition 'a9 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:630:11-630:17)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8617:11-8617:23)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8668:11-8668:23)
[Warning][Deadcode][CWE-570] condition 'a9 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3333:11-3333:17)
[Warning][Deadcode][CWE-570] condition 'a9 == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6040:11-6040:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:720:11-720:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8709:11-8709:17)
[Warning][Deadcode][CWE-570] condition '-178 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6127:14-6127:44)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:797:11-797:23)
[Warning][Deadcode][CWE-571] condition 'a8 == 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8814:11-8814:17)
[Warning][Deadcode][CWE-570] condition 'a9 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:823:11-823:17)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8827:11-8827:21)
[Warning][Deadcode][CWE-570] condition 'a8 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3487:11-3487:17)
[Warning][Deadcode][CWE-570] condition '13 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:850:14-850:41)
[Warning][Deadcode][CWE-570] condition 'a8 == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6182:11-6182:17)
[Warning][Deadcode][CWE-570] condition 'a14 <= -148' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3514:11-3514:24)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3549:11-3549:21)
[Warning][Deadcode][CWE-570] condition '182 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3569:11-3569:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= -178' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6269:11-6269:24)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3672:11-3672:23)
[Warning][Deadcode][CWE-570] condition 'a14 <= -148' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6371:11-6371:24)
[Warning][Deadcode][CWE-570] condition 'a9 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6392:11-6392:17)
[Warning][Deadcode][CWE-571] condition 'a8 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1066:11-1066:17)
[Warning][Deadcode][CWE-571] condition '-148 < a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9059:14-9059:42)
[Warning][Deadcode][CWE-571] condition '13 >= a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9059:14-9059:42)
[Warning][Deadcode][CWE-570] condition 'a8 == 7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3749:11-3749:17)
[Warning][Deadcode][CWE-571] condition '5 >= a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9088:14-9088:41)
[Warning][Deadcode][CWE-571] condition '-178 < a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9101:14-9101:44)
[Warning][Deadcode][CWE-570] condition '-144 >= a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9101:14-9101:44)
[Warning][Deadcode][CWE-570] condition '-148 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6460:14-6460:42)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9122:11-9122:21)
[Warning][Deadcode][CWE-570] condition '13 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1136:14-1136:41)
[Warning][Deadcode][CWE-570] condition 'a8 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1164:11-1164:17)
[Warning][Deadcode][CWE-570] condition '13 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6495:14-6495:41)
[Warning][Deadcode][CWE-570] condition '100 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6528:14-6528:42)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3844:11-3844:23)
[Warning][Deadcode][CWE-570] condition 'a9 == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1204:11-1204:17)
[Warning][Deadcode][CWE-571] condition '-148 < a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9210:14-9210:42)
[Warning][Deadcode][CWE-571] condition '13 >= a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9210:14-9210:42)
[Warning][Deadcode][CWE-571] condition '182 < a27' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9223:11-9223:21)
[Warning][Deadcode][CWE-570] condition '100 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3890:14-3890:42)
[Warning][Deadcode][CWE-570] condition 'a9 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9242:11-9242:17)
[Warning][Deadcode][CWE-571] condition '-144 < a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1254:14-1254:41)
[Warning][Deadcode][CWE-570] condition '5 >= a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1254:14-1254:41)
[Warning][Deadcode][CWE-571] condition 'a14 <= -148' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1268:11-1268:24)
[Warning][Deadcode][CWE-571] condition 'a8 == 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3920:11-3920:17)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9280:11-9280:21)
[Warning][Deadcode][CWE-570] condition '-78 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1305:14-1305:42)
[Warning][Deadcode][CWE-571] condition 'a8 == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1323:11-1323:17)
[Warning][Deadcode][CWE-570] condition '182 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:3979:11-3979:21)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9343:11-9343:23)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6666:11-6666:21)
[Warning][Deadcode][CWE-570] condition 'a9 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1370:11-1370:17)
[Warning][Deadcode][CWE-570] condition '-148 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4019:14-4019:42)
[Warning][Deadcode][CWE-571] condition '-144 < a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6724:14-6724:41)
[Warning][Deadcode][CWE-570] condition '5 >= a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6724:14-6724:41)
[Warning][Deadcode][CWE-571] condition '-78 < a27' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6753:14-6753:42)
[Warning][Deadcode][CWE-570] condition '100 >= a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6753:14-6753:42)
[Warning][Deadcode][CWE-570] condition '13 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6792:14-6792:41)
[Warning][Deadcode][CWE-570] condition '5 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4146:11-4146:19)
[Warning][Deadcode][CWE-570] condition '182 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6862:11-6862:21)
[Warning][Deadcode][CWE-570] condition '100 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6877:14-6877:42)
[Warning][Deadcode][CWE-570] condition 'a8 == 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1549:11-1549:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1569:11-1569:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1591:11-1591:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6911:11-6911:17)
[Warning][Deadcode][CWE-570] condition 'a9 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1607:11-1607:17)
[Warning][Deadcode][CWE-570] condition '-144 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4236:14-4236:41)
[Warning][Deadcode][CWE-571] condition '5 < a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:6944:11-6944:19)
[Warning][Deadcode][CWE-570] condition '-178 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4261:14-4261:44)
[Warning][Deadcode][CWE-570] condition 'a21 <= -178' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4318:11-4318:24)
[Warning][Deadcode][CWE-570] condition 'a8 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1714:11-1714:17)
[Warning][Deadcode][CWE-571] condition 'a21 <= -178' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1735:11-1735:24)
[Warning][Deadcode][CWE-570] condition 'a14 <= -148' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4372:11-4372:24)
[Warning][Deadcode][CWE-570] condition '182 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4396:11-4396:21)
[Warning][Deadcode][CWE-570] condition 'a8 == 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4415:11-4415:17)
[Warning][Deadcode][CWE-570] condition '-148 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7105:14-7105:42)
[Warning][Deadcode][CWE-570] condition 'a21 <= -178' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4476:11-4476:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9794:11-9794:12)
[Warning][Deadcode][CWE-570] condition '-148 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7155:14-7155:42)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9794:11-9794:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9794:11-9794:12)
[Warning][Deadcode][CWE-570] condition '13 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4508:14-4508:41)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9794:11-9794:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9794:11-9794:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9794:11-9794:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:9794:11-9794:12)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4560:11-4560:23)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4592:11-4592:23)
[Warning][Deadcode][CWE-570] condition '5 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4612:11-4612:19)
[Warning][Deadcode][CWE-571] condition '100 < a27' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7261:14-7261:42)
[Warning][Deadcode][CWE-570] condition '182 >= a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7261:14-7261:42)
[Warning][Deadcode][CWE-571] condition 'a14 <= -148' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4637:11-4637:24)
[Warning][Deadcode][CWE-570] condition 'a9 == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:1986:11-1986:17)
[Warning][Deadcode][CWE-570] condition '5 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4671:11-4671:19)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2027:11-2027:23)
[Warning][Deadcode][CWE-571] condition '-178 < a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7336:14-7336:44)
[Warning][Deadcode][CWE-571] condition '-144 >= a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7336:14-7336:44)
[Warning][Deadcode][CWE-570] condition 'a27 <= -78' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4712:11-4712:23)
[Warning][Deadcode][CWE-570] condition '13 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7397:14-7397:41)
[Warning][Deadcode][CWE-570] condition 'a9 == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4807:11-4807:17)
[Warning][Deadcode][CWE-570] condition 'a14 <= -148' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2164:11-2164:24)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2216:11-2216:21)
[Warning][Deadcode][CWE-570] condition '-78 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7518:14-7518:42)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4885:11-4885:21)
[Warning][Deadcode][CWE-570] condition 'a9 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7531:11-7531:17)
[Warning][Deadcode][CWE-571] condition '5 >= a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2252:14-2252:41)
[Warning][Deadcode][CWE-571] condition '-148 < a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7565:14-7565:42)
[Warning][Deadcode][CWE-571] condition '13 >= a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7565:14-7565:42)
[Warning][Deadcode][CWE-570] condition '182 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4947:11-4947:21)
[Warning][Deadcode][CWE-570] condition 'a8 == 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7605:11-7605:17)
[Warning][Deadcode][CWE-570] condition 'a14 <= -148' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7634:11-7634:24)
[Warning][Deadcode][CWE-571] condition 'a21 <= -178' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:4990:11-4990:24)
[Warning][Deadcode][CWE-570] condition 'a9 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5058:11-5058:17)
[Warning][Deadcode][CWE-570] condition '-144 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2412:14-2412:41)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7756:11-7756:23)
[Warning][Deadcode][CWE-570] condition '5 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7791:11-7791:19)
[Warning][Deadcode][CWE-570] condition 'a21 <= -178' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5147:11-5147:24)
[Warning][Deadcode][CWE-571] condition 'a14 <= -148' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2512:11-2512:24)
[Warning][Deadcode][CWE-570] condition 'a21 <= -178' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5175:11-5175:24)
[Warning][Deadcode][CWE-571] condition '-178 < a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5199:14-5199:44)
[Warning][Deadcode][CWE-570] condition '-144 >= a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5199:14-5199:44)
[Warning][Deadcode][CWE-570] condition 'a21 <= -178' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5213:11-5213:24)
[Warning][Deadcode][CWE-570] condition '-78 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2549:14-2549:42)
[Warning][Deadcode][CWE-570] condition 'a8 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2614:11-2614:17)
[Warning][Deadcode][CWE-571] condition '-144 < a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5294:14-5294:41)
[Warning][Deadcode][CWE-571] condition '5 >= a21' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5294:14-5294:41)
[Warning][Deadcode][CWE-570] condition 'a8 == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:7937:11-7937:17)
[Warning][Deadcode][CWE-570] condition 'a21 <= -178' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2640:11-2640:24)
[Warning][Deadcode][CWE-571] condition '-78 < a27' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8011:14-8011:42)
[Warning][Deadcode][CWE-570] condition '100 >= a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8011:14-8011:42)
[Warning][Deadcode][CWE-570] condition 'a8 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8031:11-8031:17)
[Warning][Deadcode][CWE-570] condition '-144 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:2725:14-2725:41)
[Warning][Deadcode][CWE-570] condition 'a9 == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5409:11-5409:17)
[Warning][Deadcode][CWE-571] condition 'a8 == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8076:11-8076:17)
[Warning][Deadcode][CWE-570] condition 'a8 == 7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5475:11-5475:17)
[Warning][Deadcode][CWE-571] condition 'a27 <= -78' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:5495:11-5495:23)
[Warning][Deadcode][CWE-570] condition '100 < a27' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem19_label11.c:8164:14-8164:42)

[Info] runtime: 00:00:51.822
[Info] vars: 232693, evals: 220665

[Info] |called|=0

Memory statistics: total=120614.16MB, max=614.13MB, minor=120572.24MB, major=1075.47MB, promoted=1033.55MB
    minor collections=57510  major collections=21 compactions=0

[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
