diff --git a/testcases/synthesis/Matching.scala b/testcases/synthesis/Matching.scala
new file mode 100644
index 0000000000000000000000000000000000000000..21a7cf442e9165130e5a0c095bc4c86b608b9e69
--- /dev/null
+++ b/testcases/synthesis/Matching.scala
@@ -0,0 +1,13 @@
+import leon.Utils._
+
+object Matching {
+    def t1(a: NatList) = choose( (x: Nat) => Cons(x, Nil()) == a)
+
+  abstract class Nat
+  case class Z() extends Nat
+  case class Succ(n: Nat) extends Nat
+
+  abstract class NatList
+  case class Nil() extends NatList
+  case class Cons(head: Nat, tail: NatList) extends NatList
+}