From d5f10bc3f225db4d68f97b1d550cdf0a4e2e4c11 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 7 Jul 2015 17:55:44 +0200
Subject: [PATCH] Forgotten testcase
---
.../purescala/valid/Methods.scala | 29 +++++++++++++++++++
1 file changed, 29 insertions(+)
create mode 100644 src/test/resources/regression/verification/purescala/valid/Methods.scala
diff --git a/src/test/resources/regression/verification/purescala/valid/Methods.scala b/src/test/resources/regression/verification/purescala/valid/Methods.scala
new file mode 100644
index 000000000..e3c71b2a5
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Methods.scala
@@ -0,0 +1,29 @@
+import leon.lang._
+
+object Methods {
+ abstract class A
+
+ abstract class B extends A {
+ def foo(i: BigInt) = {
+ require(i > 0)
+ i + 1
+ } ensuring ( _ >= 0 )
+ }
+
+ case class C(x: BigInt) extends B {
+ val y = BigInt(42)
+ override def foo(i: BigInt) = {
+ x + y + (if (i>0) i else -i)
+ } ensuring ( _ >= x )
+ }
+
+ case class E() extends B
+
+ case class D() extends A
+
+ def f1 = {
+ val c = C(42)
+ (if (c.foo(0) + c.x > 0) c else D()).isInstanceOf[B]
+ }.holds
+
+}
--
GitLab