(Spin Version 5.2.4 -- 2 December 2009)

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

State-vector 56 byte, depth reached 18, errors: 0
       92 states, stored
       62 states, matched
      154 transitions (= stored+matched)
        1 atomic steps
hash conflicts:         0 (resolved)

    2.462	memory usage (Mbyte)

unreached in proctype f
	line 13, state 20, "((y>6))"
	line 13, state 20, "else"
	(1 of 24 states)
unreached in proctype g
	line 33, state 7, "y = 3"
	line 36, state 10, "x = 8"
	line 40, state 15, "y = 6"
	line 38, state 17, "((h>6))"
	line 38, state 17, "else"
	line 43, state 19, "h = 4"
	line 31, state 20, "((x<5))"
	line 31, state 20, "else"
	line 52, state 30, "x = 6"
	line 54, state 33, "h = 1"
	line 52, state 35, "((y<1))"
	line 52, state 35, "else"
	line 57, state 37, "h = 3"
	(10 of 44 states)
unreached in proctype :init:
	(0 of 4 states)

pan: elapsed time 0.003 seconds