diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 72c62ef152b58b54a563ceb9e238c129af5a565c..0f3204e7027257d6dbcaf5c16234accd918347ca 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -85,10 +85,11 @@ object Evaluator {
             }
           }
 
-          if(!fd.hasBody) {
+          if(!fd.hasBody && !context.isDefinedAt(fd.id)) {
             throw RuntimeErrorEx("Evaluation of function with unknown implementation.")
           }
-          val callResult = rec(frame, matchToIfThenElse(fd.body.get))
+          val body = fd.body.getOrElse(context(fd.id))
+          val callResult = rec(frame, matchToIfThenElse(body))
 
           if(fd.hasPostcondition) {
             val freshResID = FreshIdentifier("result").setType(fd.returnType)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 7745edc76851e1bcebd621c2a2f80d31522b74c7..5dc1f673e60a33a8825b4a5ea99f1ccaa959b68e 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -781,19 +781,30 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
     import Evaluator._
 
     val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
-    println(functionsModel.toList.map(p => p._1 + " -> " + {
-      val (cses, default) = p._2 
-      val ite = cses.foldLeft(fromZ3Formula(model, default))((expr, q) => IfExpr(
-                      And(
-                        q._1.zip(functionDeclToDef(p._1).args).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id)))
-                      ),
-                      fromZ3Formula(model, q._2),
-                      expr))
-      ite.toString
-    }).mkString("\n"))
+
+//    println(functionsModel.toList.map(p => p._1 + " -> " + {
+//      val (cses, default) = p._2 
+//      val ite = cses.foldLeft(fromZ3Formula(model, default))((expr, q) => IfExpr(
+//                      And(
+//                        q._1.zip(functionDeclToDef(p._1).args).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id)))
+//                      ),
+//                      fromZ3Formula(model, q._2),
+//                      expr))
+//
 
     if(!forceStop) {
-      val asMap = modelToMap(model, variables)
+      val functionsAsMap = functionsModel.map(p => {
+        val fd = functionDeclToDef(p._1)
+        val (cses, default) = p._2 
+        val ite = cses.foldLeft(fromZ3Formula(model, default))((expr, q) => IfExpr(
+                        And(
+                          q._1.zip(fd.args).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id)))
+                        ),
+                        fromZ3Formula(model, q._2),
+                        expr))
+        (fd.id, ite)
+      })
+      val asMap = modelToMap(model, variables) ++ functionsAsMap
       model.delete
       lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
       val evalResult = eval(asMap, formula, evaluator)