./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.4.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.4.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.4.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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:695:2-695:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:849:2-849: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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:555-555)
  on line 561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:561-561)
  on line 569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:569-569)
  on line 601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:601-601)
  on line 654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:654-654)
  on line 664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:664-664)
  on line 682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:682-682)
  on line 691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:691-691)
  on line 724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:724-724)
  on line 735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:735-735)
  on line 757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:757-757)
  on line 768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:768-768)
  on line 811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:811-811)
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:822-822)
  on line 838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:838-838)
  on line 856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:856-856)
  on line 864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:864-864)
  on line 868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:868-868)
  on line 870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:870-870)
  on line 888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:888-888)
  on line 896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:896-896)
  on line 900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:900-900)
  on line 902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:902-902)
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:920-920)
  on line 928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:928-928)
  on line 932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:932-932)
  on line 934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:934-934)
  on line 971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:971-971)
  on line 1000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1000-1000)
  on line 1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1006-1006)
  on line 1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1026-1026)
  on line 1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1032-1032)
  on line 1064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1064-1064)
  on line 1102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1102-1102)
  on line 1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1105-1105)
  on line 1107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1107-1107)
  on line 1109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1109-1109)
  on line 1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1111-1111)
  on line 1113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1113-1113)
  on line 1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1116-1116)
  on line 1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1118-1118)
  on line 1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1120-1120)
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1122-1122)
  on line 1130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1130-1130)
  on line 1147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1147-1147)
  on line 1170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1170-1170)
  on line 1208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1208-1208)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1211-1211)
  on line 1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1213-1213)
  on line 1215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1215-1215)
  on line 1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1217-1217)
  on line 1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1219-1219)
  on line 1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1222-1222)
  on line 1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1224-1224)
  on line 1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1226-1226)
  on line 1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1228-1228)
  on line 1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1236-1236)
  on line 1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1253-1253)
  on line 1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1276-1276)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1314-1314)
  on line 1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1317-1317)
  on line 1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1319-1319)
  on line 1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1321-1321)
  on line 1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1323-1323)
  on line 1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1325-1325)
  on line 1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1328-1328)
  on line 1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1330-1330)
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1332-1332)
  on line 1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1334-1334)
  on line 1342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1342-1342)
  on line 1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1359-1359)
  on line 1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1398-1398)
  on line 1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1404-1404)
  on line 1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1418-1418)
  on line 1451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1451-1451)
  on line 1477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1477-1477)
  on line 1489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1489-1489)
  on line 1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1515-1515)
  on line 1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1527-1527)
  on line 1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1553-1553)
  on line 1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1561-1561)
  on line 1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1566-1566)
  on line 1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1572-1572)
  on line 1577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1577-1577)
  on line 1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1583-1583)
  on line 1588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1588-1588)
  on line 1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1593-1593)
  on line 1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1598-1598)
  on line 1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1605-1605)
  on line 1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1622-1622)
  on line 1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1638-1638)
  on line 1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1646-1646)
  on line 1663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1663-1663)
  on line 1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1679-1679)
  on line 1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1691-1691)
  on line 1696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1696-1696)
  on line 1702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1702-1702)
  on line 1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1707-1707)
  on line 1713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1713-1713)
  on line 1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1718-1718)
  on line 1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1723-1723)
  on line 1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1728-1728)
  on line 1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1756-1756)
  on line 1784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1812-1812)
  on line 1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1820-1820)
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1825-1825)
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1831-1831)
  on line 1836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1836-1836)
  on line 1842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1842-1842)
  on line 1847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1847-1847)
  on line 1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1852-1852)
  on line 1857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1857-1857)
  on line 1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1864-1864)
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1881-1881)
  on line 1897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1897-1897)
  on line 1905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1905-1905)
  on line 1922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1922-1922)
  on line 1938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1938-1938)
  on line 1946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1946-1946)
  on line 1963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1963-1963)
  on line 1979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1979-1979)
  on line 1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1986-1986)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 521
  dead: 140 (2 in uncalled functions)
  total lines: 661
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:926:7-926: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:589:6-589: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1206:7-1206: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:591:6-591:22)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:391:6-391: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:398:6-398: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:930:7-930:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:400:6-400:15)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:778:7-778: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:599:6-599: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:605:7-605: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:610:6-610: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:612:6-612:22)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:621:6-621: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:623:6-623: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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:230:6-230: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:960:7-960:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:431:6-431: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:963:7-963: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:807:7-807:20)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:433:6-433:15)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:809:7-809: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:966:7-966: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:969:7-969: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:817:7-817: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:820:7-820:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1312:7-1312:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:246:6-246: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:644:9-644: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:646:8-646:36)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:252:7-252: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:648:8-648: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:650:8-650: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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:652:7-652:20)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:259:6-259:22)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:658:9-658: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:660:7-660: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:662:7-662: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:456:7-456: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:668:9-668: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:670:7-670:19)
[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.4.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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:464:6-464: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:466:6-466:15)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:680:6-680: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:278:6-278: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:687:6-687: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:854:7-854: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:689:6-689:15)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:284:7-284: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:289:6-289: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:291:6-291:22)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:862:7-862: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:300:6-300: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:302:6-302: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:866:7-866:20)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:489:7-489: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:310:6-310: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:712:7-712: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:316:7-316: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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:323:6-323: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:720:6-720: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:722:6-722: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1100:7-1100: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:886:7-886:29)
[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.4.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.4.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.4.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.4.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.4.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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:518:7-518:20)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:733:7-733:29)
[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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:526:7-526: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:894:7-894:29)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:534:9-534: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:536:7-536: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:898:7-898:20)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:745:7-745:20)
[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.4.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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:355:9-355:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:357:8-357: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:359:8-359:36)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:753:6-753: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:361:8-361:36)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:755:6-755:15)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:363:7-363: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:567:6-567: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:369:9-369: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:573:7-573: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.4.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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:373:7-373:20)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:918:7-918: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:578:6-578: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:580:6-580:22)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:379:9-379: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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:381:7-381:19)
[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.4.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:766:7-766:29)
[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
