diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index f9e9f28c303ca1fda2f1c0b376421bedf4188b70..25e0d58999156906fce6599de55f86f77b6ef250 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -7,6 +7,16 @@ import leon.purescala.Trees._
 // ⟨ P | T ⟩
 case class Solution(pre: Expr, term: Expr, score: Score = 0) {
   override def toString = "⟨ "+pre+" | "+term+" ⟩" 
+
+  def toExpr = {
+    if (pre == BooleanLiteral(true)) {
+      term
+    } else if (pre == BooleanLiteral(false)) {
+      Error("Impossible program").setType(term.getType)
+    } else {
+      IfExpr(pre, term, Error("Precondition failed").setType(term.getType))
+    }
+  }
 }
 
 object Solution {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index e894cfcfb3ab0f1f7d13c988f6436a36a2648369..8a2426f3bdfb28f24009dcea188b5a88ee8fecf8 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -96,7 +96,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
         val sol = synthesize(Problem(as, phi, xs), rules)
 
         info("Scala code:")
-        info(ScalaPrinter(IfExpr(sol.pre, sol.term, Error("Precondition failed").setType(sol.term.getType))))
+        info(ScalaPrinter(sol.toExpr))
 
         a
       case _ =>