diff --git a/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f2b06b5b28e405bfb2487875c8e964b8f212792c
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala
@@ -0,0 +1,11 @@
+object MyTuple1 {
+
+  def foo(): Int = {
+    val t = (1, true, 3)
+    val a1 = t._1
+    val a2 = t._2
+    val a3 = t._3
+    a3
+  } ensuring( _ == 1)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..22b62dc75b75b3193cb2f304118a89afbc90eb91
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala
@@ -0,0 +1,14 @@
+object MyTuple2 {
+
+  abstract class A
+  case class B(i: Int) extends A
+  case class C(a: A) extends A
+
+  def foo(): Int = {
+    val t = (B(2), C(B(3)))
+    t match {
+      case (B(x), C(y)) => x
+    }
+  } ensuring( _ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da9f85b16a48f0676d1f15741ad47536e14b57ab
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala
@@ -0,0 +1,7 @@
+object MyTuple3 {
+
+  def foo(t: (Int, Int)): (Int, Int) = {
+    t
+  } ensuring(res => res._1 > 0 && res._2 > 1)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..48383898e203c723751a7a53869ac6c8c69ae3b5
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala
@@ -0,0 +1,11 @@
+object MyTuple1 {
+
+  def foo(): Int = {
+    val t = (1, true, 3)
+    val a1 = t._1
+    val a2 = t._2
+    val a3 = t._3
+    a3
+  } ensuring( _ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9fd21eb20b14350d86d06071800ec3b86acc1a84
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala
@@ -0,0 +1,14 @@
+object MyTuple2 {
+
+  abstract class A
+  case class B(i: Int) extends A
+  case class C(a: A) extends A
+
+  def foo(): Int = {
+    val t = (B(2), C(B(3)))
+    t match {
+      case (B(x), C(y)) => x
+    }
+  } ensuring(_ == 2)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2e14c067b78d86d4d915eb72178169d641e9755a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala
@@ -0,0 +1,8 @@
+object MyTuple3 {
+
+  def foo(): Int = {
+    val t = ((2, 3), true)
+    t._1._2
+  } ensuring( _ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6fcfed661beca0487da4b02db71677e2dbaac60e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala
@@ -0,0 +1,14 @@
+
+object MyTuple4 {
+
+  abstract class A
+  case class B(i: Int) extends A
+  case class C(a: A) extends A
+
+  def foo(): Int = {
+    val t = (1, (C(B(4)), 2), 3)
+    val (a1, (C(B(x)), a2), a3) = t
+    x
+  } ensuring( _ == 4)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6a55bc8c9cdbc4f70be7a6b79c8d11137ecb0d71
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala
@@ -0,0 +1,16 @@
+object MyTuple1 {
+
+  abstract class A
+  case class B(t: (Int, Int)) extends A
+  case class C(a: A) extends A
+
+  def foo(): Int = {
+    val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3)
+    t match {
+      case (_, (B((x, y)), _), _) => x
+      case (_, (C(B((_, x))), _), y) => x
+      case (_, _, x) => x
+    }
+  } ensuring( _ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a54710fbbe54d9532a5ab4d2ba9906a48ad37acc
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala
@@ -0,0 +1,8 @@
+object MyTuple6 {
+
+  def foo(t: (Int, Int)): (Int, Int) = {
+    require(t._1 > 0 && t._2 > 1)
+    t
+  } ensuring(res => res._1 > 0 && res._2 > 1)
+
+}