diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor.java
deleted file mode 100644
index 76030a6129ac4c62115daf62162bffb658c891fd..0000000000000000000000000000000000000000
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor.java
+++ /dev/null
@@ -1,50 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.codegen.runtime;
-
-import java.util.List;
-import java.util.LinkedList;
-import java.util.HashMap;
-
-public class LeonCodeGenRuntimeHenkinMonitor extends LeonCodeGenRuntimeMonitor {
-  private final HashMap<Integer, List<Tuple>> tpes = new HashMap<Integer, List<Tuple>>();
-  private final HashMap<Class<?>, List<Tuple>> lambdas = new HashMap<Class<?>, List<Tuple>>();
-  public final boolean checkForalls;
-
-  public LeonCodeGenRuntimeHenkinMonitor(int maxInvocations, boolean checkForalls) {
-    super(maxInvocations);
-    this.checkForalls = checkForalls;
-  }
-
-  public LeonCodeGenRuntimeHenkinMonitor(int maxInvocations) {
-    this(maxInvocations, false);
-  }
-
-  public void add(int type, Tuple input) {
-    if (!tpes.containsKey(type)) tpes.put(type, new LinkedList<Tuple>());
-    tpes.get(type).add(input);
-  }
-
-  public void add(Class<?> clazz, Tuple input) {
-    if (!lambdas.containsKey(clazz)) lambdas.put(clazz, new LinkedList<Tuple>());
-    lambdas.get(clazz).add(input);
-  }
-
-  public List<Tuple> domain(Object obj, int type) {
-    List<Tuple> domain = new LinkedList<Tuple>();
-    if (obj instanceof FiniteLambda) {
-      FiniteLambda l = (FiniteLambda) obj;
-      for (Tuple key : l.mapping.keySet()) {
-        domain.add(key);
-      }
-    } else if (obj instanceof Lambda) {
-      List<Tuple> lambdaDomain = lambdas.get(obj.getClass());
-      if (lambdaDomain != null) domain.addAll(lambdaDomain);
-    }
-
-    List<Tuple> tpeDomain = tpes.get(type);
-    if (tpeDomain != null) domain.addAll(tpeDomain);
-
-    return domain;
-  }
-}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 4cfbc037c1054b2c7c408ac8202ab0ea2598a873..14b8f5cdf5fb00237282ac231ed881b9179e053d 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -87,7 +87,6 @@ trait CodeGeneration {
   private[codegen] val GenericValuesClass        = "leon/codegen/runtime/GenericValues"
   private[codegen] val MonitorClass              = "leon/codegen/runtime/Monitor"
   private[codegen] val NoMonitorClass            = "leon/codegen/runtime/NoMonitor"
-  private[codegen] val HenkinClass               = "leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor"
   private[codegen] val StrOpsClass               = "leon/codegen/runtime/StrOps"
 
   def idToSafeJVMName(id: Identifier) = {
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index ca2510451cf0883679ddcca870ac1f3a1a9ec7b4..9cef8cd0452fa6596f1ebc2e86ed5d6f4d394c1f 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -169,7 +169,7 @@ class CompilationUnit(val ctx: LeonContext,
   def getMonitor(model: solvers.Model, maxInvocations: Int): Monitor = {
     val bodies = model.toSeq.filter { case (id, v) => abstractFunDefs(id) }.toMap
     val domains = model match {
-      case hm: solvers.HenkinModel => Some(hm.doms)
+      case hm: solvers.PartialModel => Some(hm.domains)
       case _ => None
     }
 
diff --git a/src/main/scala/leon/codegen/runtime/Monitor.scala b/src/main/scala/leon/codegen/runtime/Monitor.scala
index 7f5bbe00659c7623287d6039d4cad95ab198df75..0861ce3bc406711e5d4d460c5e5cacdb7eb09cd0 100644
--- a/src/main/scala/leon/codegen/runtime/Monitor.scala
+++ b/src/main/scala/leon/codegen/runtime/Monitor.scala
@@ -11,7 +11,7 @@ import purescala.Common._
 import purescala.Types._
 import purescala.TypeOps._
 import purescala.ExprOps.{valuateWithModel, replaceFromIDs, variablesOf}
-import purescala.Quantification.{extractQuorums, HenkinDomains}
+import purescala.Quantification.{extractQuorums, Domains}
 
 import codegen.CompilationUnit
 
@@ -56,7 +56,7 @@ class NoMonitor extends Monitor {
   }
 }
 
-class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Identifier, Expr], domains: Option[HenkinDomains] = None) extends Monitor {
+class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Identifier, Expr], domains: Option[Domains] = None) extends Monitor {
 
   private[this] var invocations = 0
 
diff --git a/src/main/scala/leon/evaluators/ContextualEvaluator.scala b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
index 76f5c500890135fc7fc7d3e75814c2d92020e2b0..51205fc5c8221c439801786b3c9ee3cc7b2e3287 100644
--- a/src/main/scala/leon/evaluators/ContextualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
@@ -8,7 +8,7 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.Types._
-import solvers.{HenkinModel, Model}
+import solvers.{PartialModel, Model}
 
 abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps: Int) extends Evaluator(ctx, prog) with CEvalHelpers {
 
@@ -60,8 +60,8 @@ private[evaluators] trait CEvalHelpers {
   /* This is an effort to generalize forall to non-det. solvers
     def forallInstantiations(gctx:GC, fargs: Seq[ValDef], conj: Expr) = {
 
-      val henkinModel: HenkinModel = gctx.model match {
-        case hm: HenkinModel => hm
+      val henkinModel: PartialModel = gctx.model match {
+        case hm: PartialModel => hm
         case _ => throw EvalError("Can't evaluate foralls without henkin model")
       }
 
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 2ebb5ade5390801bd24e5f2eb0f464ab9f0e2d38..689980682c86d03bb715b50e0dd2ff6ce530c331 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -14,7 +14,7 @@ import purescala.Common._
 import purescala.Expressions._
 import purescala.Definitions._
 import purescala.DefOps
-import solvers.{HenkinModel, Model, SolverFactory}
+import solvers.{PartialModel, Model, SolverFactory}
 import solvers.combinators.UnrollingProcedure
 import scala.collection.mutable.{Map => MutableMap}
 import scala.concurrent.duration._
@@ -540,7 +540,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
           solver.assertCnstr(cnstr)
 
           gctx.model match {
-            case pm: HenkinModel =>
+            case pm: PartialModel =>
               val quantifiers = fargs.map(_.id).toSet
               val quorums = extractQuorums(body, quantifiers)
 
@@ -551,7 +551,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
                     case ev => ev
                   }
 
-                  val domain = pm.domain(matcher)
+                  val domain = pm.domains.get(matcher)
                   args.zipWithIndex.flatMap {
                     case (Variable(id),idx) if quantifiers(id) =>
                       Some(id -> domain.map(cargs => path -> cargs(idx)))
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index 36509832dc0cee6ad8c54ef43af1d73d1b1ae864..3fff6e523a945b23761a232094c9327ba276e201 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -13,7 +13,7 @@ import purescala.Definitions.{TypedFunDef, Program}
 import purescala.Expressions._
 import purescala.Quantification._
 
-import leon.solvers.{SolverFactory, HenkinModel}
+import leon.solvers.{SolverFactory, PartialModel}
 import leon.solvers.combinators.UnrollingProcedure
 import leon.utils.StreamUtils._
 
@@ -160,7 +160,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
         solver.assertCnstr(cnstr)
 
         gctx.model match {
-          case pm: HenkinModel =>
+          case pm: PartialModel =>
             val quantifiers = fargs.map(_.id).toSet
             val quorums = extractQuorums(body, quantifiers)
 
@@ -173,7 +173,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
                 }
 
                 optMatcher.toSeq.flatMap { matcher =>
-                  val domain = pm.domain(matcher)
+                  val domain = pm.domains.get(matcher)
                   args.zipWithIndex.flatMap {
                     case (Variable(id),idx) if quantifiers(id) =>
                       Some(id -> domain.map(cargs => path -> cargs(idx)))
diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index 3efdc9df7e5b92b0e5d87faf9205c1ef8f3e90af..297ee1fc95105dc55509aaf74439b3640c0c4ca9 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -70,11 +70,11 @@ object Quantification {
       (p: (Expr, Expr, Seq[Expr])) => p._3.collect { case Variable(id) if quantified(id) => id }.toSet)
   }
 
-  object HenkinDomains {
-    def empty = new HenkinDomains(Map.empty, Map.empty)
+  object Domains {
+    def empty = new Domains(Map.empty, Map.empty)
   }
 
-  class HenkinDomains (val lambdas: Map[Lambda, Set[Seq[Expr]]], val tpes: Map[TypeTree, Set[Seq[Expr]]]) {
+  class Domains (val lambdas: Map[Lambda, Set[Seq[Expr]]], val tpes: Map[TypeTree, Set[Seq[Expr]]]) {
     def get(e: Expr): Set[Seq[Expr]] = {
       val specialized: Set[Seq[Expr]] = e match {
         case FiniteLambda(mapping, _, _) => mapping.map(_._1).toSet
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 0257a0b7a7c5592215206eefbb6928c46cc9995f..16129a49080f8676d1101d790d39331b87fca095 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -1,7 +1,7 @@
 package leon.purescala
 
 import leon.purescala
-import leon.solvers.{ HenkinModel, Model, SolverFactory }
+import leon.solvers.{ Model, SolverFactory }
 import leon.LeonContext
 import leon.evaluators
 import leon.utils.StreamUtils
@@ -121,4 +121,4 @@ class SelfPrettyPrinter {
       }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/solvers/Model.scala b/src/main/scala/leon/solvers/Model.scala
index 820d0b12fe86a944f967039caf956e85c989e8c0..57f93655f5311655ffd1d479762dac839e750517 100644
--- a/src/main/scala/leon/solvers/Model.scala
+++ b/src/main/scala/leon/solvers/Model.scala
@@ -5,6 +5,7 @@ package solvers
 
 import purescala.Expressions._
 import purescala.Common.Identifier
+import purescala.Quantification.Domains
 import purescala.ExprOps._
 
 trait AbstractModel[+This <: Model with AbstractModel[This]]
@@ -80,3 +81,21 @@ object Model {
 class ModelBuilder extends AbstractModelBuilder[Model] {
   def result = new Model(mapBuilder.result)
 }
+
+class PartialModel(mapping: Map[Identifier, Expr], val domains: Domains)
+  extends Model(mapping)
+     with AbstractModel[PartialModel] {
+
+  override def newBuilder = new PartialModelBuilder(domains)
+}
+
+object PartialModel {
+  def empty = new PartialModel(Map.empty, Domains.empty)
+}
+
+class PartialModelBuilder(domains: Domains)
+  extends ModelBuilder
+     with AbstractModelBuilder[PartialModel] {
+
+  override def result = new PartialModel(mapBuilder.result, domains)
+}
diff --git a/src/main/scala/leon/solvers/QuantificationSolver.scala b/src/main/scala/leon/solvers/QuantificationSolver.scala
deleted file mode 100644
index 8ffe0a004cd23c39da6cd373774497ee78835974..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/solvers/QuantificationSolver.scala
+++ /dev/null
@@ -1,34 +0,0 @@
-package leon
-package solvers
-
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Quantification._
-import purescala.Definitions._
-import purescala.Types._
-
-class HenkinModel(mapping: Map[Identifier, Expr], val doms: HenkinDomains)
-  extends Model(mapping)
-     with AbstractModel[HenkinModel] {
-  override def newBuilder = new HenkinModelBuilder(doms)
-
-  def domain(expr: Expr) = doms.get(expr)
-}
-
-object HenkinModel {
-  def empty = new HenkinModel(Map.empty, HenkinDomains.empty)
-}
-
-class HenkinModelBuilder(domains: HenkinDomains)
-  extends ModelBuilder
-     with AbstractModelBuilder[HenkinModel] {
-  override def result = new HenkinModel(mapBuilder.result, domains)
-}
-
-trait QuantificationSolver extends Solver {
-  val program: Program
-
-  protected lazy val requireQuantification = program.definedFunctions.exists { fd =>
-    purescala.ExprOps.exists { case _: Forall => true case _ => false } (fd.fullBody)
-  }
-}
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index c76eb400bcfd0cb967b8982e6a484a295a89a270..8c57de44eeb0978384dd5ae6076ce24c1b3ea498 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -40,8 +40,7 @@ object UnrollingProcedure extends UnrollingProcedure
 trait AbstractUnrollingSolver[T]
   extends UnrollingProcedure
      with Solver
-     with EvaluatingSolver
-     with QuantificationSolver {
+     with EvaluatingSolver {
 
   val unfoldFactor     = context.findOptionOrDefault(optUnrollFactor)
   val feelingLucky     = context.findOptionOrDefault(optFeelingLucky)
@@ -214,7 +213,7 @@ trait AbstractUnrollingSolver[T]
     }
   }
 
-  private def getPartialModel: HenkinModel = {
+  private def getPartialModel: PartialModel = {
     val wrapped = solverGetModel
 
     val typeInsts = templateGenerator.manager.typeInstantiations
@@ -262,8 +261,8 @@ trait AbstractUnrollingSolver[T]
       })
     })
 
-    val domains = new HenkinDomains(lambdaDomains, typeDomains)
-    new HenkinModel(model.toMap, domains)
+    val domains = new Domains(lambdaDomains, typeDomains)
+    new PartialModel(model.toMap, domains)
   }
 
   private def getTotalModel: Model = {
diff --git a/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala b/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
index e636ff6a734e6d3180b3f661cc0d1e74ff691317..2b6984d00d989e6958da3c43930b9614436cffbf 100644
--- a/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
@@ -57,15 +57,18 @@ object Z3StringCapableSolver {
     }
   }
 }
+
 trait ForcedProgramConversion { self: Z3StringCapableSolver[_] =>
   override def convertProgram(p: Program): (Program, Option[Z3StringConversion]) = {
     Z3StringCapableSolver.convert(p, true)
   }
 }
 
-abstract class Z3StringCapableSolver[+TUnderlying <: Solver](val context: LeonContext, val program: Program,
-    val underlyingConstructor: (Program, Option[Z3StringConversion]) => TUnderlying)
-extends Solver {
+abstract class Z3StringCapableSolver[+TUnderlying <: Solver](
+  val context: LeonContext,
+  val program: Program,
+  val underlyingConstructor: (Program, Option[Z3StringConversion]) => TUnderlying) extends Solver {
+
   def convertProgram(p: Program): (Program, Option[Z3StringConversion]) = Z3StringCapableSolver.convert(p)
   protected val (new_program, someConverter) = convertProgram(program)
 
@@ -76,16 +79,30 @@ extends Solver {
     someConverter match {
       case None => model
       case Some(converter) =>
-        println("Conversion")
         val ids = model.ids.toSeq
         val exprs = ids.map(model.apply)
         import converter.Backward._
         val original_ids = ids.map(convertId)
         val original_exprs = exprs.map{ case e => convertExpr(e)(Map()) }
-        new Model(original_ids.zip(original_exprs).toMap)
+
+        model match {
+          case hm: PartialModel =>
+            val new_domain = new Domains(
+                hm.domains.lambdas.map(kv =>
+                  (convertExpr(kv._1)(Map()).asInstanceOf[Lambda],
+                   kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap,
+                hm.domains.tpes.map(kv =>
+                  (convertType(kv._1),
+                   kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap
+                )
+        
+            new PartialModel(original_ids.zip(original_exprs).toMap, new_domain)
+          case _ =>
+            new Model(original_ids.zip(original_exprs).toMap)
+        }
     }
   }
-  
+
   // Members declared in leon.utils.Interruptible
   def interrupt(): Unit = underlying.interrupt()
   def recoverInterrupt(): Unit = underlying.recoverInterrupt()
@@ -98,12 +115,14 @@ extends Solver {
       underlying.assertCnstr(newExpression)
     }.getOrElse(underlying.assertCnstr(expression))
   }
+
   def getUnsatCore: Set[Expr] = {
     someConverter.map{converter => 
       import converter.Backward._
       underlying.getUnsatCore map (e => convertExpr(e)(Map()))
     }.getOrElse(underlying.getUnsatCore)
   }
+
   def check: Option[Boolean] = underlying.check
   def free(): Unit = underlying.free()
   def pop(): Unit = underlying.pop()
@@ -125,35 +144,6 @@ trait Z3StringEvaluatingSolver[TUnderlying <: EvaluatingSolver] extends Evaluati
   val useCodeGen: Boolean = underlying.useCodeGen
 }
 
-trait Z3StringQuantificationSolver[TUnderlying <: QuantificationSolver] extends QuantificationSolver { self:  Z3StringCapableSolver[TUnderlying] =>
-  // Members declared in leon.solvers.QuantificationSolver
-  override def getModel = {
-    val model = underlying.getModel
-    someConverter map { converter =>
-      val ids = model.ids.toSeq
-      val exprs = ids.map(model.apply)
-      import converter.Backward._
-      val original_ids = ids.map(convertId)
-      val original_exprs = exprs.map{ case e => convertExpr(e)(Map()) }
-
-      model match {
-        case hm: HenkinModel =>
-          val new_domain = new HenkinDomains(
-              hm.doms.lambdas.map(kv =>
-                (convertExpr(kv._1)(Map()).asInstanceOf[Lambda],
-                 kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap,
-              hm.doms.tpes.map(kv =>
-                (convertType(kv._1),
-                 kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap
-              )
-      
-          new HenkinModel(original_ids.zip(original_exprs).toMap, new_domain)
-        case _ => model
-      }
-    } getOrElse model
-  }
-}
-
 class ConvertibleCodeGenEvaluator(context: LeonContext, originalProgram: Program, val converter: Z3StringConversion)
     extends CodeGenEvaluator(context, originalProgram) {
 
@@ -174,7 +164,6 @@ class ConvertibleDefaultEvaluator(context: LeonContext, originalProgram: Program
   }
 }
 
-
 class FairZ3SolverWithBackwardEvaluator(context: LeonContext, program: Program,
     originalProgram: Program, someConverter: Option[Z3StringConversion]) extends FairZ3Solver(context, program) {
   override lazy val evaluator: DeterministicEvaluator = { // We evaluate expressions using the original evaluator
@@ -195,42 +184,42 @@ class FairZ3SolverWithBackwardEvaluator(context: LeonContext, program: Program,
   }
 }
 
-
 class Z3StringFairZ3Solver(context: LeonContext, program: Program)
   extends Z3StringCapableSolver(context, program,
       (prgm: Program, someConverter: Option[Z3StringConversion]) =>
         new FairZ3SolverWithBackwardEvaluator(context, prgm, program, someConverter)) 
-  with Z3StringEvaluatingSolver[FairZ3Solver]
-  with Z3StringQuantificationSolver[FairZ3Solver] {
-     // Members declared in leon.solvers.z3.AbstractZ3Solver
-    protected[leon] val z3cfg: _root_.z3.scala.Z3Config = underlying.z3cfg
-    override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
-      someConverter match {
-        case None => underlying.checkAssumptions(assumptions)
-        case Some(converter) =>
-          underlying.checkAssumptions(assumptions map (e => converter.Forward.convertExpr(e)(Map())))
-      }
+     with Z3StringEvaluatingSolver[FairZ3Solver] {
+
+  // Members declared in leon.solvers.z3.AbstractZ3Solver
+  protected[leon] val z3cfg: _root_.z3.scala.Z3Config = underlying.z3cfg
+  override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
+    someConverter match {
+      case None => underlying.checkAssumptions(assumptions)
+      case Some(converter) =>
+        underlying.checkAssumptions(assumptions map (e => converter.Forward.convertExpr(e)(Map())))
     }
+  }
 }
 
 class Z3StringUnrollingSolver(context: LeonContext, program: Program, underlyingSolverConstructor: Program => Solver)
   extends Z3StringCapableSolver(context, program, (program: Program, converter: Option[Z3StringConversion]) =>
     new UnrollingSolver(context, program, underlyingSolverConstructor(program)))
-  with Z3StringNaiveAssumptionSolver[UnrollingSolver]
-  with Z3StringEvaluatingSolver[UnrollingSolver]
-  with Z3StringQuantificationSolver[UnrollingSolver] {
-    override def getUnsatCore = super[Z3StringNaiveAssumptionSolver].getUnsatCore
+     with Z3StringNaiveAssumptionSolver[UnrollingSolver]
+     with Z3StringEvaluatingSolver[UnrollingSolver] {
+
+  override def getUnsatCore = super[Z3StringNaiveAssumptionSolver].getUnsatCore
 }
 
 class Z3StringSMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
   extends Z3StringCapableSolver(context, program, (program: Program, converter: Option[Z3StringConversion]) =>
     new smtlib.SMTLIBZ3QuantifiedSolver(context, program)) {
-     override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
-      someConverter match {
-        case None => underlying.checkAssumptions(assumptions)
-        case Some(converter) =>
-          underlying.checkAssumptions(assumptions map (e => converter.Forward.convertExpr(e)(Map())))
-      }
+
+  override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
+    someConverter match {
+      case None => underlying.checkAssumptions(assumptions)
+      case Some(converter) =>
+        underlying.checkAssumptions(assumptions map (e => converter.Forward.convertExpr(e)(Map())))
     }
+  }
 }
 
diff --git a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
index be5f61fe997c7223fee7ad548c4a700b74597062..6d41b5fd8f45def478849c6c2d0623ed85985ffb 100644
--- a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
+++ b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
@@ -191,7 +191,6 @@ trait Z3StringConverters  { self: Z3StringConversion =>
                   convertExpr(kv._2))),
                   convertExpr(default), convertType(tpe).asInstanceOf[FunctionType])
         case Lambda(args, body) =>
-          println("Converting Lambda :" + e)
           val new_bindings = scala.collection.mutable.ListBuffer[(Identifier, Identifier)]()
           val new_args = for(arg <- args) yield {
             val in = arg.getType
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index bb28f259db42657e3365922fdcdad64442ecc1ba..2875bf3ed074756c5089896c327b487cc029fe34 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -21,7 +21,7 @@ import purescala.Common._
 import purescala.Expressions._
 import purescala.Definitions._
 import purescala.SelfPrettyPrinter
-import leon.solvers.{ HenkinModel, Model, SolverFactory }
+import leon.solvers.{ PartialModel, Model, SolverFactory }
 
 case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {
   val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {