cpu1: Depth= 476200 States= 249996 Transitions= 1.99997e+06 Memory= 55.312 t= 62.6 R= 3990.3591 cpu1: locks: global 0 gg 0 other 9179 waits: states 26761801 slots 0 cpu0: Depth= 476180 States= 250005 Transitions= 2.00003e+06 Memory= 210.301 t= 62.6 R= 3990.5028 cpu0: locks: global 0 gg 0 other 8709 waits: states 12226382 slots 0 (Spin Version 5.0 -- 12 June 2007) + Multi-Core (NCORE=2 -z20) Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 276 byte, depth reached 476180, errors: 0 500001 states, stored 3500000 states, matched 4000001 transitions (= stored+matched) 0 atomic steps hash conflicts: 875344 (resolved) hint: increase hashtable-size (-w) to reduce runtime Stats on memory usage (in Megabytes): 137.329 equivalent memory usage for states (stored*(State-vector + overhead)) 110.718 actual memory usage for states (compression: 80.62%) state-vector as stored = 220 byte + 12 byte overhead 4.000 memory used for hash table (-w19) 22.889 memory used for DFS stack (-m500010) 128.000 memory used for shared work-queues 128.006 other (proc and chan stacks) 265.613 total actual memory usage unreached in proctype test line 36, state 8, "-end-" (1 of 8 states) cpu0: elapsed time 62.8 seconds (500001 states visited) cpu0: rate 7961.8 states/second cpu0: recommend recompiling with -DPMAX=8 -DQMAX=1