./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-pthread/cs_time_var_mutex.i


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


[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-pthread/cs_time_var_mutex.i:604:2-607:2 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:612:2-615:2 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:4-796:4 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:787:2-797:2 with factor 3
[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] __CS_ret, __CS_thread_lockedon, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, j, i, __CS_cp___CS_thread_status, __CS_cp___CS_thread_lockedon, __CS_cp_block, __CS_cp_busy, __CS_cp_inode, __CS_cp_m_inode, t1, tmp, t2, tmp___0, id1, t1, thread, expr, expr, lock, cond, j, cond, j, cond, lock, lock, lock, k, tmp, tmp___1, cond, __x, __x, __x, cond
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:835:3-835:20)
[Warning][Unsound][Call][CWE-685] Potential call to function de_allocator with wrong number of arguments (expected: 0, actual: 1). This call will be ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:835:3-835:20)
[Warning][Unsound][Call][CWE-685] Potential call to function allocator with wrong number of arguments (expected: 0, actual: 1). This call will be ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:835:3-835:20)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:835:3-835:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:841:3-841:20)
[Warning][Unsound][Call][CWE-685] Potential call to function de_allocator with wrong number of arguments (expected: 0, actual: 1). This call will be ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:841:3-841:20)
[Warning][Unsound][Call][CWE-685] Potential call to function allocator with wrong number of arguments (expected: 0, actual: 1). This call will be ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:841:3-841:20)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:841:3-841:20)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:178:1-182:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:183:1-187:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:188:1-192:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:193:1-197:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:198:1-202:1)
[Warning][Deadcode] Function '__CS_pthread_mutex_lock' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:582:1-587:1)
[Warning][Deadcode] Function '__CS_pthread_mutex_unlock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:588:1-596:1)
[Warning][Deadcode] Function '__CS_pthread_cond_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:597:1-600:1)
[Warning][Deadcode] Function '__CS_pthread_cond_signal' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:601:1-608:1)
[Warning][Deadcode] Function '__CS_pthread_cond_broadcast' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:609:1-616:1)
[Warning][Deadcode] Function '__CS_pthread_cond_wait' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:617:1-630:1)
[Warning][Deadcode] Function '__CS_assert' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:631:1-637:1)
[Warning][Deadcode] Function 'allocator' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:691:1-725:1)
[Warning][Deadcode] Function 'de_allocator' is uncalled: 19 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:726:1-752:1)
[Warning][Deadcode] Function '__CS_pthread_create' has dead code:
  on lines 667..668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:667-668)
[Warning][Deadcode] Function '__CS_pthread_join' has dead code:
  on lines 646..648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:646-648)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 148
  dead: 88 (83 in uncalled functions)
  total lines: 236
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-570] condition 'j < 3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-571] condition 'i < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:787:5-787:23)
[Warning][Deadcode][CWE-571] condition '(int )__CS_thread_allocated[0] == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:826:6-826:35)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-571] condition '(int )__CS_ret != (int )__CS_ret_PREEMPTED' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:836:7-836:35)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-571] condition '(int )__CS_ret != (int )__CS_ret_PREEMPTED' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:842:7-842:35)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:19:73-19:74)
[Warning][Deadcode][CWE-571] condition 'i < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:787:5-787:23)
[Warning][Deadcode][CWE-570] condition 'j < 3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-570] condition 'i < 3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:787:5-787:23)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-571] condition '(int )thread != 123' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:644:6-644:36)
[Warning][Deadcode][CWE-570] condition '(int )thread > 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:644:6-644:36)
[Warning][Deadcode][CWE-570] condition 'j < 3' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-570] condition '(int )thread == 123' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:650:7-650:83)
[Warning][Deadcode][CWE-571] condition 'i < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:787:5-787:23)
[Warning][Deadcode][CWE-570] condition '(int )__CS_thread_index == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:666:6-666:28)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
[Warning][Deadcode][CWE-571] condition 'j < 3' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-pthread/cs_time_var_mutex.i:793:7-793:25)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
[Warning][Unsound][Call] No suitable function to call
