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 0000000000000000000000000000000000000000..0489202c0c195517cc1d6b97f2e794b53da9dd2e --- /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 ) + } + +}