diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 5dc1f673e60a33a8825b4a5ea99f1ccaa959b68e..20e1f1daccb95593219fb37cdf155aa1ccf15941 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -793,17 +793,21 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
 //
 
     if(!forceStop) {
-      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 functionsAsMap: Map[Identifier, Expr] = functionsModel.flatMap(p => {
+        if(isKnownDecl(p._1)) {
+          val fd = functionDeclToDef(p._1)
+          if(!fd.hasImplementation) {
+            val (cses, default) = p._2 
+            val ite = cses.foldLeft(fromZ3Formula(model, default, Some(fd.returnType)))((expr, q) => IfExpr(
+                            And(
+                              q._1.zip(fd.args).map(a12 => Equals(fromZ3Formula(model, a12._1, Some(a12._2.tpe)), Variable(a12._2.id)))
+                            ),
+                            fromZ3Formula(model, q._2, Some(fd.returnType)),
+                            expr))
+            Seq((fd.id, ite))
+          } else Seq()
+        } else Seq()
+      }).toMap
       val asMap = modelToMap(model, variables) ++ functionsAsMap
       model.delete
       lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")