./goblint --conf conf/bench-yaml-validate.json --enable dbg.timing.enabled --enable witness.invariant.loop-head --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.accessed --ana.base.privatization write+lock --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/protection-read/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/write+lock/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml/witness.yml --sets exp.architecture 32bit /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i


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


--sets is deprecated, use --set instead.

runtime: 00:00:10.304
vars: 17506, evals: 28344

|rho|=17506
|called|=110
|stable|=13527
|infl|=17372
|wpoint|=5
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=13946
Found 3050 contexts for 130 functions. Top 5 functions:
727	contexts for entry state of outb (5472) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5979:1-5985:1
316	contexts for entry state of __VERIFIER_nondet_int (320) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
217	contexts for entry state of printk (2788) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:12705:1-12707:1
201	contexts for entry state of switch_bank (5531) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:6683:1-6691:1
200	contexts for entry state of inb (5473) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5986:1-5993:1

Memory statistics: total=27796.31MB, max=93.92MB, minor=27769.55MB, major=262.07MB, promoted=235.31MB
    minor collections=13251  major collections=19 compactions=0


runtime: 00:00:20.335
vars: 33544, evals: 46309

|rho|=33544
|called|=84
|stable|=24940
|infl|=33424
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=27127
Found 5907 contexts for 130 functions. Top 5 functions:
1464	contexts for entry state of outb (5472) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5979:1-5985:1
611	contexts for entry state of __VERIFIER_nondet_int (320) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
493	contexts for entry state of inb (5473) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5986:1-5993:1
460	contexts for entry state of switch_bank (5531) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:6683:1-6691:1
385	contexts for entry state of printk (2788) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:12705:1-12707:1

Memory statistics: total=59678.10MB, max=142.85MB, minor=59649.45MB, major=481.43MB, promoted=452.78MB
    minor collections=28456  major collections=25 compactions=0


runtime: 00:00:30.398
vars: 49127, evals: 63848

|rho|=49127
|called|=94
|stable|=35516
|infl|=48999
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=39935
Found 8682 contexts for 130 functions. Top 5 functions:
2170	contexts for entry state of outb (5472) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5979:1-5985:1
896	contexts for entry state of __VERIFIER_nondet_int (320) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
781	contexts for entry state of inb (5473) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5986:1-5993:1
708	contexts for entry state of switch_bank (5531) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:6683:1-6691:1
544	contexts for entry state of printk (2788) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:12705:1-12707:1

Memory statistics: total=91865.59MB, max=188.92MB, minor=91835.47MB, major=698.62MB, promoted=668.50MB
    minor collections=43806  major collections=29 compactions=0


runtime: 00:00:40.462
vars: 64703, evals: 81304

|rho|=64703
|called|=82
|stable|=46670
|infl|=64586
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=52740
Found 11453 contexts for 130 functions. Top 5 functions:
2885	contexts for entry state of outb (5472) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5979:1-5985:1
1182	contexts for entry state of __VERIFIER_nondet_int (320) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1064	contexts for entry state of inb (5473) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5986:1-5993:1
959	contexts for entry state of switch_bank (5531) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:6683:1-6691:1
707	contexts for entry state of printk (2788) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:12705:1-12707:1

Memory statistics: total=124207.93MB, max=249.85MB, minor=124177.46MB, major=913.45MB, promoted=882.98MB
    minor collections=59229  major collections=32 compactions=0


runtime: 00:00:50.529
vars: 79828, evals: 98306

|rho|=79828
|called|=105
|stable|=57312
|infl|=79693
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=65175
Found 14143 contexts for 130 functions. Top 5 functions:
3572	contexts for entry state of outb (5472) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5979:1-5985:1
1460	contexts for entry state of __VERIFIER_nondet_int (320) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1342	contexts for entry state of inb (5473) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5986:1-5993:1
1200	contexts for entry state of switch_bank (5531) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:6683:1-6691:1
865	contexts for entry state of printk (2788) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:12705:1-12707:1

Memory statistics: total=156549.78MB, max=287.33MB, minor=156516.84MB, major=1126.48MB, promoted=1093.53MB
    minor collections=74652  major collections=35 compactions=0


runtime: 00:01:00.604
vars: 94879, evals: 115202

|rho|=94879
|called|=91
|stable|=67851
|infl|=94751
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=77547
Found 16822 contexts for 130 functions. Top 5 functions:
4257	contexts for entry state of outb (5472) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5979:1-5985:1
1737	contexts for entry state of __VERIFIER_nondet_int (320) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1618	contexts for entry state of inb (5473) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:5986:1-5993:1
1440	contexts for entry state of switch_bank (5531) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:6683:1-6691:1
1022	contexts for entry state of printk (2788) on /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i:12705:1-12707:1

Memory statistics: total=189437.92MB, max=330.43MB, minor=189402.19MB, major=1344.97MB, promoted=1309.23MB
    minor collections=90334  major collections=37 compactions=0

