diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 2e896736f7fb49972389c0058432f2a1e01d7fff..6594eb07e239876a5e046ebb3a99606f91225a93 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -663,7 +663,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
   override def foundAnswer(res: Option[Boolean], model: Model = Model.empty, core: Set[Expr] = Set.empty) = {
     super.foundAnswer(res, model, core)
 
-    if (!interrupted && res == None && model == None) {
+    if (!interrupted && res.isEmpty && model.isEmpty) {
       reporter.ifDebug { debug =>
         debug("Unknown result!?")
       }
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index d87559f935e637cc9b950db97e99ae4f58bc6ab5..fa3352b1ef2b5810afd063e0eb28f503e9d4a57d 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -10,18 +10,11 @@ import _root_.z3.scala._
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
-import purescala.Constructors._
-import purescala.Quantification._
 import purescala.ExprOps._
 import purescala.Types._
 
 import solvers.templates._
 import solvers.combinators._
-import Template._
-
-import evaluators._
-
-import termination._
 
 class FairZ3Solver(val context: LeonContext, val program: Program)
   extends AbstractZ3Solver
@@ -211,7 +204,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
   override def foundAnswer(res: Option[Boolean], model: Model = Model.empty, core: Set[Expr] = Set.empty) = {
     super.foundAnswer(res, model, core)
 
-    if (!interrupted && res == None && model == None) {
+    if (!interrupted && res.isEmpty && model.isEmpty) {
       reporter.ifDebug { debug => 
         if (solver.getReasonUnknown != "canceled") {
           debug("Z3 returned unknown: " + solver.getReasonUnknown)
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 7085ed7d9c5cf929dc0220b492eceafd68a16ca1..ec681763eec062c7b6a29267f9ed209b4646460c 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -419,7 +419,7 @@ case object StringRender extends Rule("StringRender") {
             .excludeFunction(hctx.functionContext)
             .prettyPrintersForType(input.getType)(hctx, hctx.program)
             .map(l => (application(l, Seq(input)), List[Identifier]())) // Use already pre-defined pretty printers.
-          val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(fd, _)), _) if fd == hctx.functionContext => 0 case _ => 1}
+          val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(tfd, _)), _) if tfd.fd == hctx.functionContext => 0 case _ => 1}
           val exprs2 = ctx.abstractStringConverters.getOrElse(input.getType, Nil).map(f => (f(input), List[Identifier]()))
           val defaultConverters: Stream[WithIds[Expr]] = exprs1.toStream #::: exprs2.toStream
           val recursiveConverters: Stream[WithIds[Expr]] =