diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 9594b704aa7984dbbb73d2a2dcf55b97b14cdeda..bd6ee1c5d1ba781a1e839c4757c15b06f1362276 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -501,6 +501,7 @@ object Trees {
         somethingChanged = true
         if(newEx.getType == Untyped) {
           Settings.reporter.warning("REPLACING WITH AN UNTYPED EXPRESSION !")
+          Settings.reporter.warning("Here's the new expression: " + newEx)
         }
         newEx
       }
@@ -980,9 +981,6 @@ object Trees {
         println("Rewriting the following PM: " + e)
 
         val condsAndRhs = for(cse <- cases) yield {
-          // println("For this case: " + cse)
-          // println("Map: " + mapForPattern(scrut, cse.pattern))
-          // println("Cond: " + conditionForPattern(scrut, cse.pattern))
           val map = mapForPattern(scrut, cse.pattern)
           val patCond = conditionForPattern(scrut, cse.pattern)
           val realCond = cse.theGuard match {
@@ -993,13 +991,11 @@ object Trees {
           (realCond, newRhs)
         } 
 
-        val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(m.getType))((p1, ex) => {
-          IfExpr(p1._1, p1._2, ex)
+        val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(bestRealType(m.getType)))((p1, ex) => {
+          IfExpr(p1._1, p1._2, ex).setType(m.getType)
         })
-        println(condsAndRhs)
-        println(bigIte)
-
-        Some(e)
+        //println(condsAndRhs)
+        Some(bigIte)
       }
       case _ => None
     }
diff --git a/src/purescala/TypeTrees.scala b/src/purescala/TypeTrees.scala
index 69ee4a306b98dc5b4dc9663f00873dcd4c99b253..3441a0104be6f5cf410a287e9875a7c8b6fae574 100644
--- a/src/purescala/TypeTrees.scala
+++ b/src/purescala/TypeTrees.scala
@@ -35,6 +35,17 @@ object TypeTrees {
     override def toString: String = PrettyPrinter(this)
   }
 
+  // Sort of a quick hack...
+  def bestRealType(t: TypeTree) : TypeTree = t match {
+    case c: ClassType if c.classDef.isInstanceOf[CaseClassDef] => {
+      c.classDef.parent match {
+        case None => scala.Predef.error("Asking for real type of a case class without abstract parent")
+        case Some(p) => AbstractClassType(p)
+      }
+    }
+    case other => other
+  }
+
   def leastUpperBound(t1: TypeTree, t2: TypeTree): TypeTree = (t1,t2) match {
     case (c1: ClassType, c2: ClassType) => {
       import scala.collection.immutable.Set
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 258fc36104c5967b1f62cb898e9f0d315539ed45..98aab5879d7447d5447605c5aa79f4d45c4ad86f 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -360,7 +360,10 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstr
 
     var z3Vars: Map[String, Z3AST] = initialMap
 
-    def rec(ex: Expr): Z3AST = ex match {
+    def rec(ex: Expr): Z3AST = { 
+      println("Stacking up call for:")
+      println(ex)
+      val recResult = (ex match {
       case Let(i, e, b) => {
         val re = rec(e)
         z3Vars = z3Vars + (i.uniqueName -> re)
@@ -368,6 +371,11 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstr
         z3Vars = z3Vars - i.uniqueName
         rb
       }
+      case e @ Error(_) => {
+        val tpe = e.getType
+        val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
+        newAST
+      }
       case v@Variable(id) => z3Vars.get(id.uniqueName) match {
         case Some(ast) => ast
         case None => {
@@ -375,6 +383,9 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstr
             scala.Predef.error("Error in formula being translated to Z3: identifier " + id + " seems to have escaped its let-definition")
           }
           val newAST = z3.mkFreshConst(id.name, typeToSort(v.getType))
+          println("*** new ID ***")
+          println(newAST)
+          println(typeToSort(v.getType))
           z3Vars = z3Vars + (id.uniqueName -> newAST)
           newAST
         }
@@ -408,9 +419,15 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstr
         constructor(args.map(rec(_)): _*)
       }
       case c@CaseClassSelector(_, cc, sel) => {
+        println("### NOW COMES A SELECTOR ! ###")
         val selector = adtFieldSelectors(sel)
+        println(selector)
         selector(rec(cc))
       }
+      case c@CaseClassInstanceOf(ccd, e) => {
+        val tester = adtTesters(ccd)
+        tester(rec(e))
+      }
       case f@FunctionInvocation(fd, args) if functionDefToDef.isDefinedAt(fd) => {
         abstractedFormula = true
         z3.mkApp(functionDefToDef(fd), args.map(rec(_)): _*)
@@ -464,6 +481,12 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstr
         reporter.warning("Can't handle this in translation to Z3: " + ex)
         throw new CantTranslateException
       }
+    })
+    println("Encoding of:")
+    println(ex)
+    println("...was encoded as:")
+    println(recResult)
+    recResult
     }
 
     try {
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index ce313c307069ab676242e8a7288be2f9a99c65a3..98bf934b2c1900ce8f681de00f21e96a421d5532 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -93,6 +93,13 @@ object BinarySearchTree {
     }
   } ensuring (contents(_) == contents(tree) ++ Set(value))
 
+  def cleanInsert(tree: Tree, value: Int) : Tree = (tree match {
+    case Leaf() => Node(Leaf(), value, Leaf())
+    case Node(l, v, r) if v < value => Node(l, v, insert(r, value))
+    case Node(l, v, r) if v > value => Node(insert(l, value), v, r)
+    case n @ Node(l, v, r) if v == value => n
+  }) ensuring(contents(_) == contents(tree) ++ Set(value))
+
   def insertSorted(tree: Tree, value: Int): Node = {
     require(isSorted(tree).sorted)
     tree match {
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 130955bc664c72a02963c83910b3a9262e873e00..fc1eac3a14e3ffde06c95472e8364c34e6cc1ab1 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -17,6 +17,10 @@ object ListWithSize {
       case Cons(x, xs) => Set(x) ++ content(xs)
     }
 
+    def sizeAndContent(l: List) : Boolean = {
+      size(l) == 0 || content(l) != Set.empty[Int]
+    } ensuring(_ == true)
+
     // proved with unrolling=1
     def funnyCons(x: Int, l: List) : List = (l match {
         case Nil() => Cons(x, Nil())