Incorrect recursive cycles given for pre/postconditions

[nickbattle]

The new cyclic mutual recursion checking in Overture 2.7.4 is picking up cycles that pass through the pre- and postconditions of a function. There is an interesting question about the correct behaviour here, but pre/post expressions are not part of the "body" of a function that is being described by the mutual recursion. For example:

functions
	f: nat -> nat
	f(a) ==
		a + 1
	pre g(a) > 0
	post g(a) = 0;
	
	g: nat -> nat
	g(a) ==
		if a > 0 then f(a-1) else 0;

This currently produces two cycles, [f,g,f] and [g,f,g], because of the call to g in the pre/post expressions. But the body of f is not recursive.

I will change the cycle detection to disregard pre/postconditions (the existing logic is wrong anyway, because the order of the post calls does not follow the order of the cycle, rather being all called together when the recursion unwinds).

[nickbattle]

Fix now available in ncb/development.