./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.BOUNDED-6.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.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.4.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, 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] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:407:2-407:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:686:2-686:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:830:2-830:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:858:2-858:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:886:2-886: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:251-251)
  on line 283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:283-283)
  on line 315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:315-315)
  on line 368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:368-368)
  on line 378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:378-378)
  on line 396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:396-396)
  on line 426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:426-426)
  on line 453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:453-453)
  on line 480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:480-480)
  on line 509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:509-509)
  on line 519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:519-519)
  on line 537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:537-537)
  on line 548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:548-548)
  on line 554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:554-554)
  on line 562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:562-562)
  on line 594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:594-594)
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:647-647)
  on line 657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:657-657)
  on line 675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:675-675)
  on line 720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:720-720)
  on line 747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:747-747)
  on line 790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:790-790)
  on line 801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:801-801)
  on line 819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:819-819)
  on line 1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1099-1099)
  on line 1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1116-1116)
  on line 1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1200-1200)
  on line 1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1217-1217)
  on line 1301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1301-1301)
  on line 1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1318-1318)
  on line 1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1363-1363)
  on line 1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1369-1369)
  on line 1383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1383-1383)
  on line 1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1416-1416)
  on line 1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1441-1441)
  on line 1453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1453-1453)
  on line 1478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1478-1478)
  on line 1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1490-1490)
  on line 1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1515-1515)
  on line 1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1521-1521)
  on line 1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1528-1528)
  on line 1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1533-1533)
  on line 1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1539-1539)
  on line 1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1544-1544)
  on line 1550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1550-1550)
  on line 1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1555-1555)
  on line 1560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1560-1560)
  on line 1565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1565-1565)
  on line 1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1572-1572)
  on line 1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1589-1589)
  on line 1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1605-1605)
  on line 1613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1613-1613)
  on line 1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1630-1630)
  on line 1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1646-1646)
  on line 1656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1656-1656)
  on line 1663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1663-1663)
  on line 1668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1668-1668)
  on line 1674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1674-1674)
  on line 1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1679-1679)
  on line 1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1685-1685)
  on line 1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1690-1690)
  on line 1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1695-1695)
  on line 1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1700-1700)
  on line 1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1727-1727)
  on line 1754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1754-1754)
  on line 1781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1781-1781)
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1787-1787)
  on line 1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1794-1794)
  on line 1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1799-1799)
  on line 1805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1805-1805)
  on line 1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1810-1810)
  on line 1816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1816-1816)
  on line 1821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1821-1821)
  on line 1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1826-1826)
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1838-1838)
  on line 1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1855-1855)
  on line 1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1871-1871)
  on line 1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1879-1879)
  on line 1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1896-1896)
  on line 1912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1912-1912)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1920-1920)
  on line 1937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1937-1937)
  on line 1953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1953-1953)
  on line 1960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1960-1960)
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1965-1965)
[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 )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:745:7-745:29)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:573:6-573: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1175:6-1175: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1177:6-1177: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.BOUNDED-6.pals.c.v+nlh-reducer.c:394:6-394: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:582:6-582: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.BOUNDED-6.pals.c.v+nlh-reducer.c:584:6-584: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:402:6-402:18)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:1186:6-1186: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.BOUNDED-6.pals.c.v+nlh-reducer.c:757:7-757:20)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:405:6-405: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1188:6-1188:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:592:6-592: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.BOUNDED-6.pals.c.v+nlh-reducer.c:598:7-598: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.BOUNDED-6.pals.c.v+nlh-reducer.c:603:6-603: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.BOUNDED-6.pals.c.v+nlh-reducer.c:605:6-605: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.BOUNDED-6.pals.c.v+nlh-reducer.c:614:6-614: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.BOUNDED-6.pals.c.v+nlh-reducer.c:616:6-616: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:231:6-231: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.BOUNDED-6.pals.c.v+nlh-reducer.c:424:7-424: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:786:7-786: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.BOUNDED-6.pals.c.v+nlh-reducer.c:788:7-788:19)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:432:6-432: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.BOUNDED-6.pals.c.v+nlh-reducer.c:796:7-796: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.BOUNDED-6.pals.c.v+nlh-reducer.c:799:7-799: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1276:6-1276: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1278:6-1278: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:246:6-246: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:249:6-249:19)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:255:7-255: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.BOUNDED-6.pals.c.v+nlh-reducer.c:637:9-637: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.BOUNDED-6.pals.c.v+nlh-reducer.c:639:8-639: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.BOUNDED-6.pals.c.v+nlh-reducer.c:260:6-260: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.BOUNDED-6.pals.c.v+nlh-reducer.c:641:8-641: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1287:6-1287: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:262:6-262: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.BOUNDED-6.pals.c.v+nlh-reducer.c:643:8-643: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1289:6-1289: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.BOUNDED-6.pals.c.v+nlh-reducer.c:645:7-645: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:651:9-651: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.BOUNDED-6.pals.c.v+nlh-reducer.c:653:7-653: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.BOUNDED-6.pals.c.v+nlh-reducer.c:451:7-451: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.BOUNDED-6.pals.c.v+nlh-reducer.c:655:7-655: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:271:6-271: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:661:9-661:51)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:273:6-273: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:663:7-663:19)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:459:6-459: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:281:6-281: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:673:6-673:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:287:7-287: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.BOUNDED-6.pals.c.v+nlh-reducer.c:292:6-292: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.BOUNDED-6.pals.c.v+nlh-reducer.c:294:6-294: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:681:6-681: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:684:6-684: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.BOUNDED-6.pals.c.v+nlh-reducer.c:303:6-303: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.BOUNDED-6.pals.c.v+nlh-reducer.c:478:7-478: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:305:6-305:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:313:6-313: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.BOUNDED-6.pals.c.v+nlh-reducer.c:319:7-319: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.BOUNDED-6.pals.c.v+nlh-reducer.c:324:6-324: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.BOUNDED-6.pals.c.v+nlh-reducer.c:326:6-326: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:703:7-703: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:499:9-499:51)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:1074:6-1074: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.BOUNDED-6.pals.c.v+nlh-reducer.c:501:8-501:36)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:1076:6-1076:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:503:8-503:36)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:711:6-711: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.BOUNDED-6.pals.c.v+nlh-reducer.c:505:8-505: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.BOUNDED-6.pals.c.v+nlh-reducer.c:335:6-335: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.BOUNDED-6.pals.c.v+nlh-reducer.c:507:7-507: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:337:6-337: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.BOUNDED-6.pals.c.v+nlh-reducer.c:513:9-513: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.BOUNDED-6.pals.c.v+nlh-reducer.c:515:7-515: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.BOUNDED-6.pals.c.v+nlh-reducer.c:517:7-517: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1085:6-1085: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.BOUNDED-6.pals.c.v+nlh-reducer.c:1087:6-1087:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:718:7-718:29)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:523:9-523: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.BOUNDED-6.pals.c.v+nlh-reducer.c:525:7-525: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:535:6-535:22)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:730:7-730:20)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:543:6-543: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:358:9-358:51)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:546:6-546: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.BOUNDED-6.pals.c.v+nlh-reducer.c:360:8-360: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.BOUNDED-6.pals.c.v+nlh-reducer.c:362:8-362:36)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:552:7-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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:364:8-364: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.BOUNDED-6.pals.c.v+nlh-reducer.c:366:7-366:20)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:738:6-738: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.BOUNDED-6.pals.c.v+nlh-reducer.c:372:9-372:51)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:560:6-560: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.BOUNDED-6.pals.c.v+nlh-reducer.c:374:7-374: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.BOUNDED-6.pals.c.v+nlh-reducer.c:376:7-376: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.BOUNDED-6.pals.c.v+nlh-reducer.c:566:7-566: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.4.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:382:9-382:51)
[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.BOUNDED-6.pals.c.v+nlh-reducer.c:571:6-571: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.BOUNDED-6.pals.c.v+nlh-reducer.c:384:7-384:19)
[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
