./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/goblint-regression/04-mutex_05-lockfuns.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
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: 38
functionCalls: 31
loops: 6
loopBreaks: 0
controlFlowStatements: 117
expressions: 729
instructions: 108
integralVars: (6,41)
arrayVars: (3,0)
pointerVars: (3,13)

Complexity estimates:
File: 2
Total: 3785
Congruence: 578
Enabled congruence domain.
Octagon: 1000
Enabled octagon domain for:
myglobal, lock, i, key, count, a, tmp, j, count, k, size, a, b, c, i, id, __x, __x, __x
Widening: 2205
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )

runtime: 00:00:10.131
vars: 24517, evals: 24497

|rho|=24517
|stable|=24517
|infl|=24510
|wpoint|=1
|sides|=4918
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=14700
|called|=9
Found 4898 contexts for 4 functions. Top 5 functions:
4895	contexts for L:entry state of unlock (1533) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:922:1-924:1
1	contexts for L:entry state of lock (1532) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:919:1-921:1
1	contexts for L:entry state of t_fun (1534) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:925:1-930:1
1	contexts for L:entry state of main (1537) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:931:1-939:1

Memory statistics: total=7503.80MB, max=76.11MB, minor=7498.05MB, major=113.67MB, promoted=107.91MB
    minor collections=3581  major collections=13 compactions=0


runtime: 00:00:20.185
vars: 42337, evals: 42315

|rho|=42337
|stable|=42335
|infl|=42330
|wpoint|=1
|sides|=8482
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=25392
|called|=8
Found 8462 contexts for 4 functions. Top 5 functions:
8459	contexts for L:entry state of unlock (1533) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:922:1-924:1
1	contexts for L:entry state of lock (1532) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:919:1-921:1
1	contexts for L:entry state of t_fun (1534) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:925:1-930:1
1	contexts for L:entry state of main (1537) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:931:1-939:1

Memory statistics: total=13528.62MB, max=133.13MB, minor=13520.01MB, major=195.59MB, promoted=186.98MB
    minor collections=6454  major collections=15 compactions=0


runtime: 00:00:30.224
vars: 58583, evals: 58562

|rho|=58583
|stable|=58583
|infl|=58575
|wpoint|=1
|sides|=11731
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=35139
|called|=8
Found 11712 contexts for 4 functions. Top 5 functions:
11709	contexts for L:entry state of unlock (1533) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:922:1-924:1
1	contexts for L:entry state of lock (1532) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:919:1-921:1
1	contexts for L:entry state of t_fun (1534) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:925:1-930:1
1	contexts for L:entry state of main (1537) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:931:1-939:1

Memory statistics: total=19435.78MB, max=176.07MB, minor=19425.73MB, major=272.23MB, promoted=262.17MB
    minor collections=9270  major collections=16 compactions=0


runtime: 00:00:40.293
vars: 73981, evals: 73960

|rho|=73981
|stable|=73979
|infl|=73974
|wpoint|=1
|sides|=14811
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44379
|called|=8
Found 14791 contexts for 4 functions. Top 5 functions:
14788	contexts for L:entry state of unlock (1533) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:922:1-924:1
1	contexts for L:entry state of lock (1532) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:919:1-921:1
1	contexts for L:entry state of t_fun (1534) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:925:1-930:1
1	contexts for L:entry state of main (1537) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:931:1-939:1

Memory statistics: total=25420.32MB, max=202.48MB, minor=25406.04MB, major=349.75MB, promoted=335.47MB
    minor collections=12123  major collections=18 compactions=0


runtime: 00:00:50.375
vars: 89373, evals: 89352

|rho|=89373
|stable|=89372
|infl|=89365
|wpoint|=1
|sides|=17889
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53613
|called|=8
Found 17870 contexts for 4 functions. Top 5 functions:
17867	contexts for L:entry state of unlock (1533) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:922:1-924:1
1	contexts for L:entry state of lock (1532) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:919:1-921:1
1	contexts for L:entry state of t_fun (1534) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:925:1-930:1
1	contexts for L:entry state of main (1537) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:931:1-939:1

Memory statistics: total=31784.63MB, max=267.79MB, minor=31768.86MB, major=426.83MB, promoted=411.06MB
    minor collections=15157  major collections=18 compactions=0


runtime: 00:01:00.446
vars: 103628, evals: 103607

|rho|=103628
|stable|=103627
|infl|=103620
|wpoint|=1
|sides|=20740
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=62166
|called|=8
Found 20721 contexts for 4 functions. Top 5 functions:
20718	contexts for L:entry state of unlock (1533) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:922:1-924:1
1	contexts for L:entry state of lock (1532) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:919:1-921:1
1	contexts for L:entry state of t_fun (1534) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:925:1-930:1
1	contexts for L:entry state of main (1537) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_05-lockfuns.i:931:1-939:1

Memory statistics: total=38046.97MB, max=307.95MB, minor=38029.70MB, major=500.57MB, promoted=483.30MB
    minor collections=18143  major collections=19 compactions=0

