diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index adfec0f1750ffeda8498f1858932de1ee1c6a9eb..3ea6081abfbbde526d0e9d5fa9293b852de0d88a 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -24,7 +24,9 @@ object ChooseInfo {
 
     // Look for choose()
     for (f <- prog.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
-      for ((ch, path) <- new ChooseCollectorWithPaths().traverse(f.body.get)) {
+      val actualBody = And(f.precondition.getOrElse(BooleanLiteral(true)), f.body.get)
+
+      for ((ch, path) <- new ChooseCollectorWithPaths().traverse(actualBody)) {
         results = ChooseInfo(ctx, prog, f, path, ch, options) :: results
       }
     }