From 0e8b6e664f5dfd115795a8904982a4fb4b1d31bb Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Tue, 23 Oct 2012 17:47:29 +0200
Subject: [PATCH] small changes in unification tests
---
testcases/synthesis/Unification.scala | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/testcases/synthesis/Unification.scala b/testcases/synthesis/Unification.scala
index 8e4a5c614..b98f7acd3 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
--
GitLab