diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 5e97203c37498c7d74680c9a133af5261066cc67..52f9d7bd0ed2bf180bae0b2a9da2d9deee9a78f0 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -26,8 +26,7 @@ import Witnesses._
   */
 case class Problem(as: List[Identifier], ws: Expr, pc: Path, phi: Expr, xs: List[Identifier], eb: ExamplesBank = ExamplesBank.empty) extends Printable {
 
-  // Activate this for debugging...
-  // assert(eb.examples.forall(_.ins.size == as.size))
+  // require(eb.examples.forall(_.ins.size == as.size))
 
   val TopLevelAnds(wsList) = ws
 
@@ -37,15 +36,16 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Path, phi: Expr, xs: List
   def allAs = as ++ (pc.bindings.map(_._1) diff wsList.collect{ case Inactive(i) => i })
 
   def asString(implicit ctx: LeonContext): String = {
+    def pad(padding: String, text: String) = text.lines.mkString(s"\n|$padding")
     val pcws = pc withCond ws
 
     val ebInfo = "/"+eb.valids.size+","+eb.invalids.size+"/"
 
-    s"""|⟦  ${if (as.nonEmpty) as.map(_.asString).mkString(", ") else "()"}
-        |   ${pcws.toClause.asString} ≺
-        |   ⟨ ${phi.asString} ⟩ 
-        |   ${if (xs.nonEmpty) xs.map(_.asString).mkString(", ") else "()"}
-        |⟧  $ebInfo""".stripMargin
+    s"""|⟦ \u0305α ${if (as.nonEmpty) as.map(_.asString).mkString(", ") else "()"}
+        |  Π ${pad("    ", pcws.fullClause.asString)}
+        |  φ ${pad("    ", phi.asString)}
+        |  \u0305x ${if (xs.nonEmpty) xs.map(_.asString).mkString(", ") else "()"}
+        |⟧ $ebInfo""".stripMargin
   }
 
   def withWs(es: Traversable[Expr]) = {
diff --git a/src/main/scala/leon/synthesis/Search.scala b/src/main/scala/leon/synthesis/Search.scala
index 564c630fcb199b776805f17fd6f80c5e8752e3d7..e9501009d89730cfccd6694f27d518c81cd52c4d 100644
--- a/src/main/scala/leon/synthesis/Search.scala
+++ b/src/main/scala/leon/synthesis/Search.scala
@@ -8,7 +8,6 @@ import graph._
 
 import scala.annotation.tailrec
 
-import scala.collection.mutable.ArrayBuffer
 import leon.utils.Interruptible
 import java.util.concurrent.atomic.AtomicBoolean
 
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 59ae2ae37f831cf068ffbcbb2e367037697069e6..1a0c1440e7ab73c5e1c25dbf9e3d790fb9aabfe7 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -82,7 +82,7 @@ class AndNode(parent: Option[Node], val ri: RuleInstantiation) extends Node(pare
 
     import hctx.reporter.info
 
-    val prefix = f"[${Option(ri.rule.asString).getOrElse("?")}%-20s]"
+    val prefix = f"[${Option(ri).map(_.asString).getOrElse("?")}%-20s]"
 
     info(pad(prefix, ri.problem.asString))
 
diff --git a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
index 8c2f14cc2e209378b03d3a3d813792f7c9b0831a..2d2999871d7d1bf6494c2363e63b3bd32d6ac138 100644
--- a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
+++ b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
@@ -53,7 +53,7 @@ case object IntroduceRecCalls extends NormalizingRule("Introduce rec. calls") {
 
     val onSuccess = forwardMap(letTuple(recs.map(_._1), tupleWrap(calls), _))
 
-    List(new RuleInstantiation(s"Introduce recursive calls ${calls mkString ", "}", SolutionBuilderDecomp(List(p.outType), onSuccess)) {
+    List(new RuleInstantiation(s"Introduce calls ${calls mkString ", "}", SolutionBuilderDecomp(List(p.outType), onSuccess)) {
 
       def apply(nohctx: SearchContext): RuleApplication = {