diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
index 1f9d473e62346e1d83a70ae39a171cff0dade354..2e0a7a2bb1959f720e62ab47f4c6783436e4d28b 100644
--- a/src/main/scala/leon/evaluators/AbstractEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
@@ -122,22 +122,26 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
         }
       }
       callResult
+
     case Let(i, ex, b) =>
       val (first, second) = e(ex)
       e(b)(rctx.withNewVar(i, (first, second)), gctx)
+
     case Application(caller, args) =>
-      underlying.e(caller) match {
+      val (ecaller, tcaller) = e(caller)
+      val nargs = args map e
+      val (eargs, targs) = nargs.unzip
+      val abs_value = Application(tcaller, targs)
+      if (ExprOps.isValue(ecaller) && (eargs forall ExprOps.isValue)) {
+        (underlying.e(Application(ecaller, eargs)), abs_value)
+      } else ecaller match {
         case l @ Lambda(params, body) =>
-          val newArgs = args.map(e)
-          val mapping = (params map { _.id } zip newArgs).toMap
+          val mapping = (params map (_.id) zip nargs).toMap
           e(body)(rctx.withNewVars2(mapping), gctx)
-        case FiniteLambda(mapping, dflt, _) =>
-          mapping.find { case (pargs, res) =>
-            (args zip pargs).forall(p => underlying.e(Equals(p._1, p._2)) == BooleanLiteral(true))
-          }.map{ case (key, value) => (value, value)}.getOrElse((dflt, dflt))
-        case f =>
-          throw EvalError("Cannot apply non-lambda function " + f.asString)
+        case _ =>
+          (Application(ecaller, eargs), abs_value)
       }
+
     case Operator(es, builder) =>
       val (ees, ts) = es.map(e).unzip
       if(ees forall ExprOps.isValue) {
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 8b84cd05eaff99293b6db2144ef64ece16f552aa..e295adafbb5468eba718b803ca7477d3703a7394 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -171,7 +171,7 @@ object SolverFactory {
   }
 
   lazy val hasNativeZ3 = try {
-    new _root_.z3.scala.Z3Config
+    _root_.z3.Z3Wrapper.withinJar()
     true
   } catch {
     case _: java.lang.UnsatisfiedLinkError =>
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 2a5c414f18b5ca07f6d85009346b53389c13e4f1..9907f03945440723d8a2829992197a1ae0406d46 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -47,14 +47,6 @@ trait AbstractZ3Solver extends Solver {
     }
   }
 
-  // FIXME: (dirty?) hack to bypass z3lib bug.
-  // Uses the unique AbstractZ3Solver to ensure synchronization (no assumption on context).
-  protected[leon] val z3cfg : Z3Config =
-    AbstractZ3Solver.synchronized(new Z3Config(
-      "MODEL"             -> true,
-      "TYPE_CHECK"        -> true,
-      "WELL_SORTED_CHECK" -> true
-    ))
   toggleWarningMessages(true)
 
   protected[leon] var z3 : Z3Context = null
@@ -105,7 +97,11 @@ trait AbstractZ3Solver extends Solver {
     if (!isInitialized) {
       val timer = context.timers.solvers.z3.init.start()
 
-      z3 = new Z3Context(z3cfg)
+      z3 = new Z3Context(
+        "MODEL"             -> true,
+        "TYPE_CHECK"        -> true,
+        "WELL_SORTED_CHECK" -> true
+      )
 
       functions.clear()
       lambdas.clear()
@@ -657,7 +653,7 @@ trait AbstractZ3Solver extends Solver {
 
               case ft @ FunctionType(fts, tt) => lambdas.getB(ft) match {
                 case None => simplestValue(ft)
-                case Some(decl) => model.getModelFuncInterpretations.find(_._1 == decl) match {
+                case Some(decl) => model.getFuncInterpretations.find(_._1 == decl) match {
                   case None => simplestValue(ft)
                   case Some((_, mapping, elseValue)) =>
                     val leonElseValue = rec(elseValue, tt)
@@ -692,7 +688,8 @@ trait AbstractZ3Solver extends Solver {
               case tpe @ SetType(dt) =>
                 model.getSetValue(t) match {
                   case None => unsound(t, "invalid set AST")
-                  case Some(set) =>
+                  case Some((_, false)) => unsound(t, "co-finite set AST")
+                  case Some((set, true)) =>
                     val elems = set.map(e => rec(e, dt))
                     FiniteSet(elems, dt)
                 }
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 31731dca30d02281fae6883f139b29dbd96f18d9..6100c8c3c6bad2b4554c1ab9eac9667894812ca2 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -99,7 +99,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
     }
 
     def isValidExample(ex: Example): Boolean = {
-      if(this.keepAbstractExamples) return true // TODO: Abstract interpretation here ?
+      if (this.keepAbstractExamples) return true // TODO: Abstract interpretation here ?
       val (mapping, cond) = ex match {
         case io: InOutExample =>
           (Map((p.as zip io.ins) ++ (p.xs zip io.outs): _*), p.pc and p.phi)
diff --git a/unmanaged/64/scalaz3-unix-64b-2.1.jar b/unmanaged/64/scalaz3_2.11-3.0.jar
similarity index 51%
rename from unmanaged/64/scalaz3-unix-64b-2.1.jar
rename to unmanaged/64/scalaz3_2.11-3.0.jar
index db94f26380b6b5a7eaab64ed730b03d48cf23f46..f1d94106f61ce57a4925d647ac329ad32795f657 100644
Binary files a/unmanaged/64/scalaz3-unix-64b-2.1.jar and b/unmanaged/64/scalaz3_2.11-3.0.jar differ