From 31db59f96571f1a4d20fc21900c14055c6db42c1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Sat, 28 Feb 2015 20:54:53 +0100
Subject: [PATCH] that benchmark was checking for not equals bug
---
.../purescala/valid/{Rational.scala => NotEquals.scala} | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
rename src/test/resources/regression/verification/purescala/valid/{Rational.scala => NotEquals.scala} (86%)
diff --git a/src/test/resources/regression/verification/purescala/valid/Rational.scala b/src/test/resources/regression/verification/purescala/valid/NotEquals.scala
similarity index 86%
rename from src/test/resources/regression/verification/purescala/valid/Rational.scala
rename to src/test/resources/regression/verification/purescala/valid/NotEquals.scala
index d572a8bd3..f33e1bb5d 100644
--- a/src/test/resources/regression/verification/purescala/valid/Rational.scala
+++ b/src/test/resources/regression/verification/purescala/valid/NotEquals.scala
@@ -1,14 +1,15 @@
import leon.annotation._
import leon.lang._
-object Rationals {
+object NotEquals {
+
// Represents n/d
case class Q(n: BigInt, d: BigInt)
def op(a: Q, b: Q) = {
require(isRational(a) && isRational(b))
- Q(a.n + b.n, a.d)
+ Q(a.n + b.n, a.d)
} ensuring {
isRational(_)
}
--
GitLab