From 96ce1929f28eab449149ad5b66479394c7b59130 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 15 Jul 2015 14:52:05 +0200
Subject: [PATCH] Test unapply-synthesis interaction
---
.../regression/synthesis/Misc/Unapply.scala | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
create mode 100644 src/test/resources/regression/synthesis/Misc/Unapply.scala
diff --git a/src/test/resources/regression/synthesis/Misc/Unapply.scala b/src/test/resources/regression/synthesis/Misc/Unapply.scala
new file mode 100644
index 000000000..0489202c0
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Misc/Unapply.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object Unap {
+ def unapply[A, B](i: (Int, B, A)): Option[(A, B)] =
+ if (i._1 == 0) None() else Some((i._3, i._2))
+}
+
+object Unapply {
+ def bar(i: Int, b: Boolean): Boolean = (i, b, ()) match {
+ case Unap(_, b) if b => b
+ case Unap((), b) =>
+ choose( (b1: Boolean) => b == b1 == i < 0 )
+ }
+
+}
--
GitLab