./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+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.1.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.1.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, assert__arg, 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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:401:2-401:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:708:2-708:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1057:2-1057:13)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:243-243)
  on line 275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:275-275)
  on line 307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:307-307)
  on line 360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:360-360)
  on line 370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:370-370)
  on line 388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:388-388)
  on line 397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:397-397)
  on line 420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:420-420)
  on line 430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:430-430)
  on line 453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:453-453)
  on line 463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:463-463)
  on line 486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:486-486)
  on line 515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:515-515)
  on line 525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:525-525)
  on line 543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:543-543)
  on line 550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:550-550)
  on line 582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:582-582)
  on line 614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:614-614)
  on line 667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:667-667)
  on line 677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:677-677)
  on line 695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:695-695)
  on line 704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:704-704)
  on line 736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:736-736)
  on line 768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:768-768)
  on line 811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:811-811)
  on line 826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:826-826)
  on line 830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:830-830)
  on line 856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:856-856)
  on line 871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:871-871)
  on line 875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:875-875)
  on line 884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:884-884)
  on line 910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:910-910)
  on line 923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:923-923)
  on line 966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:966-966)
  on line 981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:981-981)
  on line 985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:985-985)
  on line 1021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1021-1021)
  on line 1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1032-1032)
  on line 1046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1046-1046)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1338-1338)
  on line 1355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1355-1355)
  on line 1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1444-1444)
  on line 1461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1461-1461)
  on line 1550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1550-1550)
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1567-1567)
  on line 1599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1599-1599)
  on line 1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1606-1606)
  on line 1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1612-1612)
  on line 1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1619-1619)
  on line 1625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1625-1625)
  on line 1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1630-1630)
  on line 1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1635-1635)
  on line 1640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1640-1640)
  on line 1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1645-1645)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1652-1652)
  on line 1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1678-1678)
  on line 1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1685-1685)
  on line 1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1711-1711)
  on line 1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1724-1724)
  on line 1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1756-1756)
  on line 1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1799-1799)
  on line 1814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1814-1814)
  on line 1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1818-1818)
  on line 1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1854-1854)
  on line 1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1865-1865)
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1881-1881)
  on line 1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1888-1888)
  on line 1894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1894-1894)
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1901-1901)
  on line 1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1907-1907)
  on line 1912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1912-1912)
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1917-1917)
  on line 1922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1922-1922)
  on line 1927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1927-1927)
  on line 1934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1934-1934)
  on line 1960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1960-1960)
  on line 1973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1973-1973)
  on line 2026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2026-2026)
  on line 2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2037-2037)
  on line 2053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2053-2053)
  on line 2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2060-2060)
  on line 2066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2066-2066)
  on line 2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2073-2073)
  on line 2079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2079-2079)
  on line 2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2084-2084)
  on line 2089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2089-2089)
  on line 2094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2094-2094)
  on line 2099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2099-2099)
  on line 2133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2133-2133)
  on line 2139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2139-2139)
  on line 2152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2152-2152)
  on line 2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2157-2157)
  on line 2162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2162-2162)
  on line 2167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2167-2167)
  on line 2172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2172-2172)
  on line 2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2179-2179)
  on line 2205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2205-2205)
  on line 2212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2212-2212)
  on line 2238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2238-2238)
  on line 2245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2245-2245)
  on line 2271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2271-2271)
  on line 2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2279-2279)
  on line 2284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2284-2284)
  on line 2290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2290-2290)
  on line 2295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2295-2295)
  on line 2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2301-2301)
  on line 2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2306-2306)
  on line 2311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2311-2311)
  on line 2316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2316-2316)
  on line 2323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2323-2323)
  on line 2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2340-2340)
  on line 2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2356-2356)
  on line 2364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2364-2364)
  on line 2381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2381-2381)
  on line 2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2397-2397)
  on line 2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2405-2405)
  on line 2422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2422-2422)
  on line 2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2438-2438)
  on line 2447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2447-2447)
  on line 2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2452-2452)
  on line 2458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2458-2458)
  on line 2463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2463-2463)
  on line 2469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2469-2469)
  on line 2474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2474-2474)
  on line 2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2479-2479)
  on line 2484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2484-2484)
  on line 2512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2512-2512)
  on line 2540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2540-2540)
  on line 2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2568-2568)
  on line 2576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2576-2576)
  on line 2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2581-2581)
  on line 2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2587-2587)
  on line 2592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2592-2592)
  on line 2598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2598-2598)
  on line 2603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2603-2603)
  on line 2608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2608-2608)
  on line 2613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2613-2613)
  on line 2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2620-2620)
  on line 2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2637-2637)
  on line 2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2653-2653)
  on line 2661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2661-2661)
  on line 2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2678-2678)
  on line 2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2694-2694)
  on line 2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2702-2702)
  on line 2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2719-2719)
  on line 2735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2735-2735)
  on line 2742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2742-2742)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 796
  dead: 149 (2 in uncalled functions)
  total lines: 945
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:393:6-393:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:395:6-395:15)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1777:7-1777:20)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:789:7-789:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:418:7-418:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:426:6-426:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:428:6-428: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1797:9-1797: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:809:9-809:51)
[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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1811:6-1811: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:823:6-823: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:451:7-451: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:459:6-459:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:461:6-461: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1842:9-1842: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:854:9-854:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1844:8-1844:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1846:8-1846:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1848:8-1848:36)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1850:7-1850:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1852:7-1852:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1858:9-1858:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1860:7-1860:20)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:868:6-868:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1863:7-1863:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:484:7-484:20)
[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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1874:9-1874:51)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:919:6-919:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:921:6-921:15)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1313:6-1313:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1315:6-1315:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:505:9-505:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:507:8-507:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:509:8-509:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:511:8-511:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:513:7-513:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:519:9-519: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1324:6-1324:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:521:7-521:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1326:6-1326:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:523:7-523:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:529:9-529:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:531:7-531:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:944:7-944:20)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:541:6-541:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1969:6-1969:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1971:6-1971:15)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:548:6-548:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:554:7-554: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:559:6-559:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:561:6-561:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:570:6-570:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:572:6-572:22)
[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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:964:9-964: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1419:6-1419:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1421:6-1421: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1994:7-1994:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:580:6-580:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:586:7-586:19)
[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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:978:6-978:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:591:6-591:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:593:6-593:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1430:6-1430:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1432:6-1432:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:602:6-602:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:604:6-604:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2014:9-2014:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2016:8-2016:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2018:8-2018:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2020:8-2020:36)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:612:6-612:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2022:7-2022:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2024:7-2024:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:618:7-618: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:225:6-225:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1009:9-1009: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2030:9-2030:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1011:8-1011:36)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:623:6-623:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2032:7-2032:20)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1013:8-1013: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:625:6-625:22)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1015:8-1015:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2035:7-2035:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1017:7-1017:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1019:7-1019:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1025:9-1025:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1027:7-1027:20)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:634:6-634:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1030:7-1030:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:636:6-636:22)
[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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2046:9-2046: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1525:6-1525:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:241:6-241:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1527:6-1527:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:247:7-247: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:252:6-252:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:254:6-254:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1536:6-1536:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1538:6-1538:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:263:6-263:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:265:6-265:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:657:9-657:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:659:8-659:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:661:8-661:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:663:8-663:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:665:7-665:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:273:6-273:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:671:9-671:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:673:7-673:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:279:7-279:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:675:7-675:20)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:284:6-284:19)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:681:9-681:51)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:286:6-286:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:683:7-683: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1592:9-1592: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2121:9-2121:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2123:8-2123:36)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:295:6-295:19)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2125:8-2125:36)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:693:6-693:22)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:297:6-297:22)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2127:8-2127:36)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2129:7-2129: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:700:6-700:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2131:7-2131:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:702:6-702: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2137:9-2137:51)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:305:6-305:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:311:7-311:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:316:6-316:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:318:6-318:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:327:6-327:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:329:6-329:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:725:7-725:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1720:6-1720: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:732:6-732:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1722:6-1722:15)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:734:6-734: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:350:9-350:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:352:8-352:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:354:8-354:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:356:8-356:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:358:7-358:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:364:9-364:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:366:7-366:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:368:7-368:20)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1745:7-1745:20)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:757:7-757:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:374:9-374:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:376:7-376: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1752:6-1752: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.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:764:6-764:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1754:6-1754:15)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:766:6-766:15)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.1.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:386:6-386:22)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
