./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.267
vars: 32769, evals: 36340

|rho|=32769
|stable|=32205
|infl|=32716
|wpoint|=87
|sides|=5464
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=21959
|called|=60
Found 5784 contexts for 107 functions. Top 5 functions:
1720	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
652	contexts for L:entry state of __VERIFIER_nondet_int (3808) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
564	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
496	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
398	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=25472.80MB, max=174.57MB, minor=25464.69MB, major=340.96MB, promoted=332.85MB
    minor collections=12152  major collections=18 compactions=0


runtime: 00:00:20.408
vars: 45236, evals: 62861

|rho|=45236
|stable|=40165
|infl|=45162
|wpoint|=124
|sides|=7462
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=30427
|called|=81
Found 7015 contexts for 113 functions. Top 5 functions:
2203	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
827	contexts for L:entry state of __VERIFIER_nondet_int (3808) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
654	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
645	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
454	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=49068.17MB, max=464.37MB, minor=49058.23MB, major=820.45MB, promoted=810.51MB
    minor collections=23404  major collections=22 compactions=0

