Cosmetics

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 {

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) {