diff --git a/src/main/scala/inox/InoxContext.scala b/src/main/scala/inox/InoxContext.scala
index 0f6a3ed7d70f776f3b5f134da342ecaaa0de3ee7..5eda99d46b9310230e39980c25666c7ec70ac9b0 100644
--- a/src/main/scala/inox/InoxContext.scala
+++ b/src/main/scala/inox/InoxContext.scala
@@ -7,38 +7,35 @@ import inox.utils._
 import scala.reflect.ClassTag
 
 /** Everything that is part of a compilation unit, except the actual program tree.
-  * LeonContexts are immutable, and so should all their fields (with the possible
+  * Contexts are immutable, and so should all their fields (with the possible
   * exception of the reporter).
   */
-case class Context(
+case class InoxContext(
   reporter: Reporter,
   interruptManager: InterruptManager,
-  options: Seq[LeonOption[Any]] = Seq(),
-  timers: TimerStorage = new TimerStorage,
-  bank: evaluators.EvaluationBank) {
+  options: Seq[InoxOption[Any]] = Seq(),
+  timers: TimerStorage = new TimerStorage) {
 
-  def findOption[A: ClassTag](optDef: LeonOptionDef[A]): Option[A] = options.collectFirst {
-    case LeonOption(`optDef`, value:A) => value
+  def findOption[A: ClassTag](optDef: InoxOptionDef[A]): Option[A] = options.collectFirst {
+    case InoxOption(`optDef`, value:A) => value
   }
 
-  def findOptionOrDefault[A: ClassTag](optDef: LeonOptionDef[A]): A =
+  def findOptionOrDefault[A: ClassTag](optDef: InoxOptionDef[A]): A =
     findOption(optDef).getOrElse(optDef.default)
-
-  def toSctx = solvers.SolverContext(this, new evaluators.EvaluationBank)
 }
 
-object Context {
+object InoxContext {
   def empty = {
     val reporter = new DefaultReporter(Set())
-    LeonContext(reporter, new InterruptManager(reporter))
+    InoxContext(reporter, new InterruptManager(reporter))
   }
 
   def printNames = {
     val reporter = new DefaultReporter(Set())
-    LeonContext(
+    InoxContext(
       reporter,
       new InterruptManager(reporter),
-      options = Seq(LeonOption[Set[DebugSection]](GlobalOptions.optDebug)(Set(DebugSectionTrees)))
+      options = Seq(InoxOption[Set[DebugSection]](InoxOptions.optDebug)(Set(ast.DebugSectionTrees)))
     )
   }
 }
diff --git a/src/main/scala/inox/InoxOptions.scala b/src/main/scala/inox/InoxOptions.scala
index 32fdc8c72dd67cf518ccbb1b1e014a63925aecc4..c50fb86460866c9b2e5155fb523dc6327f6da8ee 100644
--- a/src/main/scala/inox/InoxOptions.scala
+++ b/src/main/scala/inox/InoxOptions.scala
@@ -12,10 +12,12 @@ abstract class InoxOptionDef[+A] {
   val default: A
   val parser: OptionParser[A]
   val usageRhs: String
+
   def usageDesc = {
     if (usageRhs.isEmpty) s"--$name"
     else s"--$name=$usageRhs"
   }
+
   def helpString = {
     f"$usageDesc%-28s" + description.replaceAll("\n", "\n" + " " * 28)
   }
@@ -40,6 +42,7 @@ abstract class InoxOptionDef[+A] {
     case that: InoxOptionDef[_] => this.name == that.name
     case _ => false
   }
+
   override def hashCode = name.hashCode
 }
 
@@ -152,7 +155,7 @@ object OptionsHelpers {
 
 object InoxOptions {
 
-  val optSelectedSolvers = new LeonOptionDef[Set[String]] {
+  val optSelectedSolvers = new InoxOptionDef[Set[String]] {
     val name = "solvers"
     val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
     val default = Set("fairz3")
@@ -160,7 +163,7 @@ object InoxOptions {
     val usageRhs = "s1,s2,..."
   }
 
-  val optDebug = new LeonOptionDef[Set[DebugSection]] {
+  val optDebug = new InoxOptionDef[Set[DebugSection]] {
     import OptionParsers._
     val name = "debug"
     val description = {
@@ -184,7 +187,7 @@ object InoxOptions {
     }
   }
 
-  val optTimeout = LeonLongOptionDef(
+  val optTimeout = InoxLongOptionDef(
     "timeout",
     "Set a timeout for attempting to prove a verification condition/ repair a function (in sec.)",
     0L,
diff --git a/src/main/scala/inox/Printable.scala b/src/main/scala/inox/Printable.scala
deleted file mode 100644
index d92b53d8094bc426bd4de1408f766a8115864303..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/Printable.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package inox
-
-/** A trait for objects that can be pretty-printed given a [[inox.Context]] */
-trait Printable {
-  def asString(implicit ctx: Context): String
-}
diff --git a/src/main/scala/inox/Program.scala b/src/main/scala/inox/Program.scala
index 0e0649f50fc2667e408ef10f4d37b5c7c8d788d1..c478fc490e33ccab3cb08ce24b13333ef40575c7 100644
--- a/src/main/scala/inox/Program.scala
+++ b/src/main/scala/inox/Program.scala
@@ -4,6 +4,11 @@ package inox
 
 import ast._
 
-class Program(val trees: Trees)(val symbols: trees.Symbols, val ctx: Context) {
+trait Program {
+  val trees: Trees
+  implicit val symbols: trees.Symbols
+  implicit val ctx: InoxContext
 
+  implicit def implicitProgram: this.type = this
+  implicit def printerOpts: trees.PrinterOptions = trees.PrinterOptions.fromSymbols(symbols, ctx)
 }
diff --git a/src/main/scala/inox/Reporter.scala b/src/main/scala/inox/Reporter.scala
index 8e6e2c09c713a29408c79e961737fb4c74f9d107..597f6551741058d1780604e29f59ebcaf19eddcc 100644
--- a/src/main/scala/inox/Reporter.scala
+++ b/src/main/scala/inox/Reporter.scala
@@ -4,8 +4,7 @@ package inox
 
 import utils._
 
-abstract class DebugSection(val name: String, val mask: Int)
-case object DebugSectionSolver extends DebugSection("solver", 1 << 0)
+abstract class DebugSection(val name: String)
 
 abstract class Reporter(val debugSections: Set[DebugSection]) {
 
@@ -70,12 +69,7 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
     }
   }
 
-  // Debugging
-  private val debugMask = debugSections.foldLeft(0){ _ | _.mask }
-
-  def isDebugEnabled(implicit section: DebugSection): Boolean = {
-    (debugMask & section.mask) == section.mask
-  }
+  def isDebugEnabled(implicit section: DebugSection): Boolean = debugSections(section)
 
   def ifDebug(pos: Position, body: (Any => Unit) => Any)(implicit section: DebugSection) = {
     if (isDebugEnabled) {
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 0274053bcbf7c1a6d5738608af4056f8ead3e561..87eaed93fea08fe6c8925114fa47ea83a8a0510a 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -5,7 +5,7 @@ package ast
 
 import scala.collection.mutable.{Map => MutableMap}
 
-trait Definitions { self: Trees =>
+trait Definitions { self0: Trees =>
 
   sealed trait Definition extends Tree {
     val id: Identifier
@@ -63,9 +63,17 @@ trait Definitions { self: Trees =>
         with Constructors
         with Paths {
 
-    val trees: self.type = self
-    val symbols: this.type = this
-    private implicit def s: Symbols = symbols
+    val trees: self0.type = self0
+
+    // @nv: this is a hack to reinject `this` into the set of implicits
+    // in scope when using the pattern:
+    // {{{
+    //    implicit val symbols: Symbols
+    //    import symbols._
+    // }}}
+    // which seems to remove `symbols` from the set of current implicits
+    // for some mysterious reason.
+    implicit def implicitSymbols: this.type = this
 
     private val typedClassCache: MutableMap[(Identifier, Seq[Type]), Option[TypedClassDef]] = MutableMap.empty
     def lookupClass(id: Identifier): Option[ClassDef] = classes.get(id)
@@ -82,6 +90,8 @@ trait Definitions { self: Trees =>
 
     def getFunction(id: Identifier): FunDef = lookupFunction(id).getOrElse(throw FunctionLookupException(id))
     def getFunction(id: Identifier, tps: Seq[Type]): TypedFunDef = lookupFunction(id, tps).getOrElse(throw FunctionLookupException(id))
+
+    def asString: String = asString(PrinterOptions.fromSymbols(this, InoxContext.printNames))
   }
 
   case class TypeParameterDef(tp: TypeParameter) extends Definition {
@@ -226,6 +236,16 @@ trait Definitions { self: Trees =>
     lazy val hasInvariant: Boolean = invariant.isDefined
 
     def toType = ClassType(cd.id, tps)
+
+    def toCase = this match {
+      case tccd: TypedCaseClassDef => tccd
+      case _ => throw NotWellFormedException(cd.id, symbols)
+    }
+
+    def toAbstract = this match {
+      case accd: TypedAbstractClassDef => accd
+      case _ => throw NotWellFormedException(cd.id, symbols)
+    }
   }
 
   case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit symbols: Symbols) extends TypedClassDef {
diff --git a/src/main/scala/inox/ast/GenTreeOps.scala b/src/main/scala/inox/ast/GenTreeOps.scala
index 3217b76b4f67066c213a10cfc061801f026cb82d..c87ea98dc6ee25ccfb2f2fad0871396b5b66f7fb 100644
--- a/src/main/scala/inox/ast/GenTreeOps.scala
+++ b/src/main/scala/inox/ast/GenTreeOps.scala
@@ -31,7 +31,7 @@ trait GenTreeOps {
   /** An extractor for [[SubTree]]*/
   val Deconstructor: TreeExtractor {
     val trees: GenTreeOps.this.trees.type
-    type SubTree <: GenTreeOps.this.SubTree
+    type SubTree = GenTreeOps.this.SubTree
   }
 
   /* ========
diff --git a/src/main/scala/inox/ast/Paths.scala b/src/main/scala/inox/ast/Paths.scala
index 0531ff0551a471173f9cdd0757bdfeb8d2a39ad4..e39e79757dca34b4529abbfbad6dafa2d8dc26d0 100644
--- a/src/main/scala/inox/ast/Paths.scala
+++ b/src/main/scala/inox/ast/Paths.scala
@@ -30,7 +30,7 @@ trait Paths { self: TypeOps with Constructors =>
     * could introduce non-sensical equations.
     */
   class Path private(private[ast] val elements: Seq[Path.Element])
-    extends inox.Printable {
+    extends Printable {
 
     import Path.Element
 
@@ -224,8 +224,7 @@ trait Paths { self: TypeOps with Constructors =>
 
     override def hashCode: Int = elements.hashCode
 
-    override def toString = asString(Context.printNames)
-    def asString(implicit ctx: Context): String = fullClause.asString
-    def asString(pgm: Program)(implicit ctx: Context): String = fullClause.asString(pgm)
+    override def toString = asString(PrinterOptions.fromContext(InoxContext.printNames))
+    def asString(implicit opts: PrinterOptions): String = fullClause.asString
   }
 }
diff --git a/src/main/scala/inox/ast/PrinterOptions.scala b/src/main/scala/inox/ast/PrinterOptions.scala
deleted file mode 100644
index b44b5a90561f57b8882a8ad0564cc6b7123cf2f0..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/ast/PrinterOptions.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import utils._
-
-case class PrinterOptions (
-  baseIndent: Int = 0,
-  printPositions: Boolean = false,
-  printUniqueIds: Boolean = false,
-  printTypes: Boolean = false
-)
-
-object PrinterOptions {
-  def fromContext(ctx: LeonContext): PrinterOptions = {
-    val debugTrees     = ctx.findOptionOrDefault(GlobalOptions.optDebug) contains DebugSectionTrees
-    val debugTypes     = ctx.findOptionOrDefault(GlobalOptions.optDebug) contains DebugSectionTypes
-    val debugPositions = ctx.findOptionOrDefault(GlobalOptions.optDebug) contains DebugSectionPositions
-
-    PrinterOptions(
-      baseIndent     = 0,
-      printPositions = debugPositions,
-      printUniqueIds = debugTrees,
-      printTypes     = debugTypes
-    )
-  }
-}
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 6b3e243a3c10e73f494acea246f0928f2ee60c33..39bb9eba37b37a37a3fd9560f26cf40eaf8359bf 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -5,6 +5,7 @@ package ast
 
 import utils._
 import org.apache.commons.lang3.StringEscapeUtils
+import scala.language.implicitConversions
 
 trait Printers { self: Trees =>
 
@@ -17,10 +18,29 @@ trait Printers { self: Trees =>
     def parent = parents.headOption
   }
 
+  case class PrinterOptions(
+    baseIndent: Int = 0,
+    printPositions: Boolean = false,
+    printUniqueIds: Boolean = false,
+    printTypes: Boolean = false,
+    symbols: Option[Symbols] = None) {
+      require(!printTypes || symbols.isDefined,
+        "Can't print types without an available symbol table")
+  }
+
+  object PrinterOptions {
+    def fromContext(ctx: InoxContext): PrinterOptions = ???
+    def fromSymbols(s: Symbols, ctx: InoxContext): PrinterOptions = ???
+  }
+
+  trait Printable {
+    def asString(implicit opts: PrinterOptions): String
+  }
+
   /** This pretty-printer uses Unicode for some operators, to make sure we
     * distinguish PureScala from "real" Scala (and also because it's cute). */
   class PrettyPrinter(opts: PrinterOptions,
-                      opgm: Option[Program],
+                      osym: Option[Symbols],
                       val sb: StringBuffer = new StringBuffer) {
 
     override def toString = sb.toString
@@ -96,7 +116,7 @@ trait Printers { self: Trees =>
               |}"""
 
         case Forall(args, e) =>
-          p"\u2200${typed(args)}. $e"
+          p"\u2200${nary(args)}. $e"
 
         case e @ CaseClass(cct, args) =>
           p"$cct($args)"
@@ -280,8 +300,10 @@ trait Printers { self: Trees =>
           p"${c.id}${nary(c.tps, ", ", "[", "]")}"
 
         // Definitions
-        case Program(units) =>
-          p"""${nary(units filter { /*opts.printUniqueIds ||*/ _.isMainUnit }, "\n\n")}"""
+        case Symbols(classes, functions) =>
+          p"""${nary(classes.map(_._2).toSeq, "\n\n")}"""
+          p"\n\n"
+          p"""${nary(functions.map(_._2).toSeq, "\n\n")}"""
 
         case acd: AbstractClassDef =>
           p"abstract class ${acd.id}${nary(acd.tparams, ", ", "[", "]")}"
@@ -316,7 +338,7 @@ trait Printers { self: Trees =>
       if (opts.printTypes) {
         tree match {
           case t: Expr=>
-            p" : ${t.getType} ⟩"
+            p" : ${t.getType(opts.symbols.get)} ⟩"
 
           case _ =>
         }
@@ -395,7 +417,7 @@ trait Printers { self: Trees =>
     }
   }
 
-  implicit class Printable(val f: PrinterContext => Any) {
+  implicit class PrintWrapper(val f: PrinterContext => Any) {
     def print(ctx: PrinterContext) = f(ctx)
   }
 
@@ -456,7 +478,7 @@ trait Printers { self: Trees =>
               val nctx2 = nctx.copy(parents = parents, current = t)
               printer.pp(t)(nctx2)
 
-            case p: Printable =>
+            case p: PrintWrapper =>
               p.print(nctx)
 
             case e =>
@@ -467,7 +489,7 @@ trait Printers { self: Trees =>
     }
   }
 
-  def nary(ls: Seq[Any], sep: String = ", ", init: String = "", closing: String = ""): Printable = {
+  def nary(ls: Seq[Any], sep: String = ", ", init: String = "", closing: String = ""): PrintWrapper = {
     val (i, c) = if(ls.isEmpty) ("", "") else (init, closing)
     val strs = i +: List.fill(ls.size-1)(sep) :+ c
 
@@ -475,12 +497,12 @@ trait Printers { self: Trees =>
       new StringContext(strs: _*).p(ls: _*)
   }
 
-  def typed(t: Tree with Typed): Printable = {
+  def typed(t: Tree with Typed)(implicit s: Symbols): PrintWrapper = {
     implicit pctx: PrinterContext =>
       p"$t : ${t.getType}"
   }
 
-  def typed(ts: Seq[Tree with Typed]): Printable = {
+  def typed(ts: Seq[Tree with Typed])(implicit s: Symbols): PrintWrapper = {
     nary(ts.map(typed))
   }
 
@@ -494,7 +516,7 @@ trait Printers { self: Trees =>
     def isSimpleExpr: Boolean = false
   }
 
-  class EquivalencePrettyPrinter(opts: PrinterOptions, opgm: Option[Program]) extends PrettyPrinter(opts, opgm) {
+  class EquivalencePrettyPrinter(opts: PrinterOptions, osym: Option[Symbols]) extends PrettyPrinter(opts, osym) {
     override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
       tree match {
         case id: Identifier =>
@@ -507,31 +529,31 @@ trait Printers { self: Trees =>
   }
 
   abstract class PrettyPrinterFactory {
-    def create(opts: PrinterOptions, opgm: Option[Program]): PrettyPrinter
+    def create(opts: PrinterOptions, osym: Option[Symbols]): PrettyPrinter
 
-    def apply(tree: Tree, opts: PrinterOptions = PrinterOptions(), opgm: Option[Program] = None): String = {
-      val printer = create(opts, opgm)
+    def apply(tree: Tree, opts: PrinterOptions = PrinterOptions(), osym: Option[Symbols] = None): String = {
+      val printer = create(opts, osym)
       val ctx = PrinterContext(tree, Nil, opts.baseIndent, printer)
       printer.pp(tree)(ctx)
       printer.toString
     }
 
-    def apply(tree: Tree, ctx: Context): String = {
+    def apply(tree: Tree, ctx: InoxContext): String = {
       val opts = PrinterOptions.fromContext(ctx)
       apply(tree, opts, None)
     }
 
-    def apply(tree: Tree, ctx: Context, pgm: Program): String = {
+    def apply(tree: Tree, ctx: InoxContext, sym: Symbols): String = {
       val opts = PrinterOptions.fromContext(ctx)
-      apply(tree, opts, Some(pgm))
+      apply(tree, opts, Some(sym))
     }
   }
 
   object PrettyPrinter extends PrettyPrinterFactory {
-    def create(opts: PrinterOptions, opgm: Option[Program]) = new PrettyPrinter(opts, opgm)
+    def create(opts: PrinterOptions, osym: Option[Symbols]) = new PrettyPrinter(opts, osym)
   }
 
   object EquivalencePrettyPrinter extends PrettyPrinterFactory {
-    def create(opts: PrinterOptions, opgm: Option[Program]) = new EquivalencePrettyPrinter(opts, opgm)
+    def create(opts: PrinterOptions, osym: Option[Symbols]) = new EquivalencePrettyPrinter(opts, osym)
   }
 }
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 0595a6adfa5a1b6f04f15dbfcd3c714a37117f8c..223d2627e4cd3fa7b7a88a5dae22b1bac6847a5b 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -24,10 +24,10 @@ import utils._
   * operations on Leon expressions.
   *
   */
-trait SymbolOps extends TreeOps {
+trait SymbolOps extends TreeOps { self: TypeOps =>
   import trees._
   import trees.exprOps._
-  implicit val symbols: Symbols
+  val symbols: Symbols
   import symbols._
 
   /** Computes the negation of a boolean formula, with some simplifications. */
@@ -288,8 +288,9 @@ trait SymbolOps extends TreeOps {
           }
 
         case CaseClassPattern(ob, cct, subps) =>
-          assert(cct.tcd.fields.size == subps.size)
-          val pairs = cct.tcd.fields.map(_.id).toList zip subps.toList
+          val tccd = cct.tcd.toCase
+          assert(tccd.fields.size == subps.size)
+          val pairs = tccd.fields.map(_.id).toList zip subps.toList
           val subTests = pairs.map(p => rec(caseClassSelector(cct, in, p._1), p._2))
           Path(IsInstanceOf(in, cct)) merge bind(ob, in) merge subTests
 
@@ -322,7 +323,7 @@ trait SymbolOps extends TreeOps {
 
     pattern match {
       case CaseClassPattern(b, ct, subps) =>
-        val tcd = ct.tcd
+        val tcd = ct.tcd.toCase
         assert(tcd.fields.size == subps.size)
         val pairs = tcd.fields.map(_.id).toList zip subps.toList
         val subMaps = pairs.map(p => mapForPattern(caseClassSelector(ct, asInstOf(in, ct), p._1), p._2))
@@ -428,26 +429,30 @@ trait SymbolOps extends TreeOps {
   }
 
   private def hasInstance(tcd: TypedClassDef): Boolean = {
-    val ancestors = tcd.ancestors.toSet
+    val recursive = Set(tcd, tcd.root)
 
     def isRecursive(tpe: Type, seen: Set[TypedClassDef]): Boolean = tpe match {
       case ct: ClassType =>
         val ctcd = ct.tcd
         if (seen(ctcd)) {
           false
-        } else if (ancestors(ctcd)) {
+        } else if (recursive(ctcd)) {
           true
-        } else {
-          ctcd.fieldsTypes.exists(isRecursive(_, seen + ctcd))
+        } else ctcd match {
+          case tcc: TypedCaseClassDef =>
+            tcc.fieldsTypes.exists(isRecursive(_, seen + ctcd))
+          case _ => false
         }
       case _ => false
     }
 
-    tcd match {
-      case tacd: TypedAbstractClassDef =>
-        tacd.ccDescendants.filterNot(tccd => isRecursive(tccd.toType, Set.empty)).nonEmpty
-      case tccd: TypedCaseClassDef =>
-        !isRecursive(tccd.toType, Set.empty)
+    val tcds = tcd match {
+      case tacd: TypedAbstractClassDef => tacd.ccDescendants
+      case tccd: TypedCaseClassDef => Seq(tccd)
+    }
+
+    tcds.exists { tcd =>
+      tcd.fieldsTypes.forall(tpe => !isRecursive(tpe, Set.empty))
     }
   }
 
@@ -654,7 +659,7 @@ trait SymbolOps extends TreeOps {
   }
 
   /** Returns the value for an identifier given a model. */
-  def valuateWithModel(model: Model)(vd: ValDef): Expr = {
+  def valuateWithModel(model: Map[ValDef, Expr])(vd: ValDef): Expr = {
     model.getOrElse(vd, simplestValue(vd.getType))
   }
 
@@ -662,7 +667,7 @@ trait SymbolOps extends TreeOps {
     *
     * Complete with simplest values in case of incomplete model.
     */
-  def valuateWithModelIn(expr: Expr, vars: Set[ValDef], model: Model): Expr = {
+  def valuateWithModelIn(expr: Expr, vars: Set[ValDef], model: Map[ValDef, Expr]): Expr = {
     val valuator = valuateWithModel(model) _
     replace(vars.map(vd => vd.toVariable -> valuator(vd)).toMap, expr)
   }
@@ -1003,7 +1008,7 @@ trait SymbolOps extends TreeOps {
         (elems forall (kv => isValueOfType(kv._1, from) < s"${kv._1} not a value of type ${from}" && isValueOfType(unWrapSome(kv._2), to) < s"${unWrapSome(kv._2)} not a value of type ${to}" ))
       case (CaseClass(ct, args), ct2: ClassType) =>
         isSubtypeOf(ct, ct2) < s"$ct not a subtype of $ct2" &&
-        ((args zip ct.tcd.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2) < s"${argstyped._1} not a value of type ${argstyped._2}" ))
+        ((args zip ct.tcd.toCase.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2) < s"${argstyped._1} not a value of type ${argstyped._2}" ))
       case (Lambda(valdefs, body), FunctionType(ins, out)) =>
         variablesOf(e).isEmpty &&
         (valdefs zip ins forall (vdin => isSubtypeOf(vdin._2, vdin._1.getType) < s"${vdin._2} is not a subtype of ${vdin._1.getType}")) &&
diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala
index b02c30a7414be6d45a023a2e9ea8b415de436edd..9295687bb38c4d32e2b6c02bf406da1f7e41d980 100644
--- a/src/main/scala/inox/ast/Trees.scala
+++ b/src/main/scala/inox/ast/Trees.scala
@@ -6,12 +6,14 @@ package ast
 import utils._
 import scala.language.implicitConversions
 
+case object DebugSectionTrees extends DebugSection("trees")
+
 trait Trees extends Expressions with Extractors with Types with Definitions with Printers {
 
-  class Unsupported(t: Tree, msg: String)(implicit ctx: Context)
-    extends Exception(s"${t.asString(ctx)}@${t.getPos} $msg")
+  class Unsupported(t: Tree, msg: String)(implicit ctx: InoxContext)
+    extends Exception(s"${t.asString(PrinterOptions.fromContext(ctx))}@${t.getPos} $msg")
 
-  abstract class Tree extends utils.Positioned with Serializable with inox.Printable {
+  abstract class Tree extends utils.Positioned with Serializable {
     def copiedFrom(o: Tree): this.type = {
       setPos(o)
       this
@@ -19,11 +21,9 @@ trait Trees extends Expressions with Extractors with Types with Definitions with
 
     // @EK: toString is considered harmful for non-internal things. Use asString(ctx) instead.
 
-    def asString(implicit symbols: Symbols, ctx: Context): String = {
-      ScalaPrinter(this, ctx, symbols)
-    }
+    def asString(implicit opts: PrinterOptions): String = PrettyPrinter(this, opts)
 
-    override def toString = asString(Context.printNames)
+    override def toString = asString(PrinterOptions.fromContext(InoxContext.printNames))
   }
 
   object exprOps extends {
diff --git a/src/main/scala/inox/ast/Types.scala b/src/main/scala/inox/ast/Types.scala
index 706c217b53313e61f6b2be89bd0c11ca24d5e11a..e7ae6f8cd7b39213362de7949b289a46cf1544ab 100644
--- a/src/main/scala/inox/ast/Types.scala
+++ b/src/main/scala/inox/ast/Types.scala
@@ -5,7 +5,7 @@ package ast
 
 trait Types { self: Trees =>
 
-  trait Typed extends utils.Printable {
+  trait Typed extends Printable {
     def getType(implicit s: Symbols): Type
     def isTyped(implicit s: Symbols): Boolean = getType != Untyped
   }
@@ -83,7 +83,7 @@ trait Types { self: Trees =>
   case class FunctionType(from: Seq[Type], to: Type) extends Type
 
   case class ClassType(id: Identifier, tps: Seq[Type]) extends Type {
-    def lookupClass(implicit s: Symbols): Option[TypedClassDef] = p.lookupClass(id, tps)
+    def lookupClass(implicit s: Symbols): Option[TypedClassDef] = s.lookupClass(id, tps)
     def tcd(implicit s: Symbols): TypedClassDef = s.getClass(id, tps)
   }
 
diff --git a/src/main/scala/inox/evaluators/EvaluationResults.scala b/src/main/scala/inox/evaluators/EvaluationResults.scala
index f7da29504b6143a15552818841685124204184f8..d3de898fbfd4eb7c096de4442405a50b5fd7885d 100644
--- a/src/main/scala/inox/evaluators/EvaluationResults.scala
+++ b/src/main/scala/inox/evaluators/EvaluationResults.scala
@@ -1,18 +1,18 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package evaluators
 
 object EvaluationResults {
   /** Possible results of expression evaluation. */
-  sealed abstract class Result[+A](val result : Option[A])
+  sealed abstract class Result[+A](val result: Option[A])
 
   /** Represents an evaluation that successfully derived the result `value`. */
-  case class Successful[A](value : A) extends Result(Some(value))
+  case class Successful[A](value: A) extends Result(Some(value))
 
   /** Represents an evaluation that led to an error (in the program). */
-  case class RuntimeError(message : String) extends Result(None)
+  case class RuntimeError(message: String) extends Result(None)
 
   /** Represents an evaluation that failed (in the evaluator). */
-  case class EvaluatorError(message : String) extends Result(None)
+  case class EvaluatorError(message: String) extends Result(None)
 }
diff --git a/src/main/scala/inox/evaluators/Evaluator.scala b/src/main/scala/inox/evaluators/Evaluator.scala
index ccde2fd20d9677f7c6331fb652121e529d8a29d8..ce913f77f7022efcd64ebbf47d85c41d71450f1a 100644
--- a/src/main/scala/inox/evaluators/Evaluator.scala
+++ b/src/main/scala/inox/evaluators/Evaluator.scala
@@ -1,17 +1,11 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package evaluators
 
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-
-import solvers.Model
-
-import scala.collection.mutable.{Map => MutableMap}
-
-abstract class Evaluator(val context: LeonContext, val program: Program) extends LeonComponent {
+trait Evaluator {
+  val program: Program
+  import program.trees._
 
   /** The type of value that this [[Evaluator]] calculates
     * Typically, it will be [[Expr]] for deterministic evaluators, and
@@ -22,23 +16,18 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
   type EvaluationResult = EvaluationResults.Result[Value]
 
   /** Evaluates an expression, using [[Model.mapping]] as a valuation function for the free variables. */
-  def eval(expr: Expr, model: Model) : EvaluationResult
-
-  /** Evaluates an expression given a simple model (assumes expr is quantifier-free).
-    * Mainly useful for compatibility reasons.
-    */
-  def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = eval(expr, new Model(mapping))
+  def eval(expr: Expr, model: Map[ValDef, Expr]) : EvaluationResult
 
   /** Evaluates a ground expression. */
-  final def eval(expr: Expr) : EvaluationResult = eval(expr, Model.empty)
+  final def eval(expr: Expr) : EvaluationResult = eval(expr, Map.empty)
 
   /** Compiles an expression into a function, where the arguments are the free variables in the expression.
     * `argorder` specifies in which order the arguments should be passed.
     * The default implementation uses the evaluation function each time, but evaluators are free
     * to (and encouraged to) apply any specialization.
     */
-  def compile(expr: Expr, args: Seq[Identifier]) : Option[Model => EvaluationResult] = Some(
-    (model: Model) => if(args.exists(arg => !model.isDefinedAt(arg))) {
+  def compile(expr: Expr, args: Seq[ValDef]) : Option[Map[ValDef, Expr] => EvaluationResult] = Some(
+    (model: Map[ValDef, Expr]) => if(args.exists(arg => !model.isDefinedAt(arg))) {
       EvaluationResults.EvaluatorError("Wrong number of arguments for evaluation.")
     } else {
       eval (expr, model)
@@ -47,136 +36,6 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
 }
 
 trait DeterministicEvaluator extends Evaluator {
-  type Value = Expr
-
-  val bank: EvaluationBank
-  
-  /**Evaluates the environment first, resolving non-cyclic dependencies, and then evaluate the expression */
-  override def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = {
-    if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
-      super.eval(expr, mapping.toMap)
-    } else {
-      _evalEnv(mapping) match {
-        case Left(m) => super.eval(expr, m)
-        case Right(errorMessage) =>
-          val m = mapping.filter { case (k, v) => purescala.ExprOps.isValue(v) }
-          super.eval(expr, m) match {
-            case res@EvaluationResults.Successful(result) => res
-            case _ => EvaluationResults.EvaluatorError(errorMessage)
-          }
-      }
-    }
-  }
-
-  /** Returns an evaluated environment. If it fails, removes all non-values from the environment. */
-  def evalEnv(mapping: Iterable[(Identifier, Expr)]): Map[Identifier, Value] = {
-    if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
-      mapping.toMap
-    } else {
-      _evalEnv(mapping) match {
-        case Left(m) => m
-        case Right(msg) =>
-          mapping.filter(x => purescala.ExprOps.isValue(x._2)).toMap
-      }
-    }
-  }
-  
-  /** From a not yet well evaluated context with dependencies between variables, returns a head where all exprs are values (as a Left())
-   *  If this does not succeed, it provides an error message as Right()*/
-  private def _evalEnv(mapping: Iterable[(Identifier, Expr)]): Either[Map[Identifier, Value], String] = {
-    val (evaled, nonevaled) = mapping.partition{ case (id, expr) => purescala.ExprOps.isValue(expr)}
-    var f= nonevaled.toSet
-    var mBuilder = scala.collection.mutable.ListBuffer[(Identifier, Value)]() ++= evaled
-    var changed = true
-    while(f.nonEmpty && changed) {
-      changed = false
-      for((i, v) <- f) {
-        eval(v, mBuilder.toMap).result match {
-          case None =>
-          case Some(e) =>
-            changed = true
-            mBuilder += ((i -> e))
-            f -= ((i, v))
-        }
-      }
-    }
-    if(!changed) {
-      val str = "In the context " + mapping + ",\n" +
-      (for((i, v) <- f) yield {
-        s"eval($v) returned the error: " + eval(v, mBuilder.toMap)
-      }).mkString("\n")
-      Right(str)
-    } else Left(mBuilder.toMap)
-  }
+  type Value = program.trees.Expr
 }
 
-trait NDEvaluator extends Evaluator {
-  type Value = Stream[Expr]
-}
-
-/* Status of invariant checking
- *
- * For a given invariant, its checking status can be either
- * - Complete(success) : checking has been performed previously and
- *                       resulted in a value of `success`.
- * - Pending           : invariant is currently being checked somewhere
- *                       in the program. If it fails, the failure is
- *                       assumed to be bubbled up to all relevant failure
- *                       points.
- * - NoCheck           : invariant has never been seen before. Discovering
- *                       NoCheck for an invariant will automatically update
- *                       the status to `Pending` as this creates a checking
- *                       obligation.
- */
-sealed abstract class CheckStatus {
-  /* The invariant was invalid and this particular case class can't exist */
-  def isFailure: Boolean = this match {
-    case Complete(status) => !status
-    case _ => false
-  }
-
-  /* The invariant has never been checked before and the checking obligation
-   * therefore falls onto the first caller of this method. */
-  def isRequired: Boolean = this == NoCheck
-}
-
-case class Complete(success: Boolean) extends CheckStatus
-case object Pending extends CheckStatus
-case object NoCheck extends CheckStatus
-
-class EvaluationBank private(
-  /* Shared set that tracks checked case-class invariants
-   *
-   * Checking case-class invariants can require invoking a solver
-   * on a ground formula that contains a reference to `this` (the
-   * current case class). If we then wish to check the model
-   * returned by the solver, the expression given to the evaluator
-   * will again contain the constructor for the current case-class.
-   * This will create an invariant-checking loop.
-   *
-   * To avoid this problem, we introduce a set of invariants
-   * that have already been checked that is shared between related
-   * solvers and evaluators. This set is used by the evaluators to
-   * determine whether the invariant of a given case
-   * class should be checked.
-   */
-  checkCache: MutableMap[CaseClass, CheckStatus]) {
-
-  def this() = this(MutableMap.empty)
-
-  /* Status of the invariant checking for `cc` */
-  def invariantCheck(cc: CaseClass): CheckStatus = synchronized {
-    if (!cc.ct.classDef.hasInvariant) Complete(true)
-    else checkCache.getOrElse(cc, {
-      checkCache(cc) = Pending
-      NoCheck
-    })
-  }
-
-  /* Update the cache with the invariant check result for `cc` */
-  def invariantResult(cc: CaseClass, success: Boolean): Unit = synchronized {
-    checkCache(cc) = Complete(success)
-  }
-
-  override def clone: EvaluationBank = new EvaluationBank(checkCache.clone)
-}
diff --git a/src/main/scala/inox/evaluators/SolvingEvalInterface.scala b/src/main/scala/inox/evaluators/SolvingEvalInterface.scala
new file mode 100644
index 0000000000000000000000000000000000000000..55e8b84dbeaf3a922edc8aa2c3d3285526a8513a
--- /dev/null
+++ b/src/main/scala/inox/evaluators/SolvingEvalInterface.scala
@@ -0,0 +1,37 @@
+
+package inox
+package evaluators
+
+import scala.collection.mutable.{Map => MutableMap}
+
+trait SolvingEvalInterface {
+  val program: Program
+  import program._
+  import program.trees._
+  import program.symbols._
+
+  val evaluator: DeterministicEvaluator with SolvingEvaluator { val program: SolvingEvalInterface.this.program.type }
+  val bodies: Map[Identifier, (Seq[ValDef], Expr)]
+
+  private val inputCache: MutableMap[(Identifier, Seq[Expr]), Expr] = MutableMap.empty
+  private val forallCache: MutableMap[Forall, Expr] = MutableMap.empty
+
+  def onInputInvocation(id: Identifier, args: Seq[Expr]): Expr = inputCache.getOrElseUpdate((id, args), {
+    val (vds, body) = bodies.getOrElse(id, throw new RuntimeException("Body for " + id + " not found"))
+    val tpSubst = canBeSupertypeOf(tupleTypeWrap(vds.map(_.tpe)), tupleTypeWrap(args.map(_.getType))).getOrElse {
+      throw new RuntimeException("Cannot construct typing substitution from " + vds.map(_.asString).mkString(",") + " to " + args.map(_.asString))
+    }
+
+    val model = (vds.map(vd => vd.copy(tpe = instantiateType(vd.tpe, tpSubst))) zip args).toMap
+    val instBody = instantiateType(body, tpSubst)
+    evaluator.eval(instBody, model).result.getOrElse {
+      throw new RuntimeException("Couldn't evaluate " + instBody.asString + " with model " +
+        model.map(p => p._1.asString -> p._2.asString).mkString("{", ", ", "}"))
+    }
+  })
+
+  def onForallInvocation(forall: Forall): Expr = forallCache.getOrElseUpdate(forall, {
+    
+
+  })
+}
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e05333f49c550166196f1d061d8834a1b2c56792
--- /dev/null
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -0,0 +1,103 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package evaluators
+
+import scala.collection.mutable.{Map => MutableMap}
+
+trait SolvingEvaluator extends Evaluator {
+
+  object bankOption extends InoxOptionDef[EvaluationBank] {
+    val parser = { (_: String) => throw FatalError("Unparsable option \"bankOption\"") }
+    val name = "bank-option"
+    val description = "Evaluation bank shared between solver and evaluator"
+    val usageRhs = ""
+    def default = new EvaluationBank {
+      val program: SolvingEvaluator.this.program.type = SolvingEvaluator.this.program
+    }
+  }
+
+  val solver: SolverFactory[Solver]
+}
+
+/* Status of invariant checking
+ *
+ * For a given invariant, its checking status can be either
+ * - Complete(success) : checking has been performed previously and
+ *                       resulted in a value of `success`.
+ * - Pending           : invariant is currently being checked somewhere
+ *                       in the program. If it fails, the failure is
+ *                       assumed to be bubbled up to all relevant failure
+ *                       points.
+ * - NoCheck           : invariant has never been seen before. Discovering
+ *                       NoCheck for an invariant will automatically update
+ *                       the status to `Pending` as this creates a checking
+ *                       obligation.
+ */
+sealed abstract class CheckStatus {
+  /* The invariant was invalid and this particular case class can't exist */
+  def isFailure: Boolean = this match {
+    case Complete(status) => !status
+    case _ => false
+  }
+
+  /* The invariant has never been checked before and the checking obligation
+   * therefore falls onto the first caller of this method. */
+  def isRequired: Boolean = this == NoCheck
+}
+
+case class Complete(success: Boolean) extends CheckStatus
+case object Pending extends CheckStatus
+case object NoCheck extends CheckStatus
+
+object EvaluationBank {
+  def empty(p: Program): EvaluationBank { val program: p.type } = new EvaluationBank {
+    val program: p.type = p
+    val checkCache = MutableMap.empty
+  }
+
+  private def apply(p: Program)(cache: MutableMap[p.trees.CaseClass, CheckStatus]): EvaluationBank { val program: p.type } = new EvaluationBank {
+    val program: p.type = p
+    val checkCache = cache
+  }
+}
+
+trait EvaluationBank {
+  implicit val program: Program
+  import program._
+  import program.trees._
+
+  /* Shared set that tracks checked case-class invariants
+   *
+   * Checking case-class invariants can require invoking a solver
+   * on a ground formula that contains a reference to `this` (the
+   * current case class). If we then wish to check the model
+   * returned by the solver, the expression given to the evaluator
+   * will again contain the constructor for the current case-class.
+   * This will create an invariant-checking loop.
+   *
+   * To avoid this problem, we introduce a set of invariants
+   * that have already been checked that is shared between related
+   * solvers and evaluators. This set is used by the evaluators to
+   * determine whether the invariant of a given case
+   * class should be checked.
+   */
+  val checkCache: MutableMap[CaseClass, CheckStatus]
+
+  /* Status of the invariant checking for `cc` */
+  def invariantCheck(cc: CaseClass): CheckStatus = synchronized {
+    if (!cc.ct.tcd.hasInvariant) Complete(true)
+    else checkCache.getOrElse(cc, {
+      checkCache(cc) = Pending
+      NoCheck
+    })
+  }
+
+  /* Update the cache with the invariant check result for `cc` */
+  def invariantResult(cc: CaseClass, success: Boolean): Unit = synchronized {
+    checkCache(cc) = Complete(success)
+  }
+
+  override def clone: EvaluationBank { val program: EvaluationBank.this.program.type } =
+    EvaluationBank(program)(checkCache.clone)
+}
diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index 368316aa09df4339c65da9b2550bddc88920498f..ed98affade8896e911f05fbab1508dc25fa86e01 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -1,5 +1,7 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
+import scala.language.implicitConversions
+
 /** Core package of the Leon system 
   *
   * Provides the basic types and definitions for the Leon system.
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index 935274abfaef3b8e3a8bcdffd245b7e9496cab53..549d5ca75a87b6ad49159b69e63c04ba3ea02138 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -1,34 +1,53 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package solvers
 
-import leon.utils.{DebugSectionSolver, Interruptible}
-import purescala.Expressions._
-import purescala.Common.Tree
-import verification.VC
+import utils._
 import evaluators._
 
-case class SolverContext(context: LeonContext, bank: EvaluationBank) {
-  lazy val reporter = context.reporter
-  override def clone = SolverContext(context, bank.clone)
+case class SolverOptions(options: Seq[InoxOption[Any]]) {
+  def set(opts: Seq[LeonOption[Any]]): SolverOptions = {
+    val changed = opts.map(_.optionDef).toSet
+    val remainingOpts = options.filter { case InoxOption(optDef, _) => !changed(optDef) }
+    copy(options = remainingOpts ++ opts)
+  }
 }
 
+case object DebugSectionSolver extends DebugSection("solver")
+
 trait Solver extends Interruptible {
   def name: String
-  val sctx: SolverContext
+  val program: Program
+  val options: SolverOptions
+
+  import program._
+  import program.trees._
 
-  implicit lazy val context = sctx.context
-  lazy val reporter = sctx.reporter
+  sealed trait SolverResponse
+  sealed trait SolverCheckResponse extends SolverResponse
+  sealed trait SolverModelResponse extends SolverResponse
+
+  case object Unknown extends SolverCheckResponse with SolverModelResponse
+  case object UNSAT extends SolverCheckResponse with SolverModelResponse
+  case object SAT extends SolverCheckResponse
+  case class Model(model: Map[ValDef, Expr]) extends SolverModelResponse
+
+  object SolverUnsupportedError {
+    def msg(t: Tree, reason: Option[String]) = {
+      s"(of ${t.getClass}) is unsupported by solver ${name}" + reason.map(":\n  " + _ ).getOrElse("")
+    }
+  }
+
+  case class SolverUnsupportedError(t: Tree, reason: Option[String] = None)
+    extends Unsupported(t, SolverUnsupportedError.msg(t,reason))
+
+  lazy val reporter = program.ctx.reporter
 
   // This is ugly, but helpful for smtlib solvers
   def dbg(msg: => Any) {}
 
   def assertCnstr(expression: Expr): Unit
-  def assertVC(vc: VC) = {
-    dbg(s"; Solving $vc @ ${vc.getPos}\n")
-    assertCnstr(Not(vc.condition))
-  }
 
   /** Returns Some(true) if it found a satisfying model, Some(false) if no model exists, and None otherwise */
   def check: Option[Boolean]
@@ -47,20 +66,20 @@ trait Solver extends Interruptible {
   def getUnsatCore: Set[Expr]
 
   protected def unsupported(t: Tree): Nothing = {
-    val err = SolverUnsupportedError(t, this, None)
-    context.reporter.warning(err.getMessage)
+    val err = SolverUnsupportedError(t, None)
+    reporter.warning(err.getMessage)
     throw err
   }
 
   protected def unsupported(t: Tree, str: String): Nothing = {
-    val err = SolverUnsupportedError(t, this, Some(str))
-    //leonContext.reporter.warning(str)
+    val err = SolverUnsupportedError(t, Some(str))
+    reporter.warning(err.getMessage)
     throw err
   }
 
   implicit val debugSection = DebugSectionSolver
 
   private[solvers] def debugS(msg: String) = {
-    context.reporter.debug("["+name+"] "+msg)
+    reporter.debug("["+name+"] "+msg)
   }
 }
diff --git a/src/main/scala/inox/utils/ASCIIHelpers.scala b/src/main/scala/inox/utils/ASCIIHelpers.scala
index 0b5a746f540ef1ad49c4e5e88155a4228b33e15c..3737bd97314a62bd6c1d43548abd44003d12b379 100644
--- a/src/main/scala/inox/utils/ASCIIHelpers.scala
+++ b/src/main/scala/inox/utils/ASCIIHelpers.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon.utils
+package inox.utils
 
 object ASCIIHelpers {
   case class Table(title: String, rows: Seq[TableRow] = Nil) {
diff --git a/src/main/scala/inox/utils/ModelEnumerator.scala b/src/main/scala/inox/utils/ModelEnumerator.scala
index 75fd2a0a3de2a8bcb554b810e3538346443aaf19..f1cf05af188cc060cca568ec8cadb23dbec0a069 100644
--- a/src/main/scala/inox/utils/ModelEnumerator.scala
+++ b/src/main/scala/inox/utils/ModelEnumerator.scala
@@ -12,8 +12,11 @@ import purescala.Types._
 import evaluators._
 import solvers._
 
-class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) {
-  private[this] val evaluator = new DefaultEvaluator(ctx, pgm)
+class ModelEnumerator(sf: SolverFactory[Solver]) {
+  val program = sf.program
+  import program.trees._
+
+  protected val evaluator = new DefaultEvaluator(ctx, pgm)
 
   def enumSimple(ids: Seq[Identifier], satisfying: Expr): FreeableIterator[Map[Identifier, Expr]] = {
     enumVarying0(ids, satisfying, None, -1)
diff --git a/src/main/scala/inox/utils/OracleTraverser.scala b/src/main/scala/inox/utils/OracleTraverser.scala
deleted file mode 100644
index 0044dc695e2448c8c5ff229411f56fe7d3550d32..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/utils/OracleTraverser.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package utils
-
-import purescala.Expressions._
-import purescala.Types._
-import purescala.Definitions._
-
-case class OracleTraverser(oracle: Expr, tpe: TypeTree, program: Program) {
-  private def call(name: String) = {
-    program.definedFunctions.find(_.id.name == "Oracle."+name) match {
-      case Some(fd) =>
-        FunctionInvocation(fd.typed(List(tpe)), List(oracle))
-      case None =>
-        sys.error("Unable to find Oracle."+name)
-    }
-  }
-
-  def value: Expr = {
-    call("head")
-  }
-
-  def left: OracleTraverser = {
-    OracleTraverser(call("left"), tpe, program)
-  }
-
-  def right: OracleTraverser = {
-    OracleTraverser(call("right"), tpe, program)
-  }
-}
diff --git a/src/main/scala/inox/utils/PreprocessingPhase.scala b/src/main/scala/inox/utils/PreprocessingPhase.scala
deleted file mode 100644
index 5475e0c4db4b65c9f7dcd37d630e32104c32fcb9..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/utils/PreprocessingPhase.scala
+++ /dev/null
@@ -1,50 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package utils
-
-import leon.purescala._
-import leon.purescala.Definitions.Program
-import leon.solvers.isabelle.AdaptationPhase
-import leon.verification.InjectAsserts
-import leon.xlang.{NoXLangFeaturesChecking, XLangDesugaringPhase, XLangCleanupPhase}
-
-class PreprocessingPhase(genc: Boolean = false) extends LeonPhase[Program, Program] {
-
-  val name = "preprocessing"
-  val description = "Various preprocessings on Leon programs"
-
-  override def run(ctx: LeonContext, p: Program): (LeonContext, Program) = {
-
-    def debugTrees(title: String) =
-      PrintTreePhase(title).when(ctx.reporter.isDebugEnabled(DebugSectionTrees))
-
-    val pipeBegin =
-      debugTrees("Program after extraction")      andThen
-      MethodLifting                               andThen
-      TypingPhase                                 andThen
-      synthesis.ConversionPhase                   andThen
-      InliningPhase
-
-    // Do not desugar xlang when generating C code
-    val pipeX = (
-      XLangDesugaringPhase andThen
-      debugTrees("Program after xlang desugaring")
-    ) when (!genc)
-
-    def pipeEnd = (
-      InjectAsserts  andThen
-      FunctionClosure andThen
-      //XLangCleanupPhase andThen
-      AdaptationPhase
-    ) when (!genc)
-
-    val phases =
-      pipeBegin andThen
-      pipeX andThen
-      pipeEnd andThen
-      debugTrees("Program after pre-processing")
-
-    phases.run(ctx, p)
-  }
-}
diff --git a/src/main/scala/inox/utils/PrintReportPhase.scala b/src/main/scala/inox/utils/PrintReportPhase.scala
deleted file mode 100644
index cf19df7575fd299254315eabcd3fdca4bd5fb568..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/utils/PrintReportPhase.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package utils
-
-/** Pretty-prints a [[Report]] */
-case object PrintReportPhase extends UnitPhase[Report] {
-
-  override val description: String = "Print a Leon report"
-  override val name: String = "PrintReport"
-
-  override def apply(ctx: LeonContext, rep: Report): Unit = {
-    ctx.reporter.info(rep.summaryString)
-  }
-
-}
diff --git a/src/main/scala/inox/utils/PrintTreePhase.scala b/src/main/scala/inox/utils/PrintTreePhase.scala
deleted file mode 100644
index 87003c14d8fd77fb96e24eb5e9653d79f12e5fe5..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/utils/PrintTreePhase.scala
+++ /dev/null
@@ -1,18 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package utils
-
-
-import purescala.Definitions.Program
-
-case class PrintTreePhase(title: String) extends UnitPhase[Program] {
-
-  val name = "Print program"
-  val description = "Display: "+title
-
-  def apply(ctx: LeonContext, p: Program) {
-    ctx.reporter.info(ASCIIHelpers.title(title))
-    ctx.reporter.info(p.asString(p)(ctx))
-  }
-}
diff --git a/src/main/scala/inox/utils/TimeoutFor.scala b/src/main/scala/inox/utils/TimeoutFor.scala
index fa2b9aeca28d6cb83cd6449075a3f2b1dff98124..4a07ba0f69bed143fe1c299cbf3e3ba8d5373142 100644
--- a/src/main/scala/inox/utils/TimeoutFor.scala
+++ b/src/main/scala/inox/utils/TimeoutFor.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package utils
 
 class TimeoutFor(it: Interruptible) {