diff --git a/testcases/synthesis/Unification.scala b/testcases/synthesis/Unification.scala
index 8e4a5c6145b1992bca76f2012f30b1ec3d328ea0..b98f7acd3ac3863a33853c6f917a35937b56dbd7 100644
--- a/testcases/synthesis/Unification.scala
+++ b/testcases/synthesis/Unification.scala
@@ -3,8 +3,14 @@ import leon.Utils._
 object UnificationSynthesis {
 
   def u1(a1: Int): Int = choose { (x1: Int) => Cons(x1, Nil()) == Cons(a1, Nil()) }
+
   def u2(a1: Int): Int = choose { (x1: Int) => Cons(x1, Nil()) == Cons(x1, Cons(2, Nil())) }
-  def u3(a1: Int): List = choose { (xs: List) => Cons(a1, xs) == xs }
+
+  def u3(a1: Int): (Int,Int) = choose { (x1: Int, x2: Int) => Cons(x1, Nil()) == Cons(x2, Cons(a1, Nil())) }
+
+  def u4(a1: Int): List = choose { (xs: List) => Cons(a1, xs) == xs }
+
+  def u5(a1: Int): List = choose { (xs: List) => Cons(a1, Nil()) == xs }
 
   sealed abstract class List
   case class Nil() extends List