./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-lit/fk2012.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1039:2-1042:2 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1049:5-1053:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1065:5-1071: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: 44
functionCalls: 113
loops: 9
loopBreaks: 0
controlFlowStatements: 248
expressions: 1255
instructions: 241
integralVars: (7,48)
arrayVars: (2,0)
pointerVars: (0,14)

Complexity estimates:
File: 5743
Total: 14803
Congruence: 1665
Enabled congruence domain.
Octagon: 3000
Enabled octagon domain for:
counter, pthread_create, i, key, count, a, tmp, j, count, k, size, a, b, c, i, tmp, batch, tmp, __x, __x, __x
Widening: 4395
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )

runtime: 00:00:10.122
vars: 1643, evals: 13837

|rho|=1643
|stable|=1501
|infl|=1640
|wpoint|=16
|sides|=267
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1223
|called|=3
Found 155 contexts for 11 functions. Top 5 functions:
69	contexts for L:entry state of __VERIFIER_nondet_int (348) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
19	contexts for L:entry state of assume_abort_if_not (343) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:15:1-17:1
12	contexts for L:entry state of release2 (1590) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1021:1-1026:1
12	contexts for L:entry state of release1 (1588) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1009:1-1014:1
12	contexts for L:entry state of acquire1 (1587) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1003:1-1008:1

Memory statistics: total=30946.67MB, max=23.48MB, minor=30943.63MB, major=185.05MB, promoted=182.01MB
    minor collections=14772  major collections=34 compactions=0


runtime: 00:00:20.158
vars: 2019, evals: 17687

|rho|=2019
|stable|=1940
|infl|=2016
|wpoint|=17
|sides|=345
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1449
|called|=3
Found 228 contexts for 11 functions. Top 5 functions:
134	contexts for L:entry state of __VERIFIER_nondet_int (348) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
21	contexts for L:entry state of assume_abort_if_not (343) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:15:1-17:1
14	contexts for L:entry state of release2 (1590) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1021:1-1026:1
13	contexts for L:entry state of release1 (1588) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1009:1-1014:1
13	contexts for L:entry state of acquire1 (1587) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1003:1-1008:1

Memory statistics: total=64911.03MB, max=27.00MB, minor=64907.95MB, major=362.21MB, promoted=359.13MB
    minor collections=30981  major collections=59 compactions=0


runtime: 00:00:30.197
vars: 2019, evals: 17687

|rho|=2019
|stable|=1940
|infl|=2016
|wpoint|=17
|sides|=345
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1449
|called|=3
Found 228 contexts for 11 functions. Top 5 functions:
134	contexts for L:entry state of __VERIFIER_nondet_int (348) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
21	contexts for L:entry state of assume_abort_if_not (343) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:15:1-17:1
14	contexts for L:entry state of release2 (1590) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1021:1-1026:1
13	contexts for L:entry state of release1 (1588) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1009:1-1014:1
13	contexts for L:entry state of acquire1 (1587) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1003:1-1008:1

Memory statistics: total=101425.85MB, max=27.00MB, minor=101422.77MB, major=544.46MB, promoted=541.38MB
    minor collections=48405  major collections=82 compactions=0


runtime: 00:00:40.208
vars: 2088, evals: 18202

|rho|=2088
|stable|=2008
|infl|=2080
|wpoint|=17
|sides|=350
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1510
|called|=41
Found 232 contexts for 11 functions. Top 5 functions:
134	contexts for L:entry state of __VERIFIER_nondet_int (348) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
22	contexts for L:entry state of assume_abort_if_not (343) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:15:1-17:1
14	contexts for L:entry state of release2 (1590) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1021:1-1026:1
14	contexts for L:entry state of release1 (1588) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1009:1-1014:1
14	contexts for L:entry state of acquire1 (1587) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1003:1-1008:1

Memory statistics: total=138155.02MB, max=27.00MB, minor=138151.87MB, major=728.70MB, promoted=725.54MB
    minor collections=65931  major collections=106 compactions=0


runtime: 00:00:50.224
vars: 2116, evals: 22178

|rho|=2116
|stable|=1974
|infl|=2113
|wpoint|=19
|sides|=354
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1532
|called|=3
Found 234 contexts for 11 functions. Top 5 functions:
134	contexts for L:entry state of __VERIFIER_nondet_int (348) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
22	contexts for L:entry state of assume_abort_if_not (343) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:15:1-17:1
14	contexts for L:entry state of release2 (1590) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1021:1-1026:1
14	contexts for L:entry state of release1 (1588) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1009:1-1014:1
14	contexts for L:entry state of acquire1 (1587) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1003:1-1008:1

Memory statistics: total=173233.64MB, max=31.05MB, minor=173230.48MB, major=907.27MB, promoted=904.11MB
    minor collections=82669  major collections=128 compactions=0


runtime: 00:01:00.251
vars: 2116, evals: 22178

|rho|=2116
|stable|=1974
|infl|=2113
|wpoint|=19
|sides|=354
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=1532
|called|=3
Found 234 contexts for 11 functions. Top 5 functions:
134	contexts for L:entry state of __VERIFIER_nondet_int (348) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
22	contexts for L:entry state of assume_abort_if_not (343) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:15:1-17:1
14	contexts for L:entry state of release2 (1590) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1021:1-1026:1
14	contexts for L:entry state of release1 (1588) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1009:1-1014:1
14	contexts for L:entry state of acquire1 (1587) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/fk2012.i:1003:1-1008:1

Memory statistics: total=209696.06MB, max=31.05MB, minor=209692.89MB, major=1088.10MB, promoted=1084.94MB
    minor collections=100067  major collections=150 compactions=0

