diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index e561579409b0c4779bf8a8043de09a91bc6207ac..da031c5e71e4a56b146cdc359bcfc10ab8c92fbd 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -3,6 +3,7 @@ package synthesis
 
 import purescala.Common._
 import purescala.Trees._
+import purescala.TypeTrees._
 
 object Rules {
   def all(synth: Synthesizer) = List(
@@ -65,16 +66,19 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
 class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
   def isApplicable(p: Problem, parent: Task): List[Task] = {
     if (p.as.isEmpty) {
+
+      val tpe = TupleType(p.xs.map(_.getType))
+
       synth.solveSAT(p.phi) match {
         case (Some(true), model) =>
           val onSuccess: List[Solution] => Solution = { 
-            case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)))
+            case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe))
           }
 
           List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
         case (Some(false), model) =>
           val onSuccess: List[Solution] => Solution = { 
-            case Nil => Solution(BooleanLiteral(false), BooleanLiteral(false))
+            case Nil => Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))
           }
 
           List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
diff --git a/testcases/Choose.scala b/testcases/Choose.scala
index 3d7740348902a92d9e5610cf726ed52b1770b312..336299a0f6be52b71d7f57039af9bc7c5b70a690 100644
--- a/testcases/Choose.scala
+++ b/testcases/Choose.scala
@@ -3,6 +3,7 @@ import leon.Utils._
 object ChooseTest {
 
   def c0(): Int = choose{ (x1: Int) => x1 > 13 }
+  def b0(): Int = choose{ (x1: Int) => x1 > 13 && x1 < 2 }
 
   def c1(a: Int): Int = choose{ (x1: Int) => x1 > a }
   def c2(a: Int): (Int, Int) = choose{ (x1: Int, x2: Int) => x1 > a && x2 > a }