./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_floodmax.3.1.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.1.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, assert__arg, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:394:2-394:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:701:2-701:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:855:2-855: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:236-236)
  on line 268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:268-268)
  on line 300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:300-300)
  on line 353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:353-353)
  on line 363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:363-363)
  on line 381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:381-381)
  on line 390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:390-390)
  on line 413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:413-413)
  on line 423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:423-423)
  on line 446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:446-446)
  on line 456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:456-456)
  on line 479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:479-479)
  on line 508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:508-508)
  on line 518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:518-518)
  on line 536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:536-536)
  on line 543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:543-543)
  on line 575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:575-575)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:607-607)
  on line 660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:660-660)
  on line 670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:670-670)
  on line 688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:688-688)
  on line 697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:697-697)
  on line 730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:730-730)
  on line 763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:763-763)
  on line 817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:817-817)
  on line 828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:828-828)
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:844-844)
  on line 862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:862-862)
  on line 870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:870-870)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:874-874)
  on line 876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:876-876)
  on line 894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:894-894)
  on line 902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:902-902)
  on line 906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:906-906)
  on line 908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:908-908)
  on line 926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:926-926)
  on line 934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:934-934)
  on line 938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:938-938)
  on line 940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:940-940)
  on line 977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:977-977)
  on line 1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1006-1006)
  on line 1012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1012-1012)
  on line 1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1032-1032)
  on line 1038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1038-1038)
  on line 1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1070-1070)
  on line 1108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1108-1108)
  on line 1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1113-1113)
  on line 1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1115-1115)
  on line 1117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1117-1117)
  on line 1119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1119-1119)
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1122-1122)
  on line 1124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1124-1124)
  on line 1126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1126-1126)
  on line 1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1128-1128)
  on line 1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1136-1136)
  on line 1153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1153-1153)
  on line 1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1176-1176)
  on line 1214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1214-1214)
  on line 1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1219-1219)
  on line 1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1221-1221)
  on line 1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1223-1223)
  on line 1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1225-1225)
  on line 1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1228-1228)
  on line 1230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1230-1230)
  on line 1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1232-1232)
  on line 1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1234-1234)
  on line 1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1242-1242)
  on line 1259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1259-1259)
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1282-1282)
  on line 1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1320-1320)
  on line 1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1325-1325)
  on line 1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1327-1327)
  on line 1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1329-1329)
  on line 1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1331-1331)
  on line 1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1334-1334)
  on line 1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1336-1336)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1338-1338)
  on line 1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1340-1340)
  on line 1348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1348-1348)
  on line 1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1365-1365)
  on line 1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1404-1404)
  on line 1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1410-1410)
  on line 1424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1424-1424)
  on line 1457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1457-1457)
  on line 1483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1483-1483)
  on line 1495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1495-1495)
  on line 1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1521-1521)
  on line 1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1533-1533)
  on line 1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1559-1559)
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1567-1567)
  on line 1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1572-1572)
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1578-1578)
  on line 1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1583-1583)
  on line 1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1589-1589)
  on line 1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1594-1594)
  on line 1599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1599-1599)
  on line 1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1604-1604)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1611-1611)
  on line 1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1628-1628)
  on line 1644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1644-1644)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1652-1652)
  on line 1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1669-1669)
  on line 1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1685-1685)
  on line 1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1693-1693)
  on line 1710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1710-1710)
  on line 1726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1726-1726)
  on line 1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1735-1735)
  on line 1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1740-1740)
  on line 1746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1746-1746)
  on line 1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1751-1751)
  on line 1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1757-1757)
  on line 1762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1762-1762)
  on line 1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1767-1767)
  on line 1772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1772-1772)
  on line 1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1800-1800)
  on line 1828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1828-1828)
  on line 1856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1856-1856)
  on line 1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1864-1864)
  on line 1869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1869-1869)
  on line 1875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1875-1875)
  on line 1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1880-1880)
  on line 1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1886-1886)
  on line 1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1891-1891)
  on line 1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1896-1896)
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1901-1901)
  on line 1908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1908-1908)
  on line 1925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1925-1925)
  on line 1941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1941-1941)
  on line 1949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1949-1949)
  on line 1966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1966-1966)
  on line 1982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1982-1982)
  on line 1990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1990-1990)
  on line 2007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:2007-2007)
  on line 2023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:2023-2023)
  on line 2030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:2030-2030)
[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 )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:573:6-573: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:386:6-386: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:579:7-579: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:388:6-388: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:924:7-924: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:584:6-584: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:586:6-586: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:932:7-932: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:595:6-595: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1212:7-1212: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:597:6-597: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:936:7-936: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:784:7-784: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:605:6-605: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:611:7-611: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:411:7-411: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:218:6-218: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:616:6-616: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:618:6-618: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:419:6-419: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:421:6-421: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:627:6-627: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:629:6-629: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:234:6-234: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:966:7-966: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:240:7-240: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.1.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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:813:7-813: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:245:6-245: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:815:7-815: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:247:6-247: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:972:7-972: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:975:7-975: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:823:7-823: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:826:7-826: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:444:7-444: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:256:6-256: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:258:6-258: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:452:6-452: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1318:7-1318: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:650:9-650: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:454:6-454: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:652:8-652: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:654:8-654: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:656:8-656: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:658:7-658: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:266:6-266: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:664:9-664: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:666:7-666: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:272:7-272: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:668:7-668: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:277:6-277: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:674:9-674: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:279:6-279: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:676:7-676: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:288:6-288: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:686:6-686: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:290:6-290: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:693:6-693: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:477:7-477: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:860:7-860: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:695:6-695: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:298:6-298: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:304:7-304: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:868:7-868: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:309:6-309: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:311:6-311: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:872:7-872: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:498:9-498: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:500:8-500: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:320:6-320: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:502:8-502: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:322:6-322: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:504:8-504: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:506:7-506: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:718:7-718: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:512:9-512: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:514:7-514: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:516:7-516: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:522:9-522: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:726:6-726: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:524:7-524: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:728:6-728: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1106:7-1106: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:892:7-892: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:534:6-534: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:541:6-541: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:343:9-343: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:547:7-547: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:345:8-345: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:900:7-900: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:347:8-347: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:552:6-552: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:349:8-349: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:554:6-554: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:351:7-351: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:904:7-904: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:357:9-357: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:359:7-359: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:361:7-361: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:367:9-367: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:751:7-751: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:563:6-563: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:369:7-369: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:565:6-565: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:759:6-759: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:761:6-761: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.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:379:6-379:22)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
