Kill Assert as we know it for now. Keep the trivial base case.

Assert may not be helping at all. It is trimming crucial information
from the formula, i.e.

[[ a,b ;  a = size(x) AND a+1 = size(b); x ]].

Applying assert will remove 'a+1 = size(b)' from phi and push it as
precondition when reconstructing a solution. The subproblem will become:

[[ a,b ; a = size(x) ; x]]

The input 'b' is then removed by applying Unused-Input.

src/main/scala/leon/synthesis/Rules.scala

@@ -137,6 +137,8 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) {
           if (others.isEmpty) {
             RuleSuccess(Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
           } else {
+            /*
+             * Disable for now, it is not that useful anyway
             val onSuccess: List[Solution] => Solution = { 
               case List(s) => Solution(And(s.pre +: exprsA), s.term)
               case _ => Solution.none
@@ -145,6 +147,8 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) {
             val sub = p.copy(phi = And(others))
 
             RuleDecomposed(List(sub), onSuccess)
+            */
+            RuleInapplicable
           }
         } else {
           RuleInapplicable

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -55,11 +55,11 @@ class Synthesizer(val r: Reporter,
       // current solution
       if (task.minComplexity < bestSolutionSoFar().complexity) {
         if (!subProblems.isEmpty) {
-          val name = Option(task.rule).map(_.name).getOrElse("root")
-          println("["+name+"] Got: "+task.problem)
-          println("["+name+"] Decomposed into:")
+          val prefix = "[%-20s] ".format(Option(task.rule).map(_.name).getOrElse("root"))
+          println(prefix+"Got: "+task.problem)
+          println(prefix+"Decomposed into:")
           for(p <- subProblems) {
-            println("["+name+"]  - "+p)
+            println(prefix+" - "+p)
           }
         }