./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_opt-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_opt-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_opt-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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:445:2-445:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:785:2-785:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:994:2-994:13)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:269-269)
  on line 307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:307-307)
  on line 345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:345-345)
  on line 402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:402-402)
  on line 412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:412-412)
  on line 430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:430-430)
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:441-441)
  on line 467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:467-467)
  on line 479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:479-479)
  on line 505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:505-505)
  on line 517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:517-517)
  on line 543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:543-543)
  on line 572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:572-572)
  on line 582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:582-582)
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:600-600)
  on line 609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:609-609)
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:647-647)
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:685-685)
  on line 742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:742-742)
  on line 752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:752-752)
  on line 770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:770-770)
  on line 781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:781-781)
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:818-818)
  on line 855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:855-855)
  on line 901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:901-901)
  on line 916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:916-916)
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:920-920)
  on line 956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:956-956)
  on line 967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:967-967)
  on line 981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:981-981)
  on line 1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1292-1292)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1314-1314)
  on line 1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1412-1412)
  on line 1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1434-1434)
  on line 1532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1532-1532)
  on line 1554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1554-1554)
  on line 1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1591-1591)
  on line 1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1598-1598)
  on line 1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1604-1604)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1611-1611)
  on line 1617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1617-1617)
  on line 1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1622-1622)
  on line 1627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1627-1627)
  on line 1632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1632-1632)
  on line 1637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1637-1637)
  on line 1644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1644-1644)
  on line 1670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1670-1670)
  on line 1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1685-1685)
  on line 1741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1741-1741)
  on line 1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1752-1752)
  on line 1768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1768-1768)
  on line 1775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1775-1775)
  on line 1781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1781-1781)
  on line 1788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1788-1788)
  on line 1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1794-1794)
  on line 1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1799-1799)
  on line 1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1804-1804)
  on line 1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1809-1809)
  on line 1814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1814-1814)
  on line 1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1848-1848)
  on line 1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1854-1854)
  on line 1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1867-1867)
  on line 1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1872-1872)
  on line 1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1877-1877)
  on line 1882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1882-1882)
  on line 1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1887-1887)
  on line 1894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1894-1894)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1920-1920)
  on line 1927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1927-1927)
  on line 1953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1953-1953)
  on line 1968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1968-1968)
  on line 2005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2005-2005)
  on line 2051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2051-2051)
  on line 2066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2066-2066)
  on line 2070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2070-2070)
  on line 2096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2096-2096)
  on line 2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2111-2111)
  on line 2115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2115-2115)
  on line 2124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2124-2124)
  on line 2150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2150-2150)
  on line 2165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2165-2165)
  on line 2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2211-2211)
  on line 2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2226-2226)
  on line 2230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2230-2230)
  on line 2266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2266-2266)
  on line 2277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2277-2277)
  on line 2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2293-2293)
  on line 2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2300-2300)
  on line 2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2306-2306)
  on line 2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2313-2313)
  on line 2319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2319-2319)
  on line 2324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2324-2324)
  on line 2329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2329-2329)
  on line 2334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2334-2334)
  on line 2339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2339-2339)
  on line 2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2346-2346)
  on line 2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2372-2372)
  on line 2379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2379-2379)
  on line 2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2405-2405)
  on line 2412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2412-2412)
  on line 2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2438-2438)
  on line 2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2446-2446)
  on line 2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2451-2451)
  on line 2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2457-2457)
  on line 2462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2462-2462)
  on line 2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2468-2468)
  on line 2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2473-2473)
  on line 2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2478-2478)
  on line 2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2483-2483)
  on line 2490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2490-2490)
  on line 2512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2512-2512)
  on line 2533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2533-2533)
  on line 2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2541-2541)
  on line 2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2563-2563)
  on line 2584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2584-2584)
  on line 2592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2592-2592)
  on line 2614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2614-2614)
  on line 2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2635-2635)
  on line 2644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2644-2644)
  on line 2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2649-2649)
  on line 2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2655-2655)
  on line 2660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2660-2660)
  on line 2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2666-2666)
  on line 2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2671-2671)
  on line 2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2676-2676)
  on line 2681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2681-2681)
  on line 2709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2709-2709)
  on line 2737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2737-2737)
  on line 2765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2765-2765)
  on line 2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2773-2773)
  on line 2778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2778-2778)
  on line 2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2784-2784)
  on line 2789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2789-2789)
  on line 2795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2795-2795)
  on line 2800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2800-2800)
  on line 2805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2805-2805)
  on line 2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2810-2810)
  on line 2817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2817-2817)
  on line 2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2839-2839)
  on line 2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2860-2860)
  on line 2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2868-2868)
  on line 2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2890-2890)
  on line 2911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2911-2911)
  on line 2919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2919-2919)
  on line 2941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2941-2941)
  on line 2962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2962-2962)
  on line 2969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2969-2969)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 893
  dead: 149 (2 in uncalled functions)
  total lines: 1042
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___6 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2223:6-2223: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1731:8-1731: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1733:8-1733:36)
[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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:392:9-392: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1735:8-1735: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:394:8-394:36)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1737:7-1737: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:396:8-396:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1739:7-1739:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:398:8-398:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:400:7-400:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1745:9-1745:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1747:7-1747: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:406:9-406:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:408:7-408:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1750:7-1750:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:410:7-410: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:416:9-416:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:418:7-418:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:805:7-805: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1761:9-1761:51)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:814:6-814:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:428:6-428: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2254:9-2254:51)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:816:6-816:15)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2256:8-2256: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2258:8-2258: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2260:8-2260:36)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:437:6-437:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2262:7-2262:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:439:6-439:15)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2264:7-2264: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2270:9-2270:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2272:7-2272:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2275:7-2275: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2286:9-2286:51)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:842:7-842:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:465:7-465:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:851:6-851: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1836:9-1836:51)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:853:6-853:15)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1838:8-1838: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1840:8-1840:36)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:475:6-475:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1842:8-1842:36)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:477:6-477:15)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1844:7-1844:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1846:7-1846: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1852:9-1852:51)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1265:6-1265: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1267:6-1267:22)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:879:7-879:20)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:503:7-503:20)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1278:6-1278: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1280:6-1280:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:513:6-513:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:515:6-515:15)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1964:6-1964:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1966:6-1966: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:899:9-899:51)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___2 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:913:6-913:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:541:7-541:20)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1992:7-1992:20)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1385:6-1385: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1387:6-1387:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2001:6-2001:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2003:6-2003: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:944:9-944: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:946:8-946:36)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1398:6-1398: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:948:8-948:36)
[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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:562:9-562:51)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1400:6-1400: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:950:8-950: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:564:8-564:36)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:952:7-952: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:566:8-566:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:954:7-954:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:568:8-568:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:570:7-570:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:960:9-960:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:962:7-962: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:576:9-576:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:578:7-578:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:965:7-965:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:580:7-580: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:586:9-586:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:588:7-588:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2029:7-2029: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:598:6-598:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:607:6-607:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:613:7-613:19)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:620:6-620: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:622:6-622:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1505:6-1505: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2049:9-2049: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1507:6-1507:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:633:6-633: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:635:6-635:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:249:6-249: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2063:6-2063:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1518:6-1518: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1520:6-1520:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:645:6-645:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:651:7-651:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:658:6-658: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:660:6-660:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:267:6-267:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:273:7-273:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:671:6-671: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:673:6-673:22)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:277:6-277:21)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:280:6-280: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:282:6-282: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2094:9-2094:51)
[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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1584:9-1584:51)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:683:6-683:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:290:6-290:21)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:689:7-689:19)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:293:6-293:19)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___5 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2108:6-2108:22)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:295:6-295:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:696:6-696: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:698:6-698:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:305:6-305:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:709:6-709: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:711:6-711:22)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:315:6-315:21)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:318:6-318: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:320:6-320:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2161:6-2161:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2163:6-2163:15)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:328:6-328:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1681:6-1681:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:331:6-331:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1683:6-1683:15)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:333:6-333: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:732:9-732:51)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:343:6-343:19)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:734:8-734: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:736:8-736:36)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:349:7-349:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:738:8-738:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:740:7-740:20)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:353:6-353:21)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:356:6-356: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:746:9-746:51)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:358:6-358:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:748:7-748:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2189:7-2189:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:750:7-750: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:756:9-756:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:758:7-758:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:366:6-366:21)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:369:6-369:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1709:7-1709:20)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:371:6-371:22)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:768:6-768:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:777:6-777:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:779:6-779: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:2209:9-2209: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_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1729:9-1729:51)
[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)
