./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_opt-floodmax.4.2.ufo.BOUNDED-8.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_opt-floodmax.4.2.ufo.BOUNDED-8.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] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:494-494)
  on line 545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:545-545)
  on line 596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:596-596)
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:647-647)
  on line 731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:731-731)
  on line 741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:741-741)
  on line 759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:759-759)
  on line 803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:803-803)
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:844-844)
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:885-885)
  on line 926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:926-926)
  on line 969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:969-969)
  on line 979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:979-979)
  on line 997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:997-997)
  on line 1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1010-1010)
  on line 1061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1061-1061)
  on line 1112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1112-1112)
  on line 1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1163-1163)
  on line 1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1247-1247)
  on line 1257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1257-1257)
  on line 1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1275-1275)
  on line 1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1360-1360)
  on line 1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1401-1401)
  on line 1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1442-1442)
  on line 1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1485-1485)
  on line 1495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1495-1495)
  on line 1520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1520-1520)
  on lines 1524..1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1524-1526)
  on lines 1530..1531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1530-1531)
  on lines 1533..1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1533-1534)
  on lines 1536..1538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1536-1538)
  on lines 1540..1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1540-1541)
  on line 1543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1543-1543)
  on lines 1545..1547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1545-1547)
  on lines 1549..1550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1549-1550)
  on line 1552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1552-1552)
  on lines 1554..1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1554-1556)
  on lines 1558..1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1558-1559)
  on lines 1561..1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1561-1562)
  on line 1564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1564-1564)
  on line 1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1566-1566)
  on line 1568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1568-1568)
  on lines 1572..1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1572-1573)
  on lines 1575..1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1575-1576)
  on lines 1578..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1578-1580)
  on lines 1582..1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1582-1583)
  on line 1585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1585-1585)
  on lines 1587..1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1587-1589)
  on lines 1591..1592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1591-1592)
  on line 1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1594-1594)
  on lines 1596..1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1596-1598)
  on lines 1600..1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1600-1601)
  on lines 1603..1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1603-1604)
  on line 1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1606-1606)
  on line 1608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1608-1608)
  on line 1610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1610-1610)
  on lines 1614..1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1614-1615)
  on lines 1617..1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1617-1618)
  on lines 1620..1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1620-1622)
  on lines 1624..1625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1624-1625)
  on line 1627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1627-1627)
  on lines 1629..1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1629-1631)
  on lines 1633..1634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1633-1634)
  on line 1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1636-1636)
  on lines 1638..1640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1638-1640)
  on lines 1642..1643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1642-1643)
  on lines 1645..1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1645-1646)
  on line 1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1648-1648)
  on line 1650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1650-1650)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1652-1652)
  on lines 1656..1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1656-1657)
  on lines 1659..1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1659-1660)
  on lines 1662..1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1662-1664)
  on lines 1666..1667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1666-1667)
  on line 1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1669-1669)
  on lines 1671..1673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1671-1673)
  on lines 1675..1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1675-1676)
  on line 1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1678-1678)
  on lines 1680..1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1680-1682)
  on lines 1684..1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1684-1685)
  on lines 1687..1688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1687-1688)
  on line 1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1690-1690)
  on line 1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1692-1692)
  on line 1694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1694-1694)
  on lines 1696..1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1696-1719)
  on line 1722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1722-1722)
  on line 1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1724-1724)
  on line 1726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1726-1726)
  on line 1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1728-1728)
  on line 1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1730-1730)
  on line 1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1732-1732)
  on line 1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1735-1735)
  on line 1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1738-1738)
  on line 1741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1741-1741)
  on line 1743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1743-1743)
  on lines 1753..1755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1753-1755)
  on line 1760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1760-1760)
  on line 1762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1762-1762)
  on line 1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1767-1767)
  on line 1774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1774-1774)
  on line 1780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1780-1780)
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1787-1787)
  on line 1793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1793-1793)
  on line 1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1800-1800)
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1806-1806)
  on line 1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1813-1813)
  on line 1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1819-1819)
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1825-1825)
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1831-1831)
  on line 1837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1837-1837)
  on line 1844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1844-1844)
  on line 1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1885-1885)
  on line 1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1887-1887)
  on line 1889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1889-1889)
  on line 1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1892-1892)
  on line 1894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1894-1894)
  on line 1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1896-1896)
  on line 1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1898-1898)
  on line 1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1900-1900)
  on line 1902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1902-1902)
  on line 1905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1905-1905)
  on line 1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1907-1907)
  on line 1909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1909-1909)
  on line 1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1911-1911)
  on line 1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1913-1913)
  on line 1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1915-1915)
  on line 1918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1918-1918)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1920-1920)
  on line 1922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1922-1922)
  on line 1924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1924-1924)
  on line 1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1926-1926)
  on line 1932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1932-1932)
  on line 1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1954-1954)
  on line 1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1976-1976)
  on line 2004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2004-2004)
  on line 2045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2045-2045)
  on line 2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2047-2047)
  on line 2049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2049-2049)
  on line 2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2052-2052)
  on line 2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2054-2054)
  on line 2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2056-2056)
  on line 2058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2058-2058)
  on line 2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2060-2060)
  on line 2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2062-2062)
  on line 2065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2065-2065)
  on line 2067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2067-2067)
  on line 2069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2069-2069)
  on line 2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2071-2071)
  on line 2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2073-2073)
  on line 2075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2075-2075)
  on line 2078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2078-2078)
  on line 2080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2080-2080)
  on line 2082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2082-2082)
  on line 2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2084-2084)
  on line 2086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2086-2086)
  on line 2092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2092-2092)
  on line 2114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2114-2114)
  on line 2136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2136-2136)
  on line 2164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2164-2164)
  on line 2205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2205-2205)
  on line 2207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2207-2207)
  on line 2209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2209-2209)
  on line 2212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2212-2212)
  on line 2214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2214-2214)
  on line 2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2216-2216)
  on line 2218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2218-2218)
  on line 2220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2220-2220)
  on line 2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2222-2222)
  on line 2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2225-2225)
  on line 2227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2227-2227)
  on line 2229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2229-2229)
  on line 2231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2231-2231)
  on line 2233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2233-2233)
  on line 2235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2235-2235)
  on line 2238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2238-2238)
  on line 2240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2240-2240)
  on line 2242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2242-2242)
  on line 2244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2244-2244)
  on line 2246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2246-2246)
  on line 2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2252-2252)
  on line 2274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2274-2274)
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2296-2296)
  on line 2324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2324-2324)
  on line 2365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2365-2365)
  on line 2367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2367-2367)
  on line 2369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2369-2369)
  on line 2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2372-2372)
  on line 2374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2374-2374)
  on line 2376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2376-2376)
  on line 2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2378-2378)
  on line 2380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2380-2380)
  on line 2382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2382-2382)
  on line 2385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2385-2385)
  on line 2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2387-2387)
  on line 2389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2389-2389)
  on line 2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2391-2391)
  on line 2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2393-2393)
  on line 2395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2395-2395)
  on line 2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2398-2398)
  on line 2400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2400-2400)
  on line 2402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2402-2402)
  on line 2404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2404-2404)
  on line 2406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2406-2406)
  on line 2412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2412-2412)
  on line 2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2434-2434)
  on line 2456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2456-2456)
  on lines 2484..2485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2484-2485)
  on line 2494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2494-2494)
  on line 2506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2506-2506)
  on line 2511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2511-2511)
  on line 2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2516-2516)
  on line 2526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2526-2526)
  on line 2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2563-2563)
  on line 2600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2600-2600)
  on line 2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2637-2637)
  on line 2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2649-2649)
  on line 2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2684-2684)
  on line 2690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2690-2690)
  on line 2697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2697-2697)
  on line 2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2702-2702)
  on line 2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2708-2708)
  on line 2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2713-2713)
  on line 2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2719-2719)
  on line 2724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2724-2724)
  on line 2729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2729-2729)
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2734-2734)
  on line 2739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2739-2739)
  on line 2746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2746-2746)
  on line 2768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2768-2768)
  on line 2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2790-2790)
  on line 2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2811-2811)
  on line 2819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2819-2819)
  on line 2841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2841-2841)
  on line 2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2863-2863)
  on line 2884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2884-2884)
  on line 2892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2892-2892)
  on line 2914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2914-2914)
  on line 2936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2936-2936)
  on line 2957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2957-2957)
  on line 2965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2965-2965)
  on line 2987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2987-2987)
  on line 3009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3009-3009)
  on line 3030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3030-3030)
  on line 3037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3037-3037)
  on line 3044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3044-3044)
  on line 3049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3049-3049)
  on line 3055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3055-3055)
  on line 3060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3060-3060)
  on line 3066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3066-3066)
  on line 3071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3071-3071)
  on line 3076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3076-3076)
  on line 3081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3081-3081)
  on line 3086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3086-3086)
  on line 3123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3123-3123)
  on line 3160 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3160-3160)
  on line 3197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3197-3197)
  on line 3234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3234-3234)
  on line 3240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3240-3240)
  on line 3247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3247-3247)
  on line 3252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3252-3252)
  on line 3258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3258-3258)
  on line 3263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3263-3263)
  on line 3269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3269-3269)
  on line 3274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3274-3274)
  on line 3279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3279-3279)
  on line 3284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3284-3284)
  on line 3289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3289-3289)
  on line 3296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3296-3296)
  on line 3318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3318-3318)
  on line 3340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3340-3340)
  on line 3361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3361-3361)
  on line 3369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3369-3369)
  on line 3391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3391-3391)
  on line 3413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3413-3413)
  on line 3434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3434-3434)
  on line 3442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3442-3442)
  on line 3464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3464-3464)
  on line 3486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3486-3486)
  on line 3507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3507-3507)
  on line 3515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3515-3515)
  on line 3537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3537-3537)
  on line 3559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3559-3559)
  on line 3580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3580-3580)
  on line 3587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3587-3587)
  on line 3592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3592-3592)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 996
  dead: 363 (2 in uncalled functions)
  total lines: 1359
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1136:6-1136:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1138:6-1138:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1149:6-1149:19)
[Warning][Deadcode][CWE-571] condition '(int )p34_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1151:6-1151:22)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1473:10-1473:66)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:801:7-801:20)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1477:8-1477:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1479:8-1479:36)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1481:8-1481:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1483:7-1483:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1161:6-1161:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:811:6-811:19)
[Warning][Deadcode][CWE-571] condition '(int )r4 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1167:7-1167:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1491:7-1491:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1493:7-1493:20)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1174:6-1174:19)
[Warning][Deadcode][CWE-571] condition '(int )p41_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1176:6-1176:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:460:6-460:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1187:6-1187:19)
[Warning][Deadcode][CWE-571] condition '(int )p42_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1189:6-1189:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___2 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1517:6-1517:22)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1200:6-1200:19)
[Warning][Deadcode][CWE-571] condition '(int )p43_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1202:6-1202:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:842:7-842:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:852:6-852:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:487:6-487:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:492:6-492:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:498:7-498:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:502:6-502:21)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:505:6-505:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:507:6-507:22)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1235:10-1235:66)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1237:8-1237:36)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:515:6-515:21)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1239:8-1239:36)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:518:6-518:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1241:8-1241:36)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:520:6-520:22)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1243:8-1243:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1245:7-1245:20)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1251:10-1251:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1253:7-1253:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1255:7-1255:20)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:528:6-528:21)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1261:10-1261:66)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:531:6-531:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1263:7-1263:19)
[Warning][Deadcode][CWE-571] condition '(int )p14_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:533:6-533:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:883:7-883:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:893:6-893: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1273:6-1273:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:543:6-543:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:549:7-549:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1281:6-1281:18)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:553:6-553:21)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:556:6-556:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:558:6-558:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1286:6-1286:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:566:6-566:21)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:569:6-569:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:571:6-571:22)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:579:6-579:21)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:582:6-582:19)
[Warning][Deadcode][CWE-571] condition '(int )p24_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:584:6-584:22)
[Warning][Deadcode][CWE-570] condition '(int )r4 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:924:7-924:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:594:6-594:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:600:7-600:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:604:6-604:21)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:607:6-607:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1317:7-1317:20)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:609:6-609:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1327:6-1327:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:617:6-617:21)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:620:6-620:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:622:6-622:22)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:630:6-630:21)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:633:6-633:19)
[Warning][Deadcode][CWE-571] condition '(int )p34_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:635:6-635:22)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:957:10-957:66)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:959:8-959:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:961:8-961:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:963:8-963:36)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:965:8-965:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:967:7-967:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:645:6-645:19)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:973:10-973:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:975:7-975:19)
[Warning][Deadcode][CWE-571] condition '(int )r4 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:651:7-651:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:977:7-977:20)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:655:6-655:21)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:983:10-983:66)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:658:6-658:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:985:7-985:19)
[Warning][Deadcode][CWE-571] condition '(int )p41_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:660:6-660:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1358:7-1358:20)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:995:6-995:22)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:668:6-668:21)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:671:6-671:19)
[Warning][Deadcode][CWE-571] condition '(int )p42_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:673:6-673:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1368:6-1368:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1003:6-1003:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1008:6-1008:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:681:6-681:21)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1014:7-1014:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:684:6-684:19)
[Warning][Deadcode][CWE-571] condition '(int )p43_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:686:6-686:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1021:6-1021:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1023:6-1023:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1034:6-1034:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1036:6-1036:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1047:6-1047:19)
[Warning][Deadcode][CWE-571] condition '(int )p14_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1049:6-1049:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1399:7-1399:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1409:6-1409:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1059:6-1059:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1065:7-1065:19)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:719:10-719:66)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:721:8-721:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:723:8-723:36)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1072:6-1072:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:725:8-725:36)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1074:6-1074:22)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:727:8-727:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:729:7-729:20)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:735:10-735:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:737:7-737:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:739:7-739:20)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:745:10-745:66)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1085:6-1085:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:747:7-747:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1087:6-1087:22)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:757:6-757:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1098:6-1098:19)
[Warning][Deadcode][CWE-571] condition '(int )p24_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1100:6-1100:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:765:6-765:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:770:6-770:19)
[Warning][Deadcode][CWE-570] condition '(int )r4 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1440:7-1440:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1110:6-1110:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1116:7-1116:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1123:6-1123:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1125:6-1125:22)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
