diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index fd7d3fb6a52d95588c577d754fbcf5e2da91b20d..bddbcae12373ad9436a41d6c1185204d557bcef3 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -96,6 +96,6 @@ object Solution {
 
   def UNSAT(implicit p: Problem): Solution = {
     val tpe = tupleTypeWrap(p.xs.map(_.getType))
-    Solution(BooleanLiteral(false), Set(), Error(tpe, "Path condition is UNSAT!"))
+    Solution(BooleanLiteral(false), Set(), Error(tpe, "Spec is UNSAT for this path!"))
   }
 }
diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
index 666c589c304a5d8d507bfcfe9d86fd2fbc17e1a5..cf6063da0ae32c95e6028feaddcdfee43bf10598 100644
--- a/src/main/scala/leon/synthesis/SourceInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -39,7 +39,7 @@ object SourceInfo {
     }
 
     if (results.isEmpty) {
-      ctx.reporter.warning("No 'choose' found. Maybe the functions you chose do not exist?")
+      ctx.reporter.warning("No 'choose' found. Maybe the functions you indicated do not exist?")
     }
 
     results.sortBy(_.source.getPos)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 23d79c1e75d7f5d562c69e2e1350d112bb600436..50f2da1afa4481735cf214237997b473e9d89b3b 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -55,6 +55,8 @@ class Synthesizer(val context : LeonContext,
 
     val s = getSearch
 
+    reporter.info(ASCIIHelpers.title(s"Synthesizing '${ci.fd.id}'"))
+
     val t = context.timers.synthesis.search.start()
 
     val sols = s.search(sctx)