diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 0a43181e48c616a4789ef61bf7b57f2ee8843c05..e0ca64b78dff385aad774b86f44315b16dc7bb83 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -8,7 +8,7 @@ import leon.purescala.Common._
 // Defines a synthesis triple of the form:
 // ⟦ as ⟨ C | phi ⟩ xs ⟧
 case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifier]) {
-  override def toString = "⟦ "+as.mkString(";")+", "+(if (pc != BooleanLiteral(true)) pc+" ᚒ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+  override def toString = "⟦ "+as.mkString(";")+", "+(if (pc != BooleanLiteral(true)) pc+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
 }
 
 object Problem {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 1714ba991e0e7a629decddf59a278b6975b4b6fe..a6ea6b654397376802d8c98c8010bc7645f9cd65 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -107,7 +107,11 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       simplifyLets _
     )
 
-    val chooseToExprs = solutions.map { case (ch, sol) => (ch, simplifiers.foldLeft(sol.toExpr){ (x, sim) => sim(x) }) }
+    def simplify(e: Expr): Expr = simplifiers.foldLeft(e){ (x, sim) => sim(x) }
+
+    val chooseToExprs = solutions.map {
+      case (ch, sol) => (ch, simplify(sol.toExpr))
+    }
 
     if (inPlace) {
       for (file <- ctx.files) {