[raul@turing Sudoku]$ spin -a sudoku.pml

[raul@turing Sudoku]$ gcc -O2 -DSAFETY -o pan pan.c

[raul@turing Sudoku]$ ./pan -E
pan: assertion violated 0 (at depth 1298)
pan: wrote sudoku.pml.trail

(Spin Version 5.2.4 -- 2 December 2009)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	- (disabled by -E flag)

State-vector 100 byte, depth reached 1298, errors: 1
     2543 states, stored
        0 states, matched
     2543 transitions (= stored+matched)
   113596 atomic steps
hash conflicts:         0 (resolved)

    2.696	memory usage (Mbyte)


pan: elapsed time 0.04 seconds
pan: rate     63575 states/second

[raul@turing Sudoku]$ spin -t -B -T sudoku.pml
2 1 6 8 5 4 3 9 7 
5 8 3 9 7 1 4 2 6 
9 7 4 6 2 3 8 5 1 
1 9 5 7 3 6 2 4 8 
8 3 2 1 4 9 7 6 5 
4 6 7 2 8 5 1 3 9 
7 5 1 4 6 2 9 8 3 
3 2 9 5 1 8 6 7 4 
6 4 8 3 9 7 5 1 2 
spin: line  48 "sudoku.pml", Error: assertion violated
spin: text of failed assertion: assert(0)
spin: trail ends after 1299 steps