./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.BOUNDED-6.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.BOUNDED-6.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.BOUNDED-6.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, main__i2, init__r121, init__r131, init__r211, init__r231, init__r311, init__r321, 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] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:395:2-395:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:692:2-692:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:836:2-836:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:864:2-864:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:892:2-892:28)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:239-239)
  on line 271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:271-271)
  on line 303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:303-303)
  on line 356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:356-356)
  on line 366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:366-366)
  on line 384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:384-384)
  on line 414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:414-414)
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:441-441)
  on line 468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:468-468)
  on line 497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:497-497)
  on line 507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:507-507)
  on line 525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:525-525)
  on line 536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:536-536)
  on line 568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:568-568)
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:600-600)
  on line 653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:653-653)
  on line 663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:663-663)
  on line 681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:681-681)
  on line 796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:796-796)
  on line 807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:807-807)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:825-825)
  on line 1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1105-1105)
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1122-1122)
  on line 1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1206-1206)
  on line 1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1223-1223)
  on line 1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1307-1307)
  on line 1324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1324-1324)
  on line 1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1369-1369)
  on line 1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1375-1375)
  on line 1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1389-1389)
  on line 1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1422-1422)
  on line 1447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1447-1447)
  on line 1459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1459-1459)
  on line 1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1484-1484)
  on line 1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1496-1496)
  on line 1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1521-1521)
  on line 1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1527-1527)
  on line 1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1534-1534)
  on line 1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1539-1539)
  on line 1545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1545-1545)
  on line 1550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1550-1550)
  on line 1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1556-1556)
  on line 1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1561-1561)
  on line 1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1566-1566)
  on line 1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1571-1571)
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1578-1578)
  on line 1595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1595-1595)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1611-1611)
  on line 1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1619-1619)
  on line 1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1636-1636)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1652-1652)
  on line 1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1660-1660)
  on line 1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1677-1677)
  on line 1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1693-1693)
  on line 1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1700-1700)
  on line 1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1707-1707)
  on line 1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1712-1712)
  on line 1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1718-1718)
  on line 1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1723-1723)
  on line 1729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1729-1729)
  on line 1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1734-1734)
  on line 1739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1739-1739)
  on line 1744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1744-1744)
  on line 1771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1771-1771)
  on line 1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1798-1798)
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1825-1825)
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1831-1831)
  on line 1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1838-1838)
  on line 1843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1843-1843)
  on line 1849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1849-1849)
  on line 1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1854-1854)
  on line 1860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1860-1860)
  on line 1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1865-1865)
  on line 1870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1870-1870)
  on line 1875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1875-1875)
  on line 1882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1882-1882)
  on line 1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1899-1899)
  on line 1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1915-1915)
  on line 1923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1923-1923)
  on line 1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1940-1940)
  on line 1956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1956-1956)
  on line 1964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1964-1964)
  on line 1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1981-1981)
  on line 1997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1997-1997)
  on line 2004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:2004-2004)
  on line 2009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:2009-2009)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 576
  dead: 88 (2 in uncalled functions)
  total lines: 664
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:382:6-382: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.BOUNDED-6.pals.c.v+nlh-reducer.c:744:6-744:19)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:566:6-566: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.BOUNDED-6.pals.c.v+nlh-reducer.c:572:7-572:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:390:6-390:18)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:393:6-393: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.BOUNDED-6.pals.c.v+nlh-reducer.c:577:6-577: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.BOUNDED-6.pals.c.v+nlh-reducer.c:579:6-579:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:1181:6-1181: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1183:6-1183:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:588:6-588: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.BOUNDED-6.pals.c.v+nlh-reducer.c:590:6-590:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:1192:6-1192: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.BOUNDED-6.pals.c.v+nlh-reducer.c:763:7-763:20)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:1194:6-1194:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:219:6-219:19)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:598:6-598: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.BOUNDED-6.pals.c.v+nlh-reducer.c:604:7-604: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.BOUNDED-6.pals.c.v+nlh-reducer.c:412:7-412:20)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:609:6-609: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.BOUNDED-6.pals.c.v+nlh-reducer.c:611:6-611: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.BOUNDED-6.pals.c.v+nlh-reducer.c:420:6-420: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.BOUNDED-6.pals.c.v+nlh-reducer.c:620:6-620: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.BOUNDED-6.pals.c.v+nlh-reducer.c:622:6-622:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:234:6-234:18)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:237:6-237: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.BOUNDED-6.pals.c.v+nlh-reducer.c:243:7-243: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.BOUNDED-6.pals.c.v+nlh-reducer.c:792:7-792: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.BOUNDED-6.pals.c.v+nlh-reducer.c:248:6-248: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.BOUNDED-6.pals.c.v+nlh-reducer.c:794:7-794: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.BOUNDED-6.pals.c.v+nlh-reducer.c:250:6-250: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.BOUNDED-6.pals.c.v+nlh-reducer.c:802:7-802: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.BOUNDED-6.pals.c.v+nlh-reducer.c:805:7-805: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.BOUNDED-6.pals.c.v+nlh-reducer.c:439:7-439: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1282:6-1282: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1284:6-1284:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:259:6-259: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.BOUNDED-6.pals.c.v+nlh-reducer.c:261:6-261: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.BOUNDED-6.pals.c.v+nlh-reducer.c:447:6-447: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.BOUNDED-6.pals.c.v+nlh-reducer.c:643:9-643: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.BOUNDED-6.pals.c.v+nlh-reducer.c:645:8-645: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.BOUNDED-6.pals.c.v+nlh-reducer.c:647:8-647: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1293:6-1293: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.BOUNDED-6.pals.c.v+nlh-reducer.c:649:8-649:36)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:1295:6-1295: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.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:269:6-269: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.BOUNDED-6.pals.c.v+nlh-reducer.c:651:7-651: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.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:275:7-275: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.BOUNDED-6.pals.c.v+nlh-reducer.c:657:9-657: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.BOUNDED-6.pals.c.v+nlh-reducer.c:659:7-659: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.BOUNDED-6.pals.c.v+nlh-reducer.c:280:6-280: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.BOUNDED-6.pals.c.v+nlh-reducer.c:661:7-661:20)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:282:6-282: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.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:667:9-667: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.BOUNDED-6.pals.c.v+nlh-reducer.c:669:7-669: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.BOUNDED-6.pals.c.v+nlh-reducer.c:291:6-291: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.BOUNDED-6.pals.c.v+nlh-reducer.c:466:7-466:20)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:293:6-293:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:679:6-679:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:687:6-687:18)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:301:6-301: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.BOUNDED-6.pals.c.v+nlh-reducer.c:690:6-690: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.BOUNDED-6.pals.c.v+nlh-reducer.c:307:7-307: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.BOUNDED-6.pals.c.v+nlh-reducer.c:312:6-312: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.BOUNDED-6.pals.c.v+nlh-reducer.c:314:6-314:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:487:9-487: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.BOUNDED-6.pals.c.v+nlh-reducer.c:489:8-489: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.BOUNDED-6.pals.c.v+nlh-reducer.c:491:8-491: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.BOUNDED-6.pals.c.v+nlh-reducer.c:493:8-493: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.BOUNDED-6.pals.c.v+nlh-reducer.c:323:6-323: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.BOUNDED-6.pals.c.v+nlh-reducer.c:495:7-495:20)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:325:6-325: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.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:501:9-501: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.BOUNDED-6.pals.c.v+nlh-reducer.c:503:7-503: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.BOUNDED-6.pals.c.v+nlh-reducer.c:505:7-505: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.BOUNDED-6.pals.c.v+nlh-reducer.c:511:9-511: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.BOUNDED-6.pals.c.v+nlh-reducer.c:709:7-709: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.BOUNDED-6.pals.c.v+nlh-reducer.c:513:7-513: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1080:6-1080: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1082:6-1082: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.BOUNDED-6.pals.c.v+nlh-reducer.c:717:6-717:19)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:523:6-523: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.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1091:6-1091:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:531:6-531:18)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:346:9-346:51)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:1093:6-1093: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.BOUNDED-6.pals.c.v+nlh-reducer.c:534:6-534: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.BOUNDED-6.pals.c.v+nlh-reducer.c:348:8-348: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.BOUNDED-6.pals.c.v+nlh-reducer.c:350:8-350:36)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:540:7-540: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.BOUNDED-6.pals.c.v+nlh-reducer.c:352:8-352: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.BOUNDED-6.pals.c.v+nlh-reducer.c:354:7-354: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.BOUNDED-6.pals.c.v+nlh-reducer.c:545:6-545: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.BOUNDED-6.pals.c.v+nlh-reducer.c:547:6-547: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.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:360:9-360: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.BOUNDED-6.pals.c.v+nlh-reducer.c:362:7-362: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.BOUNDED-6.pals.c.v+nlh-reducer.c:364:7-364: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.BOUNDED-6.pals.c.v+nlh-reducer.c:370:9-370: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.BOUNDED-6.pals.c.v+nlh-reducer.c:372:7-372: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.BOUNDED-6.pals.c.v+nlh-reducer.c:736:7-736: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.BOUNDED-6.pals.c.v+nlh-reducer.c:556:6-556: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.BOUNDED-6.pals.c.v+nlh-reducer.c:558:6-558: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)
