/* Version with partition of numerical invariant using a Boolean variable */
/* exact semantics:
   if (n>=101) then n-10 else 91 */

proc MC(b:bool,n:int) returns (r:int)
var t1:int, t2:int, b1:bool;
begin
  if (b != (n>100)) then fail; endif;
  if b then
     r = n-10;
  else 
     t1 = n + 11;
     b1 = t1>100;
     t2 = MC(b1,t1);
     b1 = t2>100;
     r = MC(b1,t2);
  endif;
end

var x:int, y:int,b:bool;
begin
  b = x>100;
  y = MC(b,x);
end