./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] nomsg, r1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, main__i2, init__r121, init__r131, init__r211, init__r231, init__r311, init__r321, init__r122, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] 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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:407:2-407:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:704:2-704:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:848:2-848:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:876:2-876:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:904:2-904: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:251-251)
  on line 283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:283-283)
  on line 315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:315-315)
  on line 368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:368-368)
  on line 378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:378-378)
  on line 396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:396-396)
  on line 426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:426-426)
  on line 453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:453-453)
  on line 480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:480-480)
  on line 509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:509-509)
  on line 519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:519-519)
  on line 537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:537-537)
  on line 548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:548-548)
  on line 580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:580-580)
  on line 612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:612-612)
  on line 665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:665-665)
  on line 675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:675-675)
  on line 693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:693-693)
  on line 808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:808-808)
  on line 819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:819-819)
  on line 837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:837-837)
  on line 1117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1117-1117)
  on line 1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1134-1134)
  on line 1218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1218-1218)
  on line 1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1235-1235)
  on line 1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1319-1319)
  on line 1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1336-1336)
  on line 1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1381-1381)
  on line 1387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1387-1387)
  on line 1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1401-1401)
  on line 1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1434-1434)
  on line 1459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1459-1459)
  on line 1471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1471-1471)
  on line 1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1496-1496)
  on line 1508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1508-1508)
  on line 1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1533-1533)
  on line 1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1539-1539)
  on line 1546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1546-1546)
  on line 1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1551-1551)
  on line 1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1557-1557)
  on line 1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1562-1562)
  on line 1568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1568-1568)
  on line 1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1573-1573)
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1578-1578)
  on line 1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1583-1583)
  on line 1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1590-1590)
  on line 1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1607-1607)
  on line 1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1623-1623)
  on line 1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1631-1631)
  on line 1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1648-1648)
  on line 1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1664-1664)
  on line 1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1672-1672)
  on line 1689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1689-1689)
  on line 1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1705-1705)
  on line 1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1712-1712)
  on line 1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1719-1719)
  on line 1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1724-1724)
  on line 1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1730-1730)
  on line 1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1735-1735)
  on line 1741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1741-1741)
  on line 1746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1746-1746)
  on line 1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1751-1751)
  on line 1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1756-1756)
  on line 1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1783-1783)
  on line 1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1810-1810)
  on line 1837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1837-1837)
  on line 1843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1843-1843)
  on line 1850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1850-1850)
  on line 1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1855-1855)
  on line 1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1861-1861)
  on line 1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1866-1866)
  on line 1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1872-1872)
  on line 1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1877-1877)
  on line 1882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1882-1882)
  on line 1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1887-1887)
  on line 1894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1894-1894)
  on line 1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1911-1911)
  on line 1927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1927-1927)
  on line 1935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1935-1935)
  on line 1952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1952-1952)
  on line 1968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1968-1968)
  on line 1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1976-1976)
  on line 1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1993-1993)
  on line 2009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:2009-2009)
  on line 2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:2016-2016)
  on line 2021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:2021-2021)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 588
  dead: 88 (2 in uncalled functions)
  total lines: 676
[Warning][Deadcode][CWE-571] condition '(int )r2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:748:7-748:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:568:6-568:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:570:6-570:22)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:394:6-394: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:756:6-756:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:578:6-578:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:584:7-584:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:402:6-402: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:405:6-405:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:589:6-589:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:591:6-591:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1193:6-1193:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1195:6-1195:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:600:6-600:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:602:6-602:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1204:6-1204:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:775:7-775:20)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1206:6-1206: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:231:6-231:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:610:6-610:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:616:7-616:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:424:7-424: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:621:6-621:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:623:6-623: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:432:6-432:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:632:6-632:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:634:6-634: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:246:6-246:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:249:6-249:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:255:7-255:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:804:7-804:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:260:6-260:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:806:7-806:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:262:6-262:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:814:7-814:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:817:7-817:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:451:7-451:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1294:6-1294:19)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:271:6-271:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1296:6-1296: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_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:273:6-273: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:459:6-459:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:655:9-655:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:657:8-657:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:659:8-659: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1305:6-1305: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:661:8-661:36)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:281:6-281:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1307:6-1307:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:663:7-663:20)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:287:7-287:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:669:9-669:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:671:7-671:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:292:6-292:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:673:7-673:20)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:294:6-294:22)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:679:9-679:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:681:7-681:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:303:6-303:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:478:7-478:20)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:305:6-305: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_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:691:6-691: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:699:6-699:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:313:6-313:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:702:6-702:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:319:7-319:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:324:6-324:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:326:6-326:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:499:9-499:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:501:8-501:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:503:8-503:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:505:8-505:36)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:335:6-335:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:507:7-507:20)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:337:6-337:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:513:9-513:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:515:7-515:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:517:7-517:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:523:9-523:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:721:7-721:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:525:7-525:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1092:6-1092:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1094:6-1094: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:729:6-729: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.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:535:6-535:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1103:6-1103:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:543:6-543:18)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:358:9-358:51)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1105:6-1105:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:546:6-546:19)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:360:8-360:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:362:8-362:36)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:552:7-552:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:364:8-364:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:366:7-366:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:557:6-557:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:559:6-559:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:372:9-372:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:374:7-374:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:376:7-376:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:382:9-382:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.3.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:384:7-384: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)
