./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.4.ufo.BOUNDED-6.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.4.ufo.BOUNDED-6.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.4.ufo.BOUNDED-6.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, main__i2, init__r121, init__r131, init__r211, init__r231, init__r311, init__r321, 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] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:414:2-414:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:693:2-693:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1025:2-1025:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1053:2-1053:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1081:2-1081:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:258-258)
  on line 290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:290-290)
  on line 322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:322-322)
  on line 375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:375-375)
  on line 385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:385-385)
  on line 403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:403-403)
  on line 433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:433-433)
  on line 460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:460-460)
  on line 487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:487-487)
  on line 516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:516-516)
  on line 526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:526-526)
  on line 544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:544-544)
  on line 555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:555-555)
  on line 561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:561-561)
  on line 569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:569-569)
  on line 601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:601-601)
  on line 654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:654-654)
  on line 664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:664-664)
  on line 682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:682-682)
  on line 726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:726-726)
  on line 752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:752-752)
  on line 784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:784-784)
  on line 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:799-799)
  on line 803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:803-803)
  on line 829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:829-829)
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:844-844)
  on line 848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:848-848)
  on line 857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:857-857)
  on line 882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:882-882)
  on line 900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:900-900)
  on line 932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:932-932)
  on line 947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:947-947)
  on line 951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:951-951)
  on line 987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:987-987)
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:998-998)
  on line 1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1014-1014)
  on line 1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1294-1294)
  on line 1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1311-1311)
  on line 1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1395-1395)
  on line 1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1412-1412)
  on line 1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1496-1496)
  on line 1513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1513-1513)
  on line 1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1551-1551)
  on line 1558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1558-1558)
  on line 1564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1564-1564)
  on line 1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1571-1571)
  on line 1577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1577-1577)
  on line 1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1582-1582)
  on line 1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1587-1587)
  on line 1592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1592-1592)
  on line 1597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1597-1597)
  on line 1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1604-1604)
  on line 1629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1629-1629)
  on line 1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1636-1636)
  on line 1661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1661-1661)
  on line 1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1679-1679)
  on line 1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1705-1705)
  on line 1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1737-1737)
  on line 1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1752-1752)
  on line 1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1756-1756)
  on line 1792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1792-1792)
  on line 1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1803-1803)
  on line 1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1820-1820)
  on line 1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1827-1827)
  on line 1833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1833-1833)
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1840-1840)
  on line 1846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1846-1846)
  on line 1851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1851-1851)
  on line 1856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1856-1856)
  on line 1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1861-1861)
  on line 1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1866-1866)
  on line 1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1873-1873)
  on line 1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1898-1898)
  on line 1916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1916-1916)
  on line 1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1958-1958)
  on line 1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1969-1969)
  on line 1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1986-1986)
  on line 1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1993-1993)
  on line 1999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1999-1999)
  on line 2006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2006-2006)
  on line 2012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2012-2012)
  on line 2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2017-2017)
  on line 2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2022-2022)
  on line 2027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2027-2027)
  on line 2032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2032-2032)
  on line 2066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2066-2066)
  on line 2072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2072-2072)
  on line 2086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2086-2086)
  on line 2091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2091-2091)
  on line 2096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2096-2096)
  on line 2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2101-2101)
  on line 2106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2106-2106)
  on line 2113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2113-2113)
  on line 2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2138-2138)
  on line 2145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2145-2145)
  on line 2170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2170-2170)
  on line 2177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2177-2177)
  on line 2202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2202-2202)
  on line 2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2208-2208)
  on line 2215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2215-2215)
  on line 2220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2220-2220)
  on line 2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2226-2226)
  on line 2231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2231-2231)
  on line 2237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2237-2237)
  on line 2242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2242-2242)
  on line 2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2247-2247)
  on line 2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2252-2252)
  on line 2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2259-2259)
  on line 2276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2276-2276)
  on line 2292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2292-2292)
  on line 2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2300-2300)
  on line 2317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2317-2317)
  on line 2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2333-2333)
  on line 2343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2343-2343)
  on line 2350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2350-2350)
  on line 2355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2355-2355)
  on line 2361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2361-2361)
  on line 2366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2366-2366)
  on line 2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2372-2372)
  on line 2377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2377-2377)
  on line 2382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2382-2382)
  on line 2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2387-2387)
  on line 2414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2414-2414)
  on line 2441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2441-2441)
  on line 2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2468-2468)
  on line 2474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2474-2474)
  on line 2481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2481-2481)
  on line 2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2486-2486)
  on line 2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2492-2492)
  on line 2497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2497-2497)
  on line 2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2503-2503)
  on line 2508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2508-2508)
  on line 2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2513-2513)
  on line 2518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2518-2518)
  on line 2525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2525-2525)
  on line 2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2542-2542)
  on line 2558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2558-2558)
  on line 2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2566-2566)
  on line 2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2583-2583)
  on line 2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2599-2599)
  on line 2607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2607-2607)
  on line 2624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2624-2624)
  on line 2640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2640-2640)
  on line 2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2647-2647)
  on line 2652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2652-2652)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 796
  dead: 147 (2 in uncalled functions)
  total lines: 943
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1715:7-1715:20)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:401:6-401: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:762:7-762:20)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:409:6-409:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:412:6-412:19)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1735:9-1735: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1749:6-1749: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:782:9-782:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:431:7-431:20)
[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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:796:6-796:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:439:6-439:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1780:9-1780:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1782:8-1782:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1784:8-1784: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1786:8-1786: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1788:7-1788:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1790:7-1790:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1796:9-1796:51)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:458:7-458:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1798:7-1798:20)
[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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:827:9-827:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1801:7-1801:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:466:6-466:19)
[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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:841:6-841: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1813:9-1813:51)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1269:6-1269:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1271:6-1271: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:891:6-891:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:485:7-485:20)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1280:6-1280:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1282:6-1282:22)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:898:7-898:29)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1907:6-1907:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:506:9-506:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:508:8-508:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:510:8-510:36)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:910:7-910:20)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:512:8-512:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:514:7-514:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:520:9-520:51)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1914:7-1914:29)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:522:7-522:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:524:7-524: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:530:9-530:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:532:7-532:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:542:6-542: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1926:7-1926: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1370:6-1370:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1372:6-1372: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:930:9-930:51)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:550:6-550:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:553:6-553:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:559:7-559:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1381:6-1381:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1383:6-1383:22)
[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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:944:6-944:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:567:6-567: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:573:7-573:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:578:6-578:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:580:6-580: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1946:9-1946:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1948:8-1948:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1950:8-1950: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1952:8-1952: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1954:7-1954:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1956:7-1956:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:589:6-589:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1962:9-1962: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_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:591:6-591:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1964:7-1964:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1967:7-1967:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:975:9-975:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:977:8-977: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:599:6-599:19)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:979:8-979: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:981:8-981:36)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:605:7-605:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:983:7-983:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:985:7-985:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:610:6-610: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1979:9-1979: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_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:612:6-612: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:991:9-991:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:993:7-993:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1471:6-1471:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1473:6-1473:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:996:7-996:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:621:6-621:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:623:6-623:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:238:6-238:19)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1482:6-1482: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1484:6-1484:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:253:6-253:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:256:6-256:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:262:7-262:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:644:9-644:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:646:8-646:36)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:267:6-267:19)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:648:8-648:36)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:269:6-269:22)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:650:8-650:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:652:7-652:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2054:9-2054:51)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:658:9-658:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2056:8-2056:36)
[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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1544:9-1544:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:660:7-660:19)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2058:8-2058:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:662:7-662:20)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2060:8-2060:36)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:278:6-278:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2062:7-2062: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:668:9-668:51)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:280:6-280:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2064:7-2064:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:670:7-670:19)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:2070:9-2070:51)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:288:6-288:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:680:6-680:22)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:294:7-294:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:299:6-299:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:301:6-301:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:688:6-688:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:691:6-691:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:310:6-310:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:312:6-312:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:320:6-320:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:326:7-326:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1670:6-1670:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:331:6-331:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:333:6-333:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:710:7-710:20)
[Warning][Deadcode][CWE-570] condition '(int )m2 > (int )max2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1677:7-1677:29)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:717:6-717:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:342:6-342:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:344:6-344:22)
[Warning][Deadcode][CWE-570] condition '(int )m2 > (int )max2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:724:7-724:29)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1689:7-1689:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1696:6-1696: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.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:736:7-736:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:365:9-365:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:367:8-367:36)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1703:7-1703:29)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:369:8-369:36)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:743:6-743:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:371:8-371:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:373:7-373:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:379:9-379:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:381:7-381:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:383:7-383:20)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:750:7-750:29)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:389:9-389:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.4.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:391:7-391:19)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
