warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) cpu0: pan: error detected (at depth 32) warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) cpu1: pan: error detected (at depth 989) warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) cpu2: pan: error detected (at depth 1000) warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) cpu3: pan: error detected (at depth 989) warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) cpu4: pan: error detected (at depth 1000) cpu0: Depth= 1003 States= 1e+06 Transitions= 3.16947e+06 Memory= 451.492 cpu2: Depth= 1003 States= 1e+06 Transitions= 3.16946e+06 Memory= 451.492 cpu4: Depth= 1003 States= 1e+06 Transitions= 3.16946e+06 Memory= 451.492 cpu3: Depth= 1003 States= 1e+06 Transitions= 3.21838e+06 Memory= 451.492 cpu1: Depth= 1003 States= 1e+06 Transitions= 3.21838e+06 Memory= 451.492 cpu2: Depth= 1003 States= 2e+06 Transitions= 6.62525e+06 Memory= 451.492 cpu0: Depth= 1003 States= 2e+06 Transitions= 6.62383e+06 Memory= 451.492 cpu4: Depth= 1003 States= 2e+06 Transitions= 6.62492e+06 Memory= 451.492 cpu3: Depth= 1003 States= 2e+06 Transitions= 6.67117e+06 Memory= 451.492 cpu1: Depth= 1003 States= 2e+06 Transitions= 6.6712e+06 Memory= 451.492 cpu2: Depth= 1003 States= 3e+06 Transitions= 1.01095e+07 Memory= 451.492 cpu0: Depth= 1003 States= 3e+06 Transitions= 1.01071e+07 Memory= 451.492 cpu4: Depth= 1003 States= 3e+06 Transitions= 1.01096e+07 Memory= 451.492 cpu3: Depth= 1003 States= 3e+06 Transitions= 1.01962e+07 Memory= 451.492 cpu1: Depth= 1003 States= 3e+06 Transitions= 1.01963e+07 Memory= 451.492 cpu2: Depth= 1003 States= 4e+06 Transitions= 1.36367e+07 Memory= 451.492 cpu0: Depth= 1003 States= 4e+06 Transitions= 1.36336e+07 Memory= 451.492 cpu4: Depth= 1003 States= 4e+06 Transitions= 1.3637e+07 Memory= 451.492 cpu3: Depth= 1003 States= 4e+06 Transitions= 1.37255e+07 Memory= 451.492 cpu1: Depth= 1003 States= 4e+06 Transitions= 1.37257e+07 Memory= 451.492 cpu2: Depth= 1003 States= 5e+06 Transitions= 1.71673e+07 Memory= 451.492 cpu0: Depth= 1003 States= 5e+06 Transitions= 1.7203e+07 Memory= 451.492 cpu4: Depth= 1003 States= 5e+06 Transitions= 1.7205e+07 Memory= 451.492 cpu3: Depth= 1003 States= 5e+06 Transitions= 1.72585e+07 Memory= 451.492 cpu1: Depth= 1003 States= 5e+06 Transitions= 1.72738e+07 Memory= 451.492 cpu2: Depth= 1003 States= 6e+06 Transitions= 2.07618e+07 Memory= 451.492 cpu0: Depth= 1003 States= 6e+06 Transitions= 2.07751e+07 Memory= 451.492 cpu4: Depth= 1003 States= 6e+06 Transitions= 2.07972e+07 Memory= 451.492 cpu3: Depth= 1003 States= 6e+06 Transitions= 2.08387e+07 Memory= 451.492 cpu1: Depth= 1003 States= 6e+06 Transitions= 2.08287e+07 Memory= 451.492 cpu2: Depth= 1003 States= 7e+06 Transitions= 2.43583e+07 Memory= 451.492 cpu4: Depth= 1003 States= 7e+06 Transitions= 2.43718e+07 Memory= 451.492 cpu3: Depth= 1003 States= 7e+06 Transitions= 2.44216e+07 Memory= 451.492 cpu1: Depth= 1003 States= 7e+06 Transitions= 2.43898e+07 Memory= 451.492 cpu0: Depth= 1003 States= 7e+06 Transitions= 2.65565e+07 Memory= 451.492 cpu2: Depth= 1003 States= 8e+06 Transitions= 2.79931e+07 Memory= 451.492 cpu4: Depth= 1003 States= 8e+06 Transitions= 2.80055e+07 Memory= 451.492 cpu3: Depth= 1003 States= 8e+06 Transitions= 2.8052e+07 Memory= 451.492 cpu1: Depth= 1003 States= 8e+06 Transitions= 2.79988e+07 Memory= 451.492 cpu0: Depth= 1003 States= 8e+06 Transitions= 3.33612e+07 Memory= 451.492 cpu2: Depth= 1003 States= 9e+06 Transitions= 3.22332e+07 Memory= 451.492 cpu1: Depth= 1003 States= 9e+06 Transitions= 3.24277e+07 Memory= 451.492 cpu3: Depth= 1003 States= 9e+06 Transitions= 3.22822e+07 Memory= 451.492 cpu4: Depth= 1003 States= 9e+06 Transitions= 3.19735e+07 Memory= 451.492 cpu0: Depth= 1003 States= 9e+06 Transitions= 3.9917e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1e+07 Transitions= 3.84599e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1e+07 Transitions= 3.86859e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1e+07 Transitions= 3.78585e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1e+07 Transitions= 3.85802e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1e+07 Transitions= 4.67499e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.1e+07 Transitions= 4.52319e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.1e+07 Transitions= 4.5304e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.1e+07 Transitions= 4.4513e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.1e+07 Transitions= 4.50446e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.1e+07 Transitions= 5.35974e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.2e+07 Transitions= 5.19434e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.2e+07 Transitions= 5.21729e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.2e+07 Transitions= 5.12457e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.2e+07 Transitions= 5.17205e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.2e+07 Transitions= 6.05793e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.3e+07 Transitions= 5.87347e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.3e+07 Transitions= 5.92391e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.3e+07 Transitions= 5.80279e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.3e+07 Transitions= 5.85613e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.3e+07 Transitions= 6.65852e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.4e+07 Transitions= 6.53765e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.4e+07 Transitions= 6.48562e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.4e+07 Transitions= 6.50373e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.4e+07 Transitions= 6.63702e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.4e+07 Transitions= 7.09459e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.5e+07 Transitions= 7.14419e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.5e+07 Transitions= 7.06693e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.5e+07 Transitions= 7.09929e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.5e+07 Transitions= 7.24547e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.5e+07 Transitions= 7.46342e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.6e+07 Transitions= 7.82281e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.6e+07 Transitions= 7.69068e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.6e+07 Transitions= 7.83064e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.6e+07 Transitions= 7.73824e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.6e+07 Transitions= 8.06842e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.7e+07 Transitions= 8.16582e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.7e+07 Transitions= 8.29043e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.7e+07 Transitions= 8.579e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.7e+07 Transitions= 8.36278e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.7e+07 Transitions= 8.40201e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.8e+07 Transitions= 8.54307e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.8e+07 Transitions= 8.63222e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.8e+07 Transitions= 9.01143e+07 Memory= 451.492 cpu1: Depth= 1003 States= 1.9e+07 Transitions= 8.97772e+07 Memory= 451.492 cpu2: Depth= 1003 States= 1.9e+07 Transitions= 9.04006e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.8e+07 Transitions= 9.04288e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.8e+07 Transitions= 9.08251e+07 Memory= 451.492 cpu0: Depth= 1003 States= 1.9e+07 Transitions= 9.61611e+07 Memory= 451.492 cpu3: Depth= 1003 States= 1.9e+07 Transitions= 9.56815e+07 Memory= 451.492 cpu4: Depth= 1003 States= 1.9e+07 Transitions= 9.56478e+07 Memory= 451.492 cpu1: Depth= 1003 States= 2e+07 Transitions= 9.63994e+07 Memory= 451.492 cpu2: Depth= 1003 States= 2e+07 Transitions= 9.73878e+07 Memory= 451.492 cpu3: Depth= 1003 States= 2e+07 Transitions= 1.00038e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2e+07 Transitions= 9.99769e+07 Memory= 451.492 cpu0: Depth= 1003 States= 2e+07 Transitions= 1.04247e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.1e+07 Transitions= 1.03665e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.1e+07 Transitions= 1.04387e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.1e+07 Transitions= 1.04334e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.1e+07 Transitions= 1.05574e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.1e+07 Transitions= 1.12313e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.2e+07 Transitions= 1.08648e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.2e+07 Transitions= 1.11456e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.2e+07 Transitions= 1.12353e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.2e+07 Transitions= 1.12828e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.3e+07 Transitions= 1.13687e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.2e+07 Transitions= 1.18356e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.3e+07 Transitions= 1.19338e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.3e+07 Transitions= 1.19762e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.3e+07 Transitions= 1.20636e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.3e+07 Transitions= 1.23051e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.4e+07 Transitions= 1.20482e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.4e+07 Transitions= 1.24453e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.4e+07 Transitions= 1.27663e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.4e+07 Transitions= 1.30213e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.4e+07 Transitions= 1.28896e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.5e+07 Transitions= 1.27676e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.5e+07 Transitions= 1.30904e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.5e+07 Transitions= 1.32244e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.5e+07 Transitions= 1.35896e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.5e+07 Transitions= 1.33759e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.6e+07 Transitions= 1.35719e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.6e+07 Transitions= 1.37289e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.6e+07 Transitions= 1.38118e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.6e+07 Transitions= 1.37566e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.6e+07 Transitions= 1.42377e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.7e+07 Transitions= 1.43051e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.7e+07 Transitions= 1.43348e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.7e+07 Transitions= 1.43185e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.7e+07 Transitions= 1.42593e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.7e+07 Transitions= 1.48662e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.8e+07 Transitions= 1.49326e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.8e+07 Transitions= 1.49266e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.8e+07 Transitions= 1.48739e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.8e+07 Transitions= 1.48409e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.8e+07 Transitions= 1.54444e+08 Memory= 451.492 cpu4: Depth= 1003 States= 2.9e+07 Transitions= 1.52208e+08 Memory= 451.492 cpu2: Depth= 1003 States= 2.9e+07 Transitions= 1.54943e+08 Memory= 451.492 cpu0: Depth= 1003 States= 2.9e+07 Transitions= 1.57759e+08 Memory= 451.492 cpu1: Depth= 1003 States= 2.9e+07 Transitions= 1.55801e+08 Memory= 451.492 cpu3: Depth= 1003 States= 2.9e+07 Transitions= 1.54697e+08 Memory= 451.492 cpu0: Depth= 1003 States= 3e+07 Transitions= 1.61256e+08 Memory= 451.492 cpu4: Depth= 1003 States= 3e+07 Transitions= 1.58158e+08 Memory= 451.492 cpu1: Depth= 1003 States= 3e+07 Transitions= 1.61631e+08 Memory= 451.492 cpu2: Depth= 1003 States= 3e+07 Transitions= 1.62516e+08 Memory= 451.492 cpu3: Depth= 1003 States= 3e+07 Transitions= 1.6127e+08 Memory= 451.492 cpu0: Depth= 1003 States= 3.1e+07 Transitions= 1.64826e+08 Memory= 451.492 cpu1: Depth= 1003 States= 3.1e+07 Transitions= 1.64989e+08 Memory= 451.492 cpu4: Depth= 1003 States= 3.1e+07 Transitions= 1.64165e+08 Memory= 451.492 cpu0: Depth= 1003 States= 3.2e+07 Transitions= 1.68462e+08 Memory= 451.492 cpu2: Depth= 1003 States= 3.1e+07 Transitions= 1.69365e+08 Memory= 451.492 cpu1: Depth= 1003 States= 3.2e+07 Transitions= 1.68583e+08 Memory= 451.492 cpu3: Depth= 1003 States= 3.1e+07 Transitions= 1.68224e+08 Memory= 451.492 cpu4: Depth= 1003 States= 3.2e+07 Transitions= 1.70123e+08 Memory= 451.492 cpu0: Depth= 1003 States= 3.3e+07 Transitions= 1.72104e+08 Memory= 451.492 cpu1: Depth= 1003 States= 3.3e+07 Transitions= 1.72424e+08 Memory= 451.492 cpu2: Depth= 1003 States= 3.2e+07 Transitions= 1.73815e+08 Memory= 451.492 cpu1: done -- local memcnt 451.492 Mb cpu1: states stored 33245236 matched 1.4018031e+08 cpu2: cpu1: locks: global 0 other 353310 cpu1: waits: states 1.5892789e+08 slots 0 done -- local memcnt 451.492 Mb cpu2: states stored 32095783 matched 1.4213101e+08 cpu3: done -- local memcnt 451.492 Mb cpu3: cpu2: locks: global 12 other 270280 cpu2: waits: states 3.1259442e+09 slots 0 states stored 31629560 matched 1.4081401e+08 cpu3: locks: global 30 other 260367 cpu3: waits: states 6.7719697e+09 slots 0 cpu4: done -- local memcnt 451.492 Mb cpu4: states stored 32510951 matched 1.4159354e+08 cpu0: cpu4: locks: global 7 other 206108 cpu4: waits: states 2.965775e+09 slots 0 done -- local memcnt 451.492 Mb cpu0: states stored 33915850 matched 1.4149381e+08 cpu0: locks: global 1317 other 459158 cpu0: waits: states 5408304 slots 0 (Spin Version 5.0.0 -- 7 May 2007) + Multi-Core (NCORE=5 -z1000) + Partial Order Reduction Bit statespace search for: never claim + assertion violations + (if within scope of claim) acceptance cycles - (not selected) invalid end states - (disabled by never claim) State-vector 3436 byte, depth reached 1003, errors: 14112661 1.6339738e+08 states, stored 7.0621268e+08 states, matched 8.6961006e+08 transitions (= stored+matched) 7.7059017e+08 atomic steps hash factor: 6.57135 (best if > 100.) bits set per state: 3 (-k3) Stats on memory usage (in Megabytes): 541034.416 equivalent memory usage for states (stored*(State-vector + overhead)) 128.000 memory used for hash array (-w30) 0.153 memory used for bit stack 0.916 memory used for DFS stack (-m20000) 320.000 memory used for shared work-queues 2128.382 other (proc and chan stacks) 0.009 memory lost to fragmentation 2257.459 total actual memory usage cpu0: elapsed time 1.96e+03 seconds (1.63397e+08 states) cpu0: rate 83508.3 states/second