./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/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.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/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.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/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.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 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] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] nomsg, r1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, init__r121, init__r131, init__r211, init__r231, init__r311, init__r321, main__i2, init__r122, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:406:2-406:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:713:2-713:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:867:2-867:13)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:248-248)
  on line 280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:280-280)
  on line 312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:312-312)
  on line 365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:365-365)
  on line 375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:375-375)
  on line 393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:393-393)
  on line 402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:402-402)
  on line 425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:425-425)
  on line 435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:435-435)
  on line 458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:458-458)
  on line 468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:468-468)
  on line 491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:491-491)
  on line 520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:520-520)
  on line 530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:530-530)
  on line 548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:548-548)
  on line 555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:555-555)
  on line 587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:587-587)
  on line 619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:619-619)
  on line 672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:672-672)
  on line 682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:682-682)
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:700-700)
  on line 709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:709-709)
  on line 742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:742-742)
  on line 775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:775-775)
  on line 829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:829-829)
  on line 840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:840-840)
  on line 856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:856-856)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:874-874)
  on line 882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:882-882)
  on line 886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:886-886)
  on line 888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:888-888)
  on line 906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:906-906)
  on line 914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:914-914)
  on line 918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:918-918)
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:920-920)
  on line 938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:938-938)
  on line 946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:946-946)
  on line 950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:950-950)
  on line 952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:952-952)
  on line 989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:989-989)
  on line 1018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1018-1018)
  on line 1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1024-1024)
  on line 1044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1044-1044)
  on line 1050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1050-1050)
  on line 1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1082-1082)
  on line 1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1120-1120)
  on line 1123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1123-1123)
  on line 1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1125-1125)
  on line 1127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1127-1127)
  on line 1129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1129-1129)
  on line 1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1131-1131)
  on line 1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1134-1134)
  on line 1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1136-1136)
  on line 1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1138-1138)
  on line 1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1140-1140)
  on line 1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1148-1148)
  on line 1165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1165-1165)
  on line 1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1188-1188)
  on line 1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1226-1226)
  on line 1229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1229-1229)
  on line 1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1231-1231)
  on line 1233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1233-1233)
  on line 1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1235-1235)
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1237-1237)
  on line 1240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1240-1240)
  on line 1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1242-1242)
  on line 1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1244-1244)
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1246-1246)
  on line 1254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1254-1254)
  on line 1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1271-1271)
  on line 1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1294-1294)
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1332-1332)
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1335-1335)
  on line 1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1337-1337)
  on line 1339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1339-1339)
  on line 1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1341-1341)
  on line 1343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1343-1343)
  on line 1346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1346-1346)
  on line 1348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1348-1348)
  on line 1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1350-1350)
  on line 1352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1352-1352)
  on line 1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1360-1360)
  on line 1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1377-1377)
  on line 1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1416-1416)
  on line 1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1422-1422)
  on line 1436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1436-1436)
  on line 1469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1469-1469)
  on line 1495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1495-1495)
  on line 1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1507-1507)
  on line 1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1533-1533)
  on line 1545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1545-1545)
  on line 1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1571-1571)
  on line 1579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1579-1579)
  on line 1584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1584-1584)
  on line 1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1590-1590)
  on line 1595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1595-1595)
  on line 1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1601-1601)
  on line 1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1606-1606)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1611-1611)
  on line 1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1616-1616)
  on line 1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1623-1623)
  on line 1640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1640-1640)
  on line 1656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1656-1656)
  on line 1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1664-1664)
  on line 1681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1681-1681)
  on line 1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1697-1697)
  on line 1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1705-1705)
  on line 1722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1722-1722)
  on line 1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1738-1738)
  on line 1747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1747-1747)
  on line 1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1752-1752)
  on line 1758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1758-1758)
  on line 1763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1763-1763)
  on line 1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1769-1769)
  on line 1774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1774-1774)
  on line 1779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1779-1779)
  on line 1784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1784-1784)
  on line 1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1812-1812)
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1840-1840)
  on line 1868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1868-1868)
  on line 1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1876-1876)
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1881-1881)
  on line 1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1887-1887)
  on line 1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1892-1892)
  on line 1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1898-1898)
  on line 1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1903-1903)
  on line 1908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1908-1908)
  on line 1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1913-1913)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1920-1920)
  on line 1937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1937-1937)
  on line 1953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1953-1953)
  on line 1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1961-1961)
  on line 1978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1978-1978)
  on line 1994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1994-1994)
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:2002-2002)
  on line 2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:2019-2019)
  on line 2035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:2035-2035)
  on line 2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:2042-2042)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 533
  dead: 140 (2 in uncalled functions)
  total lines: 673
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:771:6-771:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:773:6-773:15)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:391:6-391:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:585:6-585:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:398:6-398:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:591:7-591:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:400:6-400:15)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:936:7-936:29)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:596:6-596:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:598:6-598:22)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:944:7-944:29)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:607:6-607:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1224:7-1224:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:609:6-609:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:948:7-948:20)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:796:7-796:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:617:6-617:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:623:7-623:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:423:7-423:20)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:230:6-230:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:628:6-628:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:630:6-630:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:431:6-431:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:433:6-433:15)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:639:6-639:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:641:6-641:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:246:6-246:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:978:7-978:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:252:7-252:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:981:7-981:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:825:7-825:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:257:6-257:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:827:7-827:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:259:6-259:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:984:7-984:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:987:7-987:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:835:7-835:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:838:7-838:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:456:7-456:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:268:6-268:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:270:6-270:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:464:6-464:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1330:7-1330:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:662:9-662:51)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:466:6-466:15)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:664:8-664:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:666:8-666:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:668:8-668:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:670:7-670:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:278:6-278:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:676:9-676:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:678:7-678:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:284:7-284:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:680:7-680:20)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:289:6-289:19)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:686:9-686:51)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:291:6-291:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:688:7-688:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:300:6-300:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:698:6-698:22)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:302:6-302:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:705:6-705:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:489:7-489:20)
[Warning][Deadcode][CWE-570] condition '(int )m1 > (int )max1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:872:7-872:29)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:707:6-707:15)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:310:6-310:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:316:7-316:19)
[Warning][Deadcode][CWE-570] condition '(int )m1 > (int )max1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:880:7-880:29)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:321:6-321:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:323:6-323:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:884:7-884:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:510:9-510:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:512:8-512:36)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:332:6-332:19)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:514:8-514:36)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:334:6-334:22)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:516:8-516:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:518:7-518:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:730:7-730:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:524:9-524:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:526:7-526:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:528:7-528:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:534:9-534:51)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:738:6-738:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:536:7-536:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:740:6-740:15)
[Warning][Deadcode][CWE-570] condition '(int )r3 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1118:7-1118:19)
[Warning][Deadcode][CWE-570] condition '(int )m2 > (int )max2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:904:7-904:29)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:546:6-546:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:553:6-553:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:355:9-355:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:559:7-559:19)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:357:8-357:36)
[Warning][Deadcode][CWE-570] condition '(int )m2 > (int )max2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:912:7-912:29)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:359:8-359:36)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:564:6-564:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:361:8-361:36)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:566:6-566:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:363:7-363:20)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:916:7-916:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:369:9-369:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:371:7-371:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:373:7-373:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:379:9-379:51)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:763:7-763:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:575:6-575:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:381:7-381:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:577:6-577:22)
[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
