Fix assert, Add example, add more debug output for last rule

src/main/scala/leon/purescala/Trees.scala

@@ -1059,6 +1059,8 @@ object Trees {
           None
         }
       }
+      case letTuple @ LetTuple(ids, e, body) =>
+      None
       case _ => None 
     }
     searchAndReplace(simplerLet)(expr)

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

@@ -131,7 +131,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
 
         if (!exprsA.isEmpty) {
           if (others.isEmpty) {
-            List(task.solveUsing(this, Solution(And(exprsA), BooleanLiteral(true), 150), 150))
+            List(task.solveUsing(this, Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id))))), 150))
           } else {
             val onSuccess: List[Solution] => Solution = { 
               case List(s) => Solution(And(s.pre +: exprsA), s.term, 150)

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

@@ -32,6 +32,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
 
       alternatives.find(_.isSuccess) match {
         case Some(ss) =>
+          info(" => "+ss.rule+" succeeded")
           ss.succeeded()
         case None =>
           info(" => Possible Next Steps:")

testcases/synthesis/Spt.scala

@@ -13,6 +13,8 @@ object SynthesisProceduresToolkit {
 
   def e5(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) => Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3,  x4)))
 
+  def e6(a: Nat, b: Nat): (Nat, NatList) = choose( (x: Nat, y: NatList) => a == Succ(b))
+
   abstract class Nat
   case class Z() extends Nat
   case class Succ(n: Nat) extends Nat