(* Solves for "x" in "a * x + b = 0". *)

FUNC x = Linear(a, b) IS x = -b / a END;

PROC res, flag := Test1(a, b) IS 
  VAR x IN 
    x = Linear(a, b) -> res := x; flag := 0 
  END | res := 0; flag := 1 
END;

PROC res := Test2() IS 
  IF 1 = 1 / 0 -> res := 0 | res := 1 FI 
END;

PRED Pred1(a, b) IS a = b AND a = b + 2 END;

PRED Pred2(a) IS a = 1 / 0 END;

PRED Pred3(a, b) IS a = 1 / b END;

FUNC res = Func1() IS res = 1 END;