id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
151	Fib example gets wrong answer	Stephen Siegel	ywei	"The Fibonacci example has a ""bad"" implementation which is not functionally equivalent to the spec, but the loop method comparator says it is functionally equivalent.

The problem seems to occur at State 20, where the Enabler seems to say there are no outgoing transitions, even though there are.

What is supposed to happen is that when the spec hits the branch ""if (tmp>=p)"" it must explore both the true and false branches.  When it explores the false branch it sets err=p-tmp then continues until it gets back to location l.  Then the impl proceeds and gets to its location l.   Then we check that the co-invariant holds, but it should not hold, because it will not be true that err==spec.err (they are off by a minus sign). 

"	defect	closed	major		verify	1.0	fixed	loop fib co-invariant