diff --git a/src/test/resources/regression/verification/purescala/valid/Rational.scala b/src/test/resources/regression/verification/purescala/valid/Rational.scala index 4979d970a53a73140733da599978f2d1184ceb1e..d572a8bd3324390e81cc1ce3bf855d60e9bc61d6 100644 --- a/src/test/resources/regression/verification/purescala/valid/Rational.scala +++ b/src/test/resources/regression/verification/purescala/valid/Rational.scala @@ -5,10 +5,10 @@ object Rationals { // Represents n/d case class Q(n: BigInt, d: BigInt) - def +(a: Q, b: Q) = { + def op(a: Q, b: Q) = { require(isRational(a) && isRational(b)) - Q(a.n*b.d + b.n*a.d, a.d*b.d) + Q(a.n + b.n, a.d) } ensuring { isRational(_) }