./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.2.ufo.UNBOUNDED.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.2.ufo.UNBOUNDED.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.2.ufo.UNBOUNDED.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, init__r121, init__r131, init__r211, init__r231, init__r311, init__r321, main__i2, 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] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:404:2-404:13)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:246-246)
  on line 278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:278-278)
  on line 310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:310-310)
  on line 363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:363-363)
  on line 373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:373-373)
  on line 391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:391-391)
  on line 400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:400-400)
  on line 433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:433-433)
  on line 456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:456-456)
  on line 466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:466-466)
  on line 489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:489-489)
  on line 518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:518-518)
  on line 528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:528-528)
  on line 551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:551-551)
  on line 556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:556-556)
  on line 558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:558-558)
  on line 560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:560-560)
  on lines 562..563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:562-563)
  on lines 565..567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:565-567)
  on line 569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:569-569)
  on line 571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:571-571)
  on lines 573..575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:573-575)
  on line 577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:577-577)
  on line 579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:579-579)
  on line 581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:581-581)
  on line 583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:583-583)
  on line 585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:585-585)
  on line 588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:588-588)
  on line 590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:590-590)
  on line 592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:592-592)
  on lines 594..595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:594-595)
  on lines 597..599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:597-599)
  on line 601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:601-601)
  on line 603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:603-603)
  on lines 605..607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:605-607)
  on line 609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:609-609)
  on line 611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:611-611)
  on line 613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:613-613)
  on line 615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:615-615)
  on line 617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:617-617)
  on line 620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:620-620)
  on line 622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:622-622)
  on line 624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:624-624)
  on lines 626..627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:626-627)
  on lines 629..631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:629-631)
  on line 633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:633-633)
  on line 635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:635-635)
  on lines 637..639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:637-639)
  on line 641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:641-641)
  on line 643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:643-643)
  on line 645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:645-645)
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:647-647)
  on line 649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:649-649)
  on lines 651..662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:651-662)
  on line 665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:665-665)
  on line 667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:667-667)
  on line 669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:669-669)
  on line 671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:671-671)
  on line 673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:673-673)
  on line 676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:676-676)
  on line 679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:679-679)
  on line 682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:682-682)
  on line 684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:684-684)
  on lines 693..694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:693-694)
  on line 699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:699-699)
  on line 701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:701-701)
  on line 706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:706-706)
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:713-713)
  on line 719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:719-719)
  on line 726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:726-726)
  on line 732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:732-732)
  on line 739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:739-739)
  on line 745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:745-745)
  on line 752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:752-752)
  on line 758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:758-758)
  on line 764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:764-764)
  on line 770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:770-770)
  on line 777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:777-777)
  on line 813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:813-813)
  on line 815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:815-815)
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:818-818)
  on line 820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:820-820)
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:822-822)
  on line 824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:824-824)
  on line 826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:826-826)
  on line 829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:829-829)
  on line 831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:831-831)
  on line 833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:833-833)
  on line 835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:835-835)
  on line 837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:837-837)
  on line 843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:843-843)
  on line 860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:860-860)
  on line 883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:883-883)
  on line 919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:919-919)
  on line 921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:921-921)
  on line 924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:924-924)
  on line 926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:926-926)
  on line 928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:928-928)
  on line 930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:930-930)
  on line 932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:932-932)
  on line 935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:935-935)
  on line 937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:937-937)
  on line 939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:939-939)
  on line 941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:941-941)
  on line 943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:943-943)
  on line 949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:949-949)
  on line 966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:966-966)
  on line 989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:989-989)
  on line 1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1025-1025)
  on line 1027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1027-1027)
  on line 1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1030-1030)
  on line 1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1032-1032)
  on line 1034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1034-1034)
  on line 1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1036-1036)
  on line 1038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1038-1038)
  on line 1041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1041-1041)
  on line 1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1043-1043)
  on line 1045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1045-1045)
  on line 1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1047-1047)
  on line 1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1049-1049)
  on line 1055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1055-1055)
  on line 1072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1072-1072)
  on line 1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1099-1099)
  on line 1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1111-1111)
  on line 1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1116-1116)
  on line 1126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1126-1126)
  on line 1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1154-1154)
  on line 1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1182-1182)
  on line 1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1194-1194)
  on line 1220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1220-1220)
  on line 1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1228-1228)
  on line 1233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1233-1233)
  on line 1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1239-1239)
  on line 1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1244-1244)
  on line 1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1250-1250)
  on line 1255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1255-1255)
  on line 1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1260-1260)
  on line 1265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1265-1265)
  on line 1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1272-1272)
  on line 1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1289-1289)
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1305-1305)
  on line 1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1313-1313)
  on line 1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1330-1330)
  on line 1346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1346-1346)
  on line 1354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1354-1354)
  on line 1371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1371-1371)
  on line 1387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1387-1387)
  on line 1394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1394-1394)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 304
  dead: 177 (2 in uncalled functions)
  total lines: 481
[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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:389:6-389:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:396:6-396:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:398:6-398:15)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:421:7-421:20)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:228:6-228:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:429:6-429:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:431:6-431:15)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:244:6-244: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:250:7-250: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:255:6-255: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:257:6-257:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:454:7-454: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:266:6-266: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:268:6-268: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:462:6-462:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:464:6-464:15)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:276:6-276: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:282:7-282: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:287:6-287: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:289:6-289: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:298:6-298: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:300:6-300:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:487:7-487:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:308:6-308: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:314:7-314: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:319:6-319: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:321:6-321: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:330:6-330: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:508:9-508: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:332:6-332:22)
[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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:512:8-512: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:514:8-514: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:516:7-516: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:524:7-524: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:526:7-526:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:353:9-353:51)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___0 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:548:6-548:22)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:355:8-355: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:357:8-357: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:359:8-359: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:361:7-361:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:367:9-367: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:369:7-369: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:371:7-371: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:377:9-377: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.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:379:7-379: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)
