Top-level chooses have their spec extracted

src/main/scala/leon/synthesis/ConversionPhase.scala

@@ -76,6 +76,18 @@ object ConversionPhase extends UnitPhase[Program] {
    *    choose(x => post(x))
    *  }
    *
+   * 4) Functions that have only a choose as body gets their spec from the choose. 
+   *
+   *  def foo(a: T) = {
+   *    choose(x => post(a, x))
+   *  }
+   *
+   *  gets converted to:
+   *
+   *  def foo(a: T) = {
+   *    choose(x => post(a, x))
+   *  } ensuring { x => post(a, x) }
+   *
    */
 
   def convert(e : Expr, ctx : LeonContext) : Expr = {
@@ -115,7 +127,7 @@ object ConversionPhase extends UnitPhase[Program] {
       }
     }
 
-    body match {
+    val fullBody = body match {
       case Some(body) =>
         var holes  = List[Identifier]()
 
@@ -172,6 +184,14 @@ object ConversionPhase extends UnitPhase[Program] {
         val newPost = post getOrElse Lambda(Seq(ValDef(FreshIdentifier("res", e.getType))), BooleanLiteral(true))
         withPrecondition(Choose(newPost), pre)
     }
+
+    // extract spec from chooses at the top-level
+    fullBody match {
+      case Choose(spec) =>
+        withPostcondition(fullBody, Some(spec))
+      case _ =>
+        fullBody
+    }
   }