./goblint --conf conf/svcomp.json --set ana.malloc.unique_address_count 1 --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_Triplicated.1.ufo.UNBOUNDED.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_Triplicated.1.ufo.UNBOUNDED.pals.c:74:3-100:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:511:3-526:3 with factor 1
[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] Setting "ana.int.interval" to true
[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, VALUE1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, arg, i2, voted_value, next_state, tmp, next_state, tmp, next_state, tmp, temp_count, tmp___0, tmp___1, tmp___2, tmp___6, tmp___10, tmp___11, tmp___12, tmp, tmp___0, tmp___1, tmp___2, history_id, buf, history_id, buf, historyIndex, history_id, historyIndex, history_id, history_id, ini_bool, var, tmp, tmp___0, tmp___1, tmp___2, ini_int, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:528-528)
[Warning][Deadcode] Function 'read_history_bool' has dead code:
  on line 136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:136-136)
  on line 146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:146-146)
  on line 156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:156-156)
  on line 159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:159-159)
  on line 161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:161-161)
[Warning][Deadcode] Function 'read_history_int8' has dead code:
  on line 116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:116-116)
  on line 119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:119-119)
  on line 121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:121-121)
[Warning][Deadcode] Function 'write_history_bool' has dead code:
  on line 199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:199-199)
[Warning][Deadcode] Function 'write_history_int8' has dead code:
  on line 174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:174-174)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 268
  dead: 11
  total lines: 279
[Warning][Deadcode][CWE-571] condition 'history_id == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:109:7-109:22)
[Warning][Deadcode][CWE-571] condition 'historyIndex == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:113:9-113:26)
[Warning][Deadcode][CWE-571] condition 'historyIndex == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:133:9-133:26)
[Warning][Deadcode][CWE-571] condition 'historyIndex == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:143:9-143:26)
[Warning][Deadcode][CWE-571] condition 'history_id == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:149:7-149:22)
[Warning][Deadcode][CWE-571] condition 'historyIndex == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:153:9-153:26)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:349:5-349:67)
[Warning][Deadcode][CWE-571] condition 'history_id == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:169:7-169:22)
[Warning][Deadcode][CWE-571] condition 'history_id == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:194:7-194:22)
[Warning][Deadcode][CWE-571] condition '(int )g1v_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:366:3-366:75)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:380:5-380:67)
[Warning][Deadcode][CWE-571] condition 'var < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:74:10-74:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:511:10-511:11)
[Warning][Deadcode][CWE-571] condition 'history_id == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:93:9-93:24)
[Warning][Deadcode][CWE-571] condition '(int )g2v_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:397:3-397:75)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:511:10-511:11)
[Warning][Deadcode][CWE-570] condition '(int )nomsg != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:411:5-411:67)
[Warning][Deadcode][CWE-571] condition 'history_id == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:93:9-93:24)
[Warning][Deadcode][CWE-571] condition '(int )g3v_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.c:428:3-428:75)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
