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 0000000000000000000000000000000000000000..e3c71b2a552cf8cf2e86f975e59c8f55a45d1676
--- /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
+
+}