./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.3.ufo.UNBOUNDED.pals.c.v+lhb-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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] nomsg, r1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, init__r121, init__r131, init__r211, init__r231, init__r311, init__r321, main__i2, init__r122, cond
[Info] 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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:413:2-413:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:720:2-720:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:914:2-914:13)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:255-255)
  on line 287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:287-287)
  on line 319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:319-319)
  on line 372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:372-372)
  on line 382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:382-382)
  on line 400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:400-400)
  on line 409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:409-409)
  on line 432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:432-432)
  on line 442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:442-442)
  on line 465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:465-465)
  on line 475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:475-475)
  on line 498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:498-498)
  on line 527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:527-527)
  on line 537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:537-537)
  on line 555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:555-555)
  on line 562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:562-562)
  on line 594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:594-594)
  on line 626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:626-626)
  on line 679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:679-679)
  on line 689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:689-689)
  on line 707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:707-707)
  on line 716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:716-716)
  on line 748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:748-748)
  on line 780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:780-780)
  on line 823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:823-823)
  on line 838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:838-838)
  on line 842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:842-842)
  on line 878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:878-878)
  on line 889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:889-889)
  on line 903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:903-903)
  on line 1195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1195-1195)
  on line 1212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1212-1212)
  on line 1301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1301-1301)
  on line 1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1318-1318)
  on line 1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1407-1407)
  on line 1424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1424-1424)
  on line 1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1456-1456)
  on line 1463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1463-1463)
  on line 1469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1469-1469)
  on line 1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1476-1476)
  on line 1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1482-1482)
  on line 1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1487-1487)
  on line 1492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1492-1492)
  on line 1497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1497-1497)
  on line 1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1502-1502)
  on line 1509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1509-1509)
  on line 1535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1535-1535)
  on line 1548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1548-1548)
  on line 1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1601-1601)
  on line 1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1612-1612)
  on line 1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1628-1628)
  on line 1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1635-1635)
  on line 1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1641-1641)
  on line 1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1648-1648)
  on line 1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1654-1654)
  on line 1659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1659-1659)
  on line 1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1664-1664)
  on line 1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1669-1669)
  on line 1674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1674-1674)
  on line 1708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1708-1708)
  on line 1714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1714-1714)
  on line 1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1727-1727)
  on line 1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1732-1732)
  on line 1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1737-1737)
  on line 1742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1742-1742)
  on line 1747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1747-1747)
  on line 1754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1754-1754)
  on line 1780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1780-1780)
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1787-1787)
  on line 1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1813-1813)
  on line 1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1826-1826)
  on line 1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1858-1858)
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1901-1901)
  on line 1916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1916-1916)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1920-1920)
  on line 1946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1946-1946)
  on line 1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1961-1961)
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1965-1965)
  on line 1974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1974-1974)
  on line 2000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2000-2000)
  on line 2013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2013-2013)
  on line 2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2056-2056)
  on line 2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2071-2071)
  on line 2075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2075-2075)
  on line 2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2111-2111)
  on line 2122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2122-2122)
  on line 2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2138-2138)
  on line 2145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2145-2145)
  on line 2151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2151-2151)
  on line 2158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2158-2158)
  on line 2164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2164-2164)
  on line 2169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2169-2169)
  on line 2174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2174-2174)
  on line 2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2179-2179)
  on line 2184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2184-2184)
  on line 2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2191-2191)
  on line 2217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2217-2217)
  on line 2224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2224-2224)
  on line 2250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2250-2250)
  on line 2257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2257-2257)
  on line 2283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2283-2283)
  on line 2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2291-2291)
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2296-2296)
  on line 2302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2302-2302)
  on line 2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2307-2307)
  on line 2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2313-2313)
  on line 2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2318-2318)
  on line 2323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2323-2323)
  on line 2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2328-2328)
  on line 2335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2335-2335)
  on line 2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2352-2352)
  on line 2368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2368-2368)
  on line 2376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2376-2376)
  on line 2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2393-2393)
  on line 2409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2409-2409)
  on line 2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2417-2417)
  on line 2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2434-2434)
  on line 2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2450-2450)
  on line 2459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2459-2459)
  on line 2464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2464-2464)
  on line 2470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2470-2470)
  on line 2475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2475-2475)
  on line 2481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2481-2481)
  on line 2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2486-2486)
  on line 2491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2491-2491)
  on line 2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2496-2496)
  on line 2524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2524-2524)
  on line 2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2552-2552)
  on line 2580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2580-2580)
  on line 2588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2588-2588)
  on line 2593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2593-2593)
  on line 2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2599-2599)
  on line 2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2604-2604)
  on line 2610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2610-2610)
  on line 2615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2615-2615)
  on line 2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2620-2620)
  on line 2625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2625-2625)
  on line 2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2632-2632)
  on line 2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2649-2649)
  on line 2665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2665-2665)
  on line 2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2673-2673)
  on line 2690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2690-2690)
  on line 2706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2706-2706)
  on line 2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2714-2714)
  on line 2731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2731-2731)
  on line 2747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2747-2747)
  on line 2754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2754-2754)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 808
  dead: 149 (2 in uncalled functions)
  total lines: 957
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:776:6-776:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:778:6-778:15)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1822:6-1822:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1170:6-1170:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:398:6-398:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1824:6-1824:15)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1172:6-1172:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:405:6-405:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:407:6-407:15)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1181:6-1181:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1183:6-1183:22)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:801:7-801: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1847:7-1847:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:430:7-430: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1854:6-1854:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1856:6-1856:15)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:438:6-438:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:440:6-440:15)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:821:9-821: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1276:6-1276:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1278:6-1278:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___2 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:835:6-835:22)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1879:7-1879:20)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1287:6-1287:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1289:6-1289:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:463:7-463: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:471:6-471:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:473:6-473:15)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:866:9-866:51)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1899:9-1899:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:868:8-868:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:870:8-870:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:872:8-872: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:874:7-874:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:876:7-876:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:882:9-882:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:884:7-884:20)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1913:6-1913:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:887:7-887:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:496:7-496:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1382:6-1382:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1384:6-1384: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1393:6-1393:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1395:6-1395: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:517:9-517:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:519:8-519:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:521:8-521:36)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1944:9-1944:51)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:523:8-523:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:525:7-525:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:531:9-531:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:533:7-533:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:535:7-535:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:541:9-541:51)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___5 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1958:6-1958:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:543:7-543:19)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1449:9-1449:51)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:553:6-553:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:566:7-566: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:571:6-571: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2009:6-2009:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:573:6-573:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2011:6-2011:15)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:582:6-582:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:584:6-584:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:592:6-592:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:598:7-598: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1544:6-1544:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:603:6-603:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1546:6-1546:15)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:605:6-605:22)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2034:7-2034:20)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:614:6-614:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:616:6-616: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:624:6-624:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:630:7-630:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:237:6-237:19)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2054:9-2054: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:635:6-635:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1569:7-1569:20)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:637:6-637:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___6 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2068:6-2068: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:646:6-646:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:648:6-648:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:253:6-253:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:259:7-259: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:264:6-264:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1589:9-1589:51)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:266:6-266:22)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1591:8-1591:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1593:8-1593:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1595:8-1595: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1597:7-1597:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1599:7-1599:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1605:9-1605:51)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:275:6-275:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1607:7-1607:20)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:277:6-277: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2099:9-2099:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2101:8-2101:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1610:7-1610:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:669:9-669:51)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2103:8-2103:36)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:671:8-671:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2105:8-2105:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:673:8-673: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2107:7-2107:20)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:675:8-675:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2109:7-2109:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:677:7-677:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:285:6-285:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2115:9-2115:51)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:683:9-683:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2117:7-2117:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:685:7-685:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:291:7-291:19)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1621:9-1621:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:687:7-687:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2120:7-2120:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:296:6-296:19)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:693:9-693:51)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:298:6-298:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:695:7-695:19)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2131:9-2131: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:307:6-307:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:705:6-705:22)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:309:6-309:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:712:6-712:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:714:6-714:15)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:317:6-317:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:323:7-323:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:328:6-328:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:330:6-330: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:339:6-339:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:341:6-341: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1696:9-1696:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:737:7-737:20)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1698:8-1698:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1700:8-1700:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1702:8-1702: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1704:7-1704:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1706:7-1706: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:744:6-744:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:746:6-746:15)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1712:9-1712:51)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:362:9-362:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:364:8-364:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:366:8-366:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:368:8-368:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:370:7-370:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:376:9-376:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:378:7-378:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:380:7-380: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.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:769:7-769:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:386:9-386:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:388:7-388:19)
[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)
