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


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] nomsg, id1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, main__i2, node1__m1___0, node1__m1___1, node1__m1___2, node2__m2___0, node3__m3___0, node2__m2___1, node3__m3___1, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:411:2-411:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:142-142)
  on line 163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:163-163)
  on line 184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:184-184)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:222-222)
  on line 304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:304-304)
  on lines 317..320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:317-320)
  on line 322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:322-322)
  on line 324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:324-324)
  on line 326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:326-326)
  on line 329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:329-329)
  on line 398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:398-398)
  on line 472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:472-472)
  on line 498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:498-498)
  on line 587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:587-587)
  on line 613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:613-613)
  on line 673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:673-673)
  on line 699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:699-699)
  on line 718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:718-718)
  on line 720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:720-720)
  on line 725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:725-725)
  on line 732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:732-732)
  on line 760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:760-760)
  on line 786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:786-786)
  on line 805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:805-805)
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:812-812)
  on line 851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:851-851)
  on line 881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:881-881)
  on line 912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:912-912)
  on line 918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:918-918)
  on line 925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:925-925)
  on line 930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:930-930)
  on line 936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:936-936)
  on line 941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:941-941)
  on line 961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:961-961)
  on line 966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:966-966)
  on line 980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:980-980)
  on line 985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:985-985)
  on line 1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1005-1005)
  on line 1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1010-1010)
  on line 1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1024-1024)
  on line 1029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1029-1029)
  on line 1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1049-1049)
  on line 1054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1054-1054)
  on line 1068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1068-1068)
  on line 1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1073-1073)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 295
  dead: 50 (2 in uncalled functions)
  total lines: 345
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:182:6-182:19)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:601:6-601:20)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:191:6-191:20)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:603:6-603:21)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:193:6-193:21)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:950:6-950:20)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:952:6-952:21)
[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_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:208:9-208:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:210:7-210:19)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:659:6-659:20)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:220:6-220:22)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:994:6-994:20)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:661:6-661:21)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:996:6-996:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:228:6-228:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:233:6-233:19)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:687:6-687:20)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:689:6-689:21)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1038:6-1038:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1040:6-1040:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:251:6-251:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:268:6-268:19)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:746:6-746:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:748:6-748:21)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:458:6-458:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:460:6-460:21)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:774:6-774:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:776:6-776:21)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:292:7-292:19)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:486:6-486:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:488:6-488:21)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:302:6-302:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:310:6-310:18)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:126:6-126:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:315:6-315:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:135:6-135:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:140:6-140:19)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:149:6-149:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:151:6-151:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:161:6-161:19)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:573:6-573:20)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:575:6-575:21)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:170:6-170:20)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:172:6-172:21)
[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)
