./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1331:5-1335:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:5-1354:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1379:5-1386:5 with factor 10
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1387:5-1393:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:5-1398:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
Collected factors:
functions: 35
functionCalls: 101
loops: 11
loopBreaks: 0
controlFlowStatements: 304
expressions: 1854
instructions: 337
integralVars: (8,49)
arrayVars: (4,0)
pointerVars: (3,19)

Complexity estimates:
File: 15417
function main uses mod, enable congruence domain recursively for:
  "down":
    __VERIFIER_assert
    reach_error
    __VERIFIER_nondet_int
  "up":
Total: 27621
Congruence: 2101
Enabled congruence domain.
Octagon: 4000
Enabled octagon domain for:
exit, a, i, key, count___0, a___0, tmp, j, count___0, k, size, a___0, b, c, i, i, ret_count, temp, i, end, local_count, start
Widening: 6103
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1364:5-1364:62)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(attr, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1369:5-1369:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1369:5-1369:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(attr, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1374:5-1374:76)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1374:5-1374:76)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1381:9-1381:87)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1332:14-1332:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1333:13-1333:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1337:5-1337:32)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1381:9-1381:87)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1388:9-1388:58)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1388:9-1388:58)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1396:11-1396:28)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1401:5-1401:44)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(ret_count, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1406:5-1406:52)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:67:1-71:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:72:1-76:1)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 1358..1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1358-1359)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 64
  dead: 4 (2 in uncalled functions)
  total lines: 68
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-570] condition 'i < num_threads' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1379:9-1379:33)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < num_threads' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1387:9-1387:33)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-570] condition 'i < num_threads' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1387:9-1387:33)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:12:73-12:74)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-570] condition 'num_threads > 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1357:9-1357:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < num_threads' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1379:9-1379:33)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < num_threads' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1379:9-1379:33)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1352:9-1352:24)
[Warning][Deadcode][CWE-571] condition 'i < 1000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1395:9-1395:24)
[Warning][Deadcode][CWE-571] condition 'i < num_threads' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1387:9-1387:33)
SV-COMP result: true
[Info][Race] Memory locations race summary:
  safe: 7
  vulnerable: 0
  unsafe: 0
  total memory locations: 7
lib/libc/stub/src/stdlib.c:6: Warning: Incompatible declaration for qsort (from .goblint/preprocessed/stdlib.i(3)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1254 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i (0)) 
	Failed assumption that size_t and size_t are isomorphic (different integer types unsigned int  and unsigned long ) 
lib/libc/stub/src/stdlib.c:37: Warning: Incompatible declaration for bsearch (from .goblint/preprocessed/stdlib.i(3)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i:1251 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-finding-k-matches.i (0)) 
	Failed assumption that size_t and size_t are isomorphic (different integer types unsigned int  and unsigned long ) 
lib/libc/stub/src/stdlib.c:7: Warning: The name qsort is used for two distinct globals
lib/libc/stub/src/stdlib.c:38: Warning: The name bsearch is used for two distinct globals
