./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.5.1.ufo.BOUNDED-10.pals.c.p+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_lcr.5.1.ufo.BOUNDED-10.pals.c.p+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_lcr.5.1.ufo.BOUNDED-10.pals.c.p+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, id1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, main__i2, node1__m1, node1__m1___0, node1__m1___1, node2__m2, node3__m3, node4__m4, node5__m5, 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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:221:2-221:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:337:2-337:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:456:2-456:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:226-226)
  on line 228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:228-228)
  on line 241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:241-241)
  on line 243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:243-243)
  on line 256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:256-256)
  on line 258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:258-258)
  on line 271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:271-271)
  on line 273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:273-273)
  on line 286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:286-286)
  on line 288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:288-288)
  on line 560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:560-560)
  on line 1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1101-1101)
  on line 1142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1142-1142)
  on line 1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1144-1144)
  on line 1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1187-1187)
  on line 1189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1189-1189)
  on line 1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1232-1232)
  on line 1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1234-1234)
  on line 1277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1277-1277)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1279-1279)
  on line 1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1322-1322)
  on line 1324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1324-1324)
  on line 1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1329-1329)
  on line 1368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1368-1368)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 421
  dead: 26 (2 in uncalled functions)
  total lines: 447
[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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:763:6-763:21)
[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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1077:6-1077:21)
[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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:809:6-809:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:214:6-214:19)
[Warning][Deadcode][CWE-570] condition '(int )node1__m1 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:224:7-224:38)
[Warning][Deadcode][CWE-571] condition '(int )p5_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1163:6-1163:21)
[Warning][Deadcode][CWE-570] condition '(int )node2__m2 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:239:7-239:38)
[Warning][Deadcode][CWE-571] condition '(int )p4_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1208:6-1208:21)
[Warning][Deadcode][CWE-571] condition '(int )p5_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:896:6-896:21)
[Warning][Deadcode][CWE-570] condition '(int )node3__m3 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:254:7-254:38)
[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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1253:6-1253:21)
[Warning][Deadcode][CWE-570] condition '(int )node4__m4 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:269:7-269:38)
[Warning][Deadcode][CWE-571] condition '(int )p4_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:941:6-941:21)
[Warning][Deadcode][CWE-571] condition '(int )p5_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:628:6-628:21)
[Warning][Deadcode][CWE-570] condition '(int )node5__m5 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:284:7-284:38)
[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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1298:6-1298: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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:986:6-986:21)
[Warning][Deadcode][CWE-571] condition '(int )p4_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:673:6-673: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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:718:6-718:21)
[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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1344:6-1344: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.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:1031:6-1031:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 10' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.BOUNDED-10.pals.c.p+lhb-reducer.c:330:6-330: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)
