./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+lhb-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] nomsg, r1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, init__r121, init__r131, init__r211, init__r231, init__r311, init__r321, main__i2, init__r122, cond
[Info] 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+lhb-reducer.c:405:2-405: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+lhb-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:247-247)
  on line 279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:279-279)
  on line 311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:311-311)
  on line 364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:364-364)
  on line 374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:374-374)
  on line 392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:392-392)
  on line 401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:401-401)
  on line 433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-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+lhb-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+lhb-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+lhb-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+lhb-reducer.c:518-518)
  on line 524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:524-524)
  on line 539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:539-539)
  on line 543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:543-543)
  on line 551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-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+lhb-reducer.c:556-556)
  on line 561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:561-561)
  on line 566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:566-566)
  on line 594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:594-594)
  on line 622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:622-622)
  on line 635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:635-635)
  on line 658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:658-658)
  on line 668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:668-668)
  on line 691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:691-691)
  on line 720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:720-720)
  on line 730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:730-730)
  on line 736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:736-736)
  on line 752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:752-752)
  on line 757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:757-757)
  on line 759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:759-759)
  on line 761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:761-761)
  on lines 763..764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:763-764)
  on lines 766..768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:766-768)
  on line 770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:770-770)
  on line 772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:772-772)
  on lines 774..776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:774-776)
  on line 778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:778-778)
  on line 780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:780-780)
  on line 782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:782-782)
  on line 784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:784-784)
  on line 786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:786-786)
  on line 789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:789-789)
  on line 791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:791-791)
  on line 793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:793-793)
  on lines 795..796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:795-796)
  on lines 798..800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:798-800)
  on line 802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:802-802)
  on line 804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:804-804)
  on lines 806..808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:806-808)
  on line 810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:810-810)
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:812-812)
  on line 814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:814-814)
  on line 816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:816-816)
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:818-818)
  on line 821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:821-821)
  on line 823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:823-823)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:825-825)
  on lines 827..828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:827-828)
  on lines 830..832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:830-832)
  on line 834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:834-834)
  on line 836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:836-836)
  on lines 838..840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:838-840)
  on line 842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:842-842)
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:844-844)
  on line 846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:846-846)
  on line 848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:848-848)
  on line 850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:850-850)
  on lines 852..863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:852-863)
  on line 866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:866-866)
  on line 868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:868-868)
  on line 870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:870-870)
  on line 872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:872-872)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:874-874)
  on line 877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:877-877)
  on line 880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:880-880)
  on line 883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:883-883)
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:885-885)
  on lines 894..895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:894-895)
  on line 900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:900-900)
  on line 902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:902-902)
  on line 907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:907-907)
  on line 914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:914-914)
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:920-920)
  on line 927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:927-927)
  on line 933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:933-933)
  on line 940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:940-940)
  on line 946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:946-946)
  on line 953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:953-953)
  on line 959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:959-959)
  on line 965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:965-965)
  on line 971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:971-971)
  on line 978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:978-978)
  on line 1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1014-1014)
  on line 1016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1016-1016)
  on line 1019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1019-1019)
  on line 1021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1021-1021)
  on line 1023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1023-1023)
  on line 1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-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+lhb-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+lhb-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+lhb-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+lhb-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+lhb-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+lhb-reducer.c:1038-1038)
  on line 1044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1044-1044)
  on line 1061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1061-1061)
  on line 1084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1084-1084)
  on line 1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1120-1120)
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1122-1122)
  on line 1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1125-1125)
  on line 1127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1127-1127)
  on line 1129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1129-1129)
  on line 1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1131-1131)
  on line 1133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1133-1133)
  on line 1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1136-1136)
  on line 1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1138-1138)
  on line 1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1140-1140)
  on line 1142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1142-1142)
  on line 1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1144-1144)
  on line 1150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1150-1150)
  on line 1167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1167-1167)
  on line 1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1190-1190)
  on line 1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1226-1226)
  on line 1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1228-1228)
  on line 1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1231-1231)
  on line 1233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1233-1233)
  on line 1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1235-1235)
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1237-1237)
  on line 1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1239-1239)
  on line 1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1242-1242)
  on line 1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1244-1244)
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1246-1246)
  on line 1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1248-1248)
  on line 1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1250-1250)
  on line 1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1256-1256)
  on line 1273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1273-1273)
  on line 1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1300-1300)
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1305-1305)
  on line 1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1311-1311)
  on line 1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1316-1316)
  on line 1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1321-1321)
  on line 1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1326-1326)
  on line 1354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1354-1354)
  on line 1382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1382-1382)
  on line 1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1389-1389)
  on line 1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1415-1415)
  on line 1423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1423-1423)
  on line 1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1428-1428)
  on line 1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1434-1434)
  on line 1439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1439-1439)
  on line 1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1445-1445)
  on line 1450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1450-1450)
  on line 1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1455-1455)
  on line 1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1460-1460)
  on line 1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1467-1467)
  on line 1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1484-1484)
  on line 1500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1500-1500)
  on line 1508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1508-1508)
  on line 1525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1525-1525)
  on line 1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1541-1541)
  on line 1549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1549-1549)
  on line 1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1566-1566)
  on line 1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1582-1582)
  on line 1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:1589-1589)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 357
  dead: 194 (2 in uncalled functions)
  total lines: 551
[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+lhb-reducer.c:631:6-631: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+lhb-reducer.c:633:6-633:15)
[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+lhb-reducer.c:390:6-390: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+lhb-reducer.c:397:6-397: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+lhb-reducer.c:399:6-399:15)
[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+lhb-reducer.c:656:7-656:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:664:6-664:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:422:7-422: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+lhb-reducer.c:229:6-229: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+lhb-reducer.c:666:6-666:15)
[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+lhb-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+lhb-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+lhb-reducer.c:245:6-245: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+lhb-reducer.c:251:7-251: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+lhb-reducer.c:256:6-256: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+lhb-reducer.c:258:6-258: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+lhb-reducer.c:689:7-689:20)
[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+lhb-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+lhb-reducer.c:267:6-267: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+lhb-reducer.c:269:6-269: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+lhb-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+lhb-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+lhb-reducer.c:277:6-277: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+lhb-reducer.c:710:9-710:51)
[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+lhb-reducer.c:283:7-283:19)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:712:8-712: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+lhb-reducer.c:714:8-714:36)
[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+lhb-reducer.c:288:6-288:19)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:716:8-716: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_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:290:6-290:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:718:7-718: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+lhb-reducer.c:724:9-724: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+lhb-reducer.c:726:7-726: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+lhb-reducer.c:728:7-728:20)
[Warning][Deadcode][CWE-570] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:734:9-734:51)
[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+lhb-reducer.c:299:6-299: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+lhb-reducer.c:301:6-301: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+lhb-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+lhb-reducer.c:309:6-309:19)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___1 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:749:6-749:22)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:315:7-315: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+lhb-reducer.c:320:6-320: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+lhb-reducer.c:322:6-322:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:508:9-508:51)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:331:6-331:19)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:510:8-510:36)
[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+lhb-reducer.c:333:6-333: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+lhb-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+lhb-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+lhb-reducer.c:516:7-516:20)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:522:9-522: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+lhb-reducer.c:536:6-536:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:354:9-354:51)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+lhb-reducer.c:356:8-356: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+lhb-reducer.c:358:8-358: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+lhb-reducer.c:360:8-360: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+lhb-reducer.c:362:7-362: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+lhb-reducer.c:368:9-368: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+lhb-reducer.c:370:7-370: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+lhb-reducer.c:372:7-372: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+lhb-reducer.c:378:9-378: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+lhb-reducer.c:380:7-380: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)
