~/atva/Ocaml/speedtest/david_spec2 > runobli.sh 2
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
Depth=   98442 States=   1e+06 Transitions= 3.49804e+06 Memory= 151.333
Depth=   98996 States=   2e+06 Transitions= 7.12758e+06 Memory= 190.962
Depth=  103809 States=   3e+06 Transitions= 1.10388e+07 Memory= 230.591
Depth=  230152 States=   4e+06 Transitions= 1.39409e+07 Memory= 270.731
Depth=  239637 States=   5e+06 Transitions= 1.78463e+07 Memory= 310.360
Depth=  324091 States=   6e+06 Transitions= 2.10446e+07 Memory= 350.501
Depth=  347355 States=   7e+06 Transitions= 2.46268e+07 Memory= 390.027
Depth=  400445 States=   8e+06 Transitions= 2.81532e+07 Memory= 429.861
Depth=  460791 States=   9e+06 Transitions= 3.18026e+07 Memory= 469.592
Depth=  516643 States=   1e+07 Transitions= 3.53026e+07 Memory= 509.528
Depth=  582518 States= 1.1e+07 Transitions= 3.88973e+07 Memory= 549.464
Depth=  620693 States= 1.2e+07 Transitions= 4.26078e+07 Memory= 589.400
Depth=  620693 States= 1.3e+07 Transitions= 4.64492e+07 Memory= 629.029
Depth=  621315 States= 1.4e+07 Transitions= 5.03637e+07 Memory= 668.760
Depth=  621315 States= 1.5e+07 Transitions= 5.42746e+07 Memory= 708.184
Depth=  621315 States= 1.6e+07 Transitions= 5.76678e+07 Memory= 746.482
(Spin Version 4.2.9 -- 8 February 2007)
        + Partial Order Reduction
        + Compression

Full statespace search for:
        never claim             +
        assertion violations    + (if within scope of claim)
        acceptance   cycles     + (fairness disabled)
        invalid end states      - (disabled by never claim)

State-vector 240 byte, depth reached 621315, errors: 0
1.68117e+07 states, stored
4.38203e+07 states, matched
6.0632e+07 transitions (= stored+matched)
1.14683e+08 atomic steps
hash conflicts: 1.39748e+07 (resolved)

Stats on memory usage (in Megabytes):
4303.796        equivalent memory usage for states (stored*(State-vector + overhead))
663.244 actual memory usage for states (compression: 15.41%)
        State-vector as stored = 23 byte + 16 byte overhead
67.109  memory used for hash table (-w24)
44.800  memory used for DFS stack (-m1400000)
2.447   other (proc and chan stacks)
0.114   memory lost to fragmentation
777.714 total actual memory usage

nr of templates: [ globals chans procs ]
collapse counts: [ 406 129 31 2067 210 4525 4251 2 4 ]

real    5m17.456s
user    5m15.930s
sys     0m1.530s