diff --git a/mytest/Epsilon1.scala b/mytest/Epsilon1.scala
index 1d83db59a4cee11aa8256f46e42e6d6f8018ee5e..827c1e6e5a1de4363b7fc61bf7ceeba07c85ac2e 100644
--- a/mytest/Epsilon1.scala
+++ b/mytest/Epsilon1.scala
@@ -2,7 +2,11 @@ import leon.Utils._
 
 object Epsilon1 {
 
-  def foo(x: Int): Int = {
+  def greater(x: Int): Int = {
+    epsilon((y: Int) => y > x)
+  } ensuring(_ >= x)
+
+  def greaterWrong(x: Int): Int = {
     epsilon((y: Int) => y >= x)
   } ensuring(_ > x)
 
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 20e1f1daccb95593219fb37cdf155aa1ccf15941..2e10af6c538aad94f4414c8e936b50caf90b219c 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -808,7 +808,16 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
           } else Seq()
         } else Seq()
       }).toMap
-      val asMap = modelToMap(model, variables) ++ functionsAsMap
+      val constantFunctionsAsMap: Map[Identifier, Expr] = model.getModelConstantInterpretations.flatMap(p => {
+        if(isKnownDecl(p._1)) {
+          val fd = functionDeclToDef(p._1)
+          if(!fd.hasImplementation) {
+            Seq((fd.id, fromZ3Formula(model, p._2, Some(fd.returnType))))
+          } else Seq()
+        } else Seq()
+      }).toMap
+      //val undefinedFunctionIds = functionMap.keys.filterNot(fd => fd.hasImplementation || !fd.args.isEmpty).map(_.id) 
+      val asMap = modelToMap(model, variables) ++ functionsAsMap ++ constantFunctionsAsMap
       model.delete
       lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
       val evalResult = eval(asMap, formula, evaluator)