diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index cfaa57e5042ded74ea951cfcff88d02f2b376451..164b1a10273b31b2d95c0f9945c3ef21aa0f2893 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -18,6 +18,14 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List
   def inType  = tupleTypeWrap(as.map(_.getType))
   def outType = tupleTypeWrap(xs.map(_.getType))
 
+  def asString(implicit ctx: LeonContext): String = {
+    val pcws = and(ws, pc)
+
+    val tbInfo = "/"+tb.valids.size+","+tb.invalids.size+"/"
+
+    "⟦ "+as.map(_.asString).mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws.asString+" ≺ " else "")+" ⟨ "+phi.asString+" ⟩ "+xs.map(_.asString).mkString(";")+" ⟧  "+tbInfo
+  }
+
   override def toString = {
     val pcws = and(ws, pc)
 
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 9d744426802f4d1dcdc3d04cd055464924c85d8e..812b7535339b24b8a5fda05ed4f0ce6b129b37e9 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -15,6 +15,11 @@ import leon.utils.Simplifiers
 // Defines a synthesis solution of the form:
 // ⟨ P | T ⟩
 class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrusted: Boolean = true) {
+
+  def asString(implicit ctx: LeonContext) = {
+    "⟨ "+pre.asString+" | "+defs.map(_.asString).mkString(" ")+" "+term.asString+" ⟩" 
+  }
+
   override def toString = "⟨ "+pre+" | "+defs.mkString(" ")+" "+term+" ⟩" 
 
   def guardedTerm = {
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 438fbb8505adecaeb4d9883dd1be6d5d20480f9b..c4e13648b9d2071c0ce41208b42850b2bdb0d336 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -104,11 +104,13 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
     require(!isExpanded)
     isExpanded = true
 
+    implicit val ctx = hctx.sctx.context
+
     import hctx.sctx.reporter.info
 
     val prefix = f"[${Option(ri.rule).getOrElse("?")}%-20s] "
 
-    info(prefix+ri.problem)
+    info(prefix+ri.problem.asString)
 
     ri.apply(hctx) match {
       case RuleClosed(sols) =>
@@ -123,7 +125,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
           info(prefix+"Failed")
         } else {
           val sol = sols.head
-          info(prefix+"Solved"+(if(sol.isTrusted) "" else " (untrusted)")+" with: "+sol+"...")
+          info(prefix+"Solved"+(if(sol.isTrusted) "" else " (untrusted)")+" with: "+sol.asString+"...")
         }
 
         parents.foreach{ p =>
@@ -136,7 +138,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
       case RuleExpanded(probs) =>
         info(prefix+"Decomposed into:")
         for(p <- probs) {
-          info(prefix+"     - "+p)
+          info(prefix+"     - "+p.asString)
         }
 
         descendents = probs.map(p => new OrNode(cm, Some(this), p))
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index b02063dd4eac34a78e5b10e7910b42aefcd5ace4..501004cfaceac30fdd04b0e5b9d701c4c75b0de1 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -217,7 +217,7 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
         val app = an.ri
         s"(${n.cost.asString}) ${indent(app)}"
       case on: OrNode =>
-        val p = on.p
+        val p = on.p.asString(ctx)
         s"(${n.cost.asString}) ${indent(p)}"
     }