diff --git a/library/Utils.scala b/library/Utils.scala
index 44b05cd36019b12f7b4f46655b3dfb4a2d3436f8..12c81d7a0a5211edcfd4eee228b97ab5a0376570 100644
--- a/library/Utils.scala
+++ b/library/Utils.scala
@@ -22,11 +22,11 @@ object Utils {
 
   private def noChoose = throw new RuntimeException("Implementation not supported")
 
-  def choose[A](predicate: A => Boolean) = noChoose
-  def choose[A, B](predicate: (A, B) => Boolean) = noChoose
-  def choose[A, B, C](predicate: (A, B, C) => Boolean) = noChoose
-  def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean) = noChoose
-  def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean) = noChoose
-  def choose[A, B, C, D, E, F](predicate: (A, B, C, D, E, F) => Boolean) = noChoose
-  def choose[A, B, C, D, E, F, G](predicate: (A, B, C, D, E, F, G) => Boolean) = noChoose
+  def choose[A](predicate: A => Boolean): A = noChoose
+  def choose[A, B](predicate: (A, B) => Boolean): (A, B) = noChoose
+  def choose[A, B, C](predicate: (A, B, C) => Boolean): (A, B, C) = noChoose
+  def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noChoose
+  def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noChoose
+  def choose[A, B, C, D, E, F](predicate: (A, B, C, D, E, F) => Boolean): (A, B, C, D, E, F) = noChoose
+  def choose[A, B, C, D, E, F, G](predicate: (A, B, C, D, E, F, G) => Boolean): (A, B, C, D, E, F, G) = noChoose
 }
diff --git a/testcases/Choose.scala b/testcases/Choose.scala
new file mode 100644
index 0000000000000000000000000000000000000000..22dbc18f4745710ee0b97480787d787ddb0cef78
--- /dev/null
+++ b/testcases/Choose.scala
@@ -0,0 +1,7 @@
+import leon.Utils._
+
+object Abs {
+
+  def abs(x: Int): Int = choose{ x: Int => x > 0 }
+
+}