diff --git a/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala b/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala
new file mode 100644
index 000000000..2a13c9fb0
--- /dev/null
+++ b/frontends/benchmarks/extraction/valid/PatternAlternative1 copy.scala	
@@ -0,0 +1,20 @@
+object PatternAlternative1 {
+  sealed trait SignSet
+  case object None extends SignSet
+  case object Any extends SignSet
+  case object Neg extends SignSet 
+  case object Zer extends SignSet
+  case object Pos extends SignSet
+  case object NegZer extends SignSet
+  case object  NotZer extends SignSet
+  case object  PosZer extends SignSet
+
+  def subsetOf(a: SignSet, b: SignSet): Boolean = (a, b) match {
+    case (None, _) => true
+    case (_, Any) => true
+    case (Neg, NegZer | NotZer) => true
+    case (Zer, NegZer | PosZer) => true
+    case (Pos, NotZer | PosZer) => true
+    case _                  => false
+  }
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/extraction/valid/PatternAlternative2.scala b/frontends/benchmarks/extraction/valid/PatternAlternative2.scala
new file mode 100644
index 000000000..acdf27809
--- /dev/null
+++ b/frontends/benchmarks/extraction/valid/PatternAlternative2.scala
@@ -0,0 +1,33 @@
+object PatternAlternative2 {
+  sealed trait Tree
+  case class Node(left: Tree, right: Tree) extends Tree
+  case class IntLeaf(value: Int) extends Tree
+  case class StringLeaf(value: String) extends Tree
+  case class NoneLeaf() extends Tree
+
+  def containsNoneLeaf(tree: Tree): Boolean = {
+    tree match {
+      case Node(left, right) => containsNoneLeaf(left) || containsNoneLeaf(right)
+      case NoneLeaf() => true
+      case _ => false
+    }
+  }
+
+  def containsOnlyBinaryLeaves(tree: Tree): Boolean = {
+    tree match {
+      case Node(left, right) => containsOnlyBinaryLeaves(left) && containsOnlyBinaryLeaves(right)
+      case IntLeaf(v) => v == 0 || v == 1
+      case StringLeaf(v) => v == "0" || v == "1"
+      case _ => true
+    }
+  }
+
+  def hasBinaryLeaves(tree: Tree): Boolean = {
+    require(!containsNoneLeaf(tree) && containsOnlyBinaryLeaves(tree))
+    tree match {
+      case a @ Node(left: (IntLeaf | StringLeaf), right: (IntLeaf | StringLeaf)) => hasBinaryLeaves(left) && hasBinaryLeaves(right)
+      case b @ (IntLeaf(0 | 1) | StringLeaf("0" | "1")) => true
+      case _ => false
+    }
+  } ensuring { res => res }
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/verification/valid/PatternAlternative.scala b/frontends/benchmarks/verification/valid/PatternAlternative.scala
new file mode 100644
index 000000000..7be570355
--- /dev/null
+++ b/frontends/benchmarks/verification/valid/PatternAlternative.scala
@@ -0,0 +1,33 @@
+object PatternAlternative {
+  sealed trait Tree
+  case class Node(left: Tree, right: Tree) extends Tree
+  case class IntLeaf(value: Int) extends Tree
+  case class StringLeaf(value: String) extends Tree
+  case class NoneLeaf() extends Tree
+
+  def containsNoneLeaf(tree: Tree): Boolean = {
+    tree match {
+      case Node(left, right) => containsNoneLeaf(left) || containsNoneLeaf(right)
+      case NoneLeaf() => true
+      case _ => false
+    }
+  }
+
+  def containsOnlyBinaryLeaves(tree: Tree): Boolean = {
+    tree match {
+      case Node(left, right) => containsOnlyBinaryLeaves(left) && containsOnlyBinaryLeaves(right)
+      case IntLeaf(v) => v == 0 || v == 1
+      case StringLeaf(v) => v == "0" || v == "1"
+      case _ => true
+    }
+  }
+
+  def hasBinaryLeaves(tree: Tree): Boolean = {
+    require(!containsNoneLeaf(tree) && containsOnlyBinaryLeaves(tree))
+    tree match {
+      case a @ Node(left: (IntLeaf | StringLeaf), right: (IntLeaf | StringLeaf)) => hasBinaryLeaves(left) && hasBinaryLeaves(right)
+      case b @ (IntLeaf(0 | 1) | StringLeaf("0" | "1")) => true
+      case _ => false
+    }
+  } ensuring { res => res }
+}
\ No newline at end of file