./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/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.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: 388
functionCalls: 929
loops: 6
loopBreaks: 0
controlFlowStatements: 1193
expressions: 7733
instructions: 1790
integralVars: (11,533)
arrayVars: (7,1)
pointerVars: (2,390)

Complexity estimates:
File: 36446
Total: 36446
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )

runtime: 00:00:10.286
vars: 30941, evals: 34710

|rho|=30941
|stable|=30399
|infl|=30888
|wpoint|=84
|sides|=5177
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=20706
|called|=61
Found 4812 contexts for 107 functions. Top 5 functions:
1474	contexts for L:entry state of outb (5546) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5979:1-5985:1
544	contexts for L:entry state of __VERIFIER_nondet_int (3808) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
455	contexts for L:entry state of switch_bank (5605) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:6683:1-6691:1
413	contexts for L:entry state of printk (1857) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:12705:1-12707:1
316	contexts for L:entry state of inb (5547) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5986:1-5993:1

Memory statistics: total=24515.83MB, max=151.80MB, minor=24508.36MB, major=324.92MB, promoted=317.45MB
    minor collections=11696  major collections=18 compactions=0


runtime: 00:00:20.405
vars: 44815, evals: 62540

|rho|=44815
|stable|=39742
|infl|=44780
|wpoint|=124
|sides|=7391
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=30147
|called|=43
Found 6956 contexts for 111 functions. Top 5 functions:
2186	contexts for L:entry state of outb (5546) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5979:1-5985:1
814	contexts for L:entry state of __VERIFIER_nondet_int (3808) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
649	contexts for L:entry state of switch_bank (5605) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:6683:1-6691:1
637	contexts for L:entry state of printk (1857) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:12705:1-12707:1
452	contexts for L:entry state of inb (5547) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5986:1-5993:1

Memory statistics: total=47882.93MB, max=351.13MB, minor=47873.00MB, major=553.34MB, promoted=543.41MB
    minor collections=22838  major collections=20 compactions=0

