diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 8edf77f51529dee7cb42c172e1ecbd78b6ffdd5c..6daf732ef77929267019a6a65008f30e7e72d5e4 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -394,7 +394,7 @@ object DefOps {
     import leon.utils.SearchSpace.reachable
     reachable(
       sources,
-      (tfd: TypedFunDef) => functionCallsOf(tfd.fd.fullBody) map { _.tfd },
+      (tfd: TypedFunDef) => functionCallsOf(tfd.fullBody) map { _.tfd },
       limit
     )
   }
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index ee0f6a03c643a7bef492ef320171504acfbe972d..fe162c455be7a80d6c062c767c249a5412acb77e 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -498,6 +498,15 @@ object Definitions {
     private var trCache = Map[Expr, Expr]()
     private var postCache = Map[Expr, Expr]()
 
+    def fullBody = {
+      val fb = fd.fullBody
+      trCache.getOrElse(fb, {
+        val res = translated(fb)
+        trCache += fb -> res
+        res
+      })
+    }
+
     def body = fd.body.map { b =>
       trCache.getOrElse(b, {
         val res = translated(b)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 47cebfd05e98c368be153873f30f9dde818da1e1..43e1dd91c0a35bd027d65194863dae2ed5455307 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -52,7 +52,6 @@ trait SMTLIBTarget {
   val selectors    = new IncrementalBijection[(TypeTree, Int), SSymbol]()
   val testers      = new IncrementalBijection[TypeTree, SSymbol]()
   val variables    = new IncrementalBijection[Identifier, SSymbol]()
-  val classes      = new IncrementalBijection[CaseClassDef, SSymbol]()
   val sorts        = new IncrementalBijection[TypeTree, Sort]()
   val functions    = new IncrementalBijection[TypedFunDef, SSymbol]()
 
@@ -646,7 +645,6 @@ trait SMTLIBTarget {
       out.write("\n")
       out.flush()
     }
-
     interpreter.eval(cmd) match {
       case err@ErrorResponse(msg) if !interrupted =>
         reporter.fatalError("Unexpected error from smt-"+targetName+" solver: "+msg)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
index 9fd5eeba2884fc9d6d47a3726a9ed07e6819dea4..0600de6cb149016dd08f2d8092c799ee3db82fc9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
@@ -26,7 +26,7 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
         )
       }
 
-      val (smtFunDecls, smtBodies) = funs.toSeq.collect {
+      val smtFunDecls = funs.toSeq.collect {
         case tfd if !functions.containsA(tfd) && tfd.params.nonEmpty =>
           val id = if (tfd.tps.isEmpty) {
             tfd.id
@@ -35,17 +35,19 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
           }
           val sym = id2sym(id)
           functions +=(tfd, sym)
-          (
-            FunDec(
-              sym,
-              tfd.params map { p => SortedVar(id2sym(p.id), declareSort(p.getType)) },
-              declareSort(tfd.returnType)
-            ),
-            toSMT(matchToIfThenElse(tfd.body.get))(tfd.params.map { p =>
-              (p.id, id2sym(p.id): Term)
-            }.toMap)
-            )
-      }.unzip
+          FunDec(
+            sym,
+            tfd.params map { p => SortedVar(id2sym(p.id), declareSort(p.getType)) },
+            declareSort(tfd.returnType)
+          )
+      }
+      val smtBodies = smtFunDecls map { case FunDec(sym, _, _) =>
+        val tfd = functions.toA(sym)
+        toSMT(matchToIfThenElse(tfd.body.get))(tfd.params.map { p =>
+          (p.id, id2sym(p.id): Term)
+        }.toMap
+      )
+      }
 
       if (smtFunDecls.nonEmpty) sendCommand(DefineFunsRec(smtFunDecls, smtBodies))
       functions.toB(tfd)