diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 04db1ab18e832d445671f2b6ddebb5d78aadb60e..58e4f8162ac2acce8dd229c6dc1cef6770f11c7a 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/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)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index b2792da85cbc65a4f7cc9fdd1a53519c7434c352..e1dab45ee6c22c537fcabf04aa89c48e87c82d5f 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/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)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 9361e2c92de1645ba8040177270e1a8a686e43b1..a4ab6b46f9f62e92b45959393d959d1ba9c83d28 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/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:")
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index 551317142c14811da077cca906646e03d109abaa..3a797a9b1fd563bed2f0e2b55c4424b17b3ca0cf 100644
--- a/testcases/synthesis/Spt.scala
+++ b/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