./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.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 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:3-608:3 with factor 10
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] nomsg, side1_written, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, arg, i2, tmp___5, tmp___9, tmp___14, tmp___15, tmp___16, tmp___17, tmp___18, tmp___19, side1, side2, active_side, tmp, next_state, side2, side1, manual_selection, next_state, side1, side2, manual_selection, manual_selection, tmp, side, index, val, index, val, index, val, index, val, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Deadcode] Function 'read_active_side_history' has dead code:
  on lines 157..158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:157-158)
[Warning][Deadcode] Function 'read_manual_selection_history' has dead code:
  on line 179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:179-179)
  on lines 187..188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:187-188)
[Warning][Deadcode] Function 'read_side1_failed_history' has dead code:
  on lines 97..98 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:97-98)
[Warning][Deadcode] Function 'read_side2_failed_history' has dead code:
  on lines 127..128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:127-128)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 312
  dead: 9
  total lines: 321
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:336:5-336:70)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:337:5-337:67)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-571] condition '(int )cs1_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:258:3-258:87)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-571] condition '(int )cs2_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:259:3-259:87)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:278:5-278:70)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-571] condition '(int )s2s1_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:371:3-371:78)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:279:5-279:70)
[Warning][Deadcode][CWE-571] condition '(int )s2s2_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:372:3-372:78)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:280:5-280:67)
[Warning][Deadcode][CWE-571] condition '(int )s2p_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:373:3-373:75)
[Warning][Deadcode][CWE-571] condition '(int )index == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:94:7-94:23)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-571] condition '(int )index == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:124:7-124:23)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-571] condition '(int )s1s1_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:314:3-314:78)
[Warning][Deadcode][CWE-571] condition '(int )index == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:154:7-154:23)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-571] condition '(int )s1s2_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:315:3-315:78)
[Warning][Deadcode][CWE-570] condition '(int )index == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:178:7-178:23)
[Warning][Deadcode][CWE-571] condition '(int )s1p_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:316:3-316:75)
[Warning][Deadcode][CWE-571] condition '(int )index == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:184:7-184:23)
[Warning][Deadcode][CWE-570] condition 'i2 < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:582:10-582:17)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.ufo.BOUNDED-10.pals.c:335:5-335:70)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
