From eba480cabc9ae5807c4cfede64e06583bce77b27 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 26 Oct 2012 17:42:47 +0200
Subject: [PATCH] Add testcase for matching reconstruction
---
testcases/synthesis/Matching.scala | 13 +++++++++++++
1 file changed, 13 insertions(+)
create mode 100644 testcases/synthesis/Matching.scala
diff --git a/testcases/synthesis/Matching.scala b/testcases/synthesis/Matching.scala
new file mode 100644
index 000000000..21a7cf442
--- /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
+}
--
GitLab