// @(#)$Id: answer2.h,v 1.3 1997/06/03 23:06:56 leavens Exp $

// This answer is a translation of answer 1, where the case analysis
// is desugared, and the formulas simplified.

struct Overflow {int a; int b;};

int multiply(int i, int j) throw(Overflow);
//@ behavior {
//@   ensures (inRange(i * j) => returns /\ result = i * j)
//@ 	   /\ (~inRange(i * j) =>
//@                    throws(Overflow) /\ thrown(Overflow) = [i, j]);
//@ }