diff --git a/src/main/scala/inox/InoxContext.scala b/src/main/scala/inox/InoxContext.scala
index 5eda99d46b9310230e39980c25666c7ec70ac9b0..6abc7d3e1824c7d16c6f1fd8b880b088c770de0f 100644
--- a/src/main/scala/inox/InoxContext.scala
+++ b/src/main/scala/inox/InoxContext.scala
@@ -4,8 +4,6 @@ package inox
 
 import inox.utils._
 
-import scala.reflect.ClassTag
-
 /** Everything that is part of a compilation unit, except the actual program tree.
   * Contexts are immutable, and so should all their fields (with the possible
   * exception of the reporter).
@@ -14,15 +12,7 @@ case class InoxContext(
   reporter: Reporter,
   interruptManager: InterruptManager,
   options: Seq[InoxOption[Any]] = Seq(),
-  timers: TimerStorage = new TimerStorage) {
-
-  def findOption[A: ClassTag](optDef: InoxOptionDef[A]): Option[A] = options.collectFirst {
-    case InoxOption(`optDef`, value:A) => value
-  }
-
-  def findOptionOrDefault[A: ClassTag](optDef: InoxOptionDef[A]): A =
-    findOption(optDef).getOrElse(optDef.default)
-}
+  timers: TimerStorage = new TimerStorage) extends InoxOptions
 
 object InoxContext {
   def empty = {
diff --git a/src/main/scala/inox/InoxOptions.scala b/src/main/scala/inox/InoxOptions.scala
index c50fb86460866c9b2e5155fb523dc6327f6da8ee..4ae72dcda50d9551e86411b0b28269729804cac3 100644
--- a/src/main/scala/inox/InoxOptions.scala
+++ b/src/main/scala/inox/InoxOptions.scala
@@ -5,11 +5,12 @@ package inox
 import OptionParsers._
 
 import scala.util.Try
+import scala.reflect.ClassTag
 
 abstract class InoxOptionDef[+A] {
   val name: String
   val description: String
-  val default: A
+  def default: A
   val parser: OptionParser[A]
   val usageRhs: String
 
@@ -153,8 +154,19 @@ object OptionsHelpers {
   }
 }
 
+trait InoxOptions {
+  val options: Seq[InoxOption[Any]]
+
+  def findOption[A: ClassTag](optDef: InoxOptionDef[A]): Option[A] = options.collectFirst {
+    case InoxOption(`optDef`, value: A) => value
+  }
+
+  def findOptionOrDefault[A: ClassTag](optDef: InoxOptionDef[A]): A = findOption(optDef).getOrElse(optDef.default)
+}
+
 object InoxOptions {
 
+  /*
   val optSelectedSolvers = new InoxOptionDef[Set[String]] {
     val name = "solvers"
     val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
@@ -162,25 +174,32 @@ object InoxOptions {
     val parser = setParser(stringParser)
     val usageRhs = "s1,s2,..."
   }
+  */
 
   val optDebug = new InoxOptionDef[Set[DebugSection]] {
     import OptionParsers._
     val name = "debug"
     val description = {
+      /*
       val sects = DebugSections.all.toSeq.map(_.name).sorted
       val (first, second) = sects.splitAt(sects.length/2 + 1)
-      "Enable detailed messages per component.\nAvailable:\n" +
+      */
+      "Enable detailed messages per component." /* +
+      "\nAvailable:\n" +
         "  " + first.mkString(", ") + ",\n" +
-        "  " + second.mkString(", ")
+        "  " + second.mkString(", ")*/
     }
     val default = Set[DebugSection]()
     val usageRhs = "d1,d2,..."
     private val debugParser: OptionParser[Set[DebugSection]] = s => {
+      /*
       if (s == "all") {
         Some(DebugSections.all)
       } else {
         DebugSections.all.find(_.name == s).map(Set(_))
-      }
+      }*/
+     None
+
     }
     val parser: String => Option[Set[DebugSection]] = {
       setParser[Set[DebugSection]](debugParser)(_).map(_.flatten)
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 87eaed93fea08fe6c8925114fa47ea83a8a0510a..d7fab61eec1a2467e7af1393ee93c41059f3e076 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -3,9 +3,10 @@
 package inox
 package ast
 
+import scala.reflect._
 import scala.collection.mutable.{Map => MutableMap}
 
-trait Definitions { self0: Trees =>
+trait Definitions { self: Trees =>
 
   sealed trait Definition extends Tree {
     val id: Identifier
@@ -37,12 +38,32 @@ trait Definitions { self0: Trees =>
 
     def getType(implicit s: Symbols): Type = tpe
 
+    def to[A <: VariableSymbol](implicit ev: VariableConverter[A]): A = ev.convert(this)
+
     override def equals(that: Any): Boolean = that match {
       case vs: VariableSymbol => id == vs.id && tpe == vs.tpe
       case _ => false
     }
 
-    def hashCode: Int = 61 * id.hashCode + tpe.hashCode
+    override def hashCode: Int = 61 * id.hashCode + tpe.hashCode
+  }
+
+  sealed abstract class VariableConverter[B <: VariableSymbol] {
+    def convert(a: VariableSymbol): B
+  }
+
+  implicit def convertToVal = new VariableConverter[ValDef] {
+    def convert(vs: VariableSymbol): ValDef = vs match {
+      case v: ValDef => v
+      case _ => ValDef(vs.id, vs.tpe)
+    }
+  }
+
+  implicit def convertToVar = new VariableConverter[Variable] {
+    def convert(vs: VariableSymbol): Variable = vs match {
+      case v: Variable => v
+      case _ => Variable(vs.id, vs.tpe)
+    }
   }
 
   /** 
@@ -50,8 +71,11 @@ trait Definitions { self0: Trees =>
     */
   case class ValDef(id: Identifier, tpe: Type) extends Definition with VariableSymbol {
     /** Transform this [[ValDef]] into a [[Expressions.Variable Variable]] */
-    def toVariable: Variable = Variable(id, tpe)
+    def toVariable: Variable = to[Variable]
     def freshen: ValDef = ValDef(id.freshen, tpe).copiedFrom(this)
+
+    override def equals(that: Any): Boolean = super[VariableSymbol].equals(that)
+    override def hashCode: Int = super[VariableSymbol].hashCode
   }
 
   /** A wrapper for a program. For now a program is simply a single object. */
@@ -63,7 +87,8 @@ trait Definitions { self0: Trees =>
         with Constructors
         with Paths {
 
-    val trees: self0.type = self0
+    val trees: self.type = self
+    val symbols: this.type = this
 
     // @nv: this is a hack to reinject `this` into the set of implicits
     // in scope when using the pattern:
@@ -248,12 +273,12 @@ trait Definitions { self0: Trees =>
     }
   }
 
-  case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit symbols: Symbols) extends TypedClassDef {
+  case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
     def descendants: Seq[TypedClassDef] = cd.descendants.map(_.typed(tps))
     def ccDescendants: Seq[TypedCaseClassDef] = cd.ccDescendants.map(_.typed(tps))
   }
 
-  case class TypedCaseClassDef(cd: CaseClassDef, tps: Seq[Type])(implicit symbols: Symbols) extends TypedClassDef {
+  case class TypedCaseClassDef(cd: CaseClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
     lazy val fields: Seq[ValDef] = {
       val tmap = (cd.typeArgs zip tps).toMap
       if (tmap.isEmpty) cd.fields
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 81555ad82e26e2180f051cdbe3cdec1db807ce01..9fdc9329dc280649cfd820d6edfe2f2428c71b23 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -4,6 +4,7 @@ package inox
 package ast
 
 import utils._
+import scala.reflect._
 
 /** Provides functions to manipulate [[purescala.Expressions]].
   *
@@ -33,10 +34,12 @@ trait ExprOps extends GenTreeOps {
   val Deconstructor = Operator
 
   /** Replaces bottom-up variables by looking up for them in a map */
-  def replaceFromSymbols(substs: Map[Variable, Expr], expr: Expr): Expr = postMap {
-    case v: Variable => substs.get(v)
-    case _ => None
-  } (expr)
+  def replaceFromSymbols[V <: VariableSymbol](substs: Map[V, Expr], expr: Expr)(implicit ev: VariableConverter[V]): Expr = {
+    postMap {
+      case v: Variable => substs.get(v.to[V])
+      case _ => None
+    } (expr)
+  }
 
   /** Replaces bottom-up variables by looking them up in a map from [[ValDef]] to expressions */
   def replaceFromSymbols(substs: Map[ValDef, Expr], expr: Expr): Expr = postMap {
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 1bfd1b3422a2f8be8c1af58a6d3d4389cf6500c4..d5d21dfbc6230907f0fbbc1d2adfec9cbb5f5c6c 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -47,7 +47,7 @@ trait Expressions { self: Trees =>
 
   /** Stands for an undefined Expr, similar to `???` or `null` */
   case class NoTree(tpe: Type) extends Expr with Terminal {
-    val getType = tpe
+    def getType(implicit s: Symbols): Type = tpe
   }
 
 
@@ -121,7 +121,7 @@ trait Expressions { self: Trees =>
     */
   case class Variable(id: Identifier, tpe: Type) extends Expr with Terminal with VariableSymbol {
     /** Transforms this [[Variable]] into a [[Definitions.ValDef ValDef]] */
-    def toVal = ValDef(id, tpe)
+    def toVal = to[ValDef]
   }
 
 
@@ -487,7 +487,7 @@ trait Expressions { self: Trees =>
     * you should use [[purescala.Constructors#or purescala's constructor or]] or
     * [[purescala.Constructors#orJoin purescala's constructor orJoin]]
     */
-  case class Or(exprs: Seq[Expr]) extends Expr {
+  case class Or(exprs: Seq[Expr]) extends Expr with CachingTyped {
     require(exprs.size >= 2)
     protected def computeType(implicit s: Symbols): Type = {
       if (exprs forall (_.getType == BooleanType)) BooleanType
@@ -506,7 +506,7 @@ trait Expressions { self: Trees =>
     *
     * @see [[leon.purescala.Constructors.implies]]
     */
-  case class Implies(lhs: Expr, rhs: Expr) extends Expr {
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type = {
       if(lhs.getType == BooleanType && rhs.getType == BooleanType) BooleanType
       else Untyped
@@ -517,7 +517,7 @@ trait Expressions { self: Trees =>
     *
     * @see [[leon.purescala.Constructors.not]]
     */
-  case class Not(expr: Expr) extends Expr {
+  case class Not(expr: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type = {
       if (expr.getType == BooleanType) BooleanType
       else bitVectorType(expr.getType)
@@ -683,19 +683,19 @@ trait Expressions { self: Trees =>
   }
 
   /** $encodingof `... > ...`*/
-  case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr {
+  case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr with CachingTyped{
     protected def computeType(implicit s: Symbols): Type =
       if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
   }
 
   /** $encodingof `... <= ...`*/
-  case class LessEquals(lhs: Expr, rhs: Expr) extends Expr {
+  case class LessEquals(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type =
       if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
   }
 
   /** $encodingof `... >= ...`*/
-  case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr {
+  case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type =
       if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
   }
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index a02aec44961dd0e88414383601462384055e098d..050f9a48574c0e0d37d20d78b2a510c0626c2e5f 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -299,7 +299,7 @@ trait Extractors { self: Trees =>
 
     def unapply(me: MatchExpr) : Option[(Pattern, Expr, Expr)] = {
       Option(me) collect {
-        case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliased(pattern.binders, exprOps.variablesOf(scrut)) =>
+        case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliasedSymbols(pattern.binders, exprOps.variablesOf(scrut)) =>
           ( pattern, scrut, body )
       }
     }
diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala
index 9295687bb38c4d32e2b6c02bf406da1f7e41d980..a8a6bdf3acfbe0616040e29aef0d37950fe5db84 100644
--- a/src/main/scala/inox/ast/Trees.scala
+++ b/src/main/scala/inox/ast/Trees.scala
@@ -109,7 +109,7 @@ trait Trees extends Expressions with Extractors with Types with Definitions with
     (s1 & s2).nonEmpty
   }
 
-  def aliased[T1 <: VariableSymbol,T2 <: VariableSymbol](vs1: Set[T1], vs2: Set[T2]): Boolean = {
+  def aliasedSymbols[T1 <: VariableSymbol,T2 <: VariableSymbol](vs1: Set[T1], vs2: Set[T2]): Boolean = {
     aliased(vs1.map(_.id), vs2.map(_.id))
   }
 }
diff --git a/src/main/scala/inox/evaluators/Evaluator.scala b/src/main/scala/inox/evaluators/Evaluator.scala
index ce913f77f7022efcd64ebbf47d85c41d71450f1a..b9069f65f681a8c094c1bee6d5eeff7dbd92445f 100644
--- a/src/main/scala/inox/evaluators/Evaluator.scala
+++ b/src/main/scala/inox/evaluators/Evaluator.scala
@@ -3,8 +3,11 @@
 package inox
 package evaluators
 
+case class EvaluatorOptions(options: Seq[InoxOption[Any]]) extends InoxOptions
+
 trait Evaluator {
   val program: Program
+  val options: EvaluatorOptions
   import program.trees._
 
   /** The type of value that this [[Evaluator]] calculates
diff --git a/src/main/scala/inox/evaluators/SolvingEvalInterface.scala b/src/main/scala/inox/evaluators/SolvingEvalInterface.scala
deleted file mode 100644
index 55e8b84dbeaf3a922edc8aa2c3d3285526a8513a..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/evaluators/SolvingEvalInterface.scala
+++ /dev/null
@@ -1,37 +0,0 @@
-
-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
index e05333f49c550166196f1d061d8834a1b2c56792..9b5aee6aeb2cd97ce74c1f7f0439ccec02b0a124 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -3,101 +3,88 @@
 package inox
 package evaluators
 
+import solvers._
+
 import scala.collection.mutable.{Map => MutableMap}
 
 trait SolvingEvaluator extends Evaluator {
 
-  object bankOption extends InoxOptionDef[EvaluationBank] {
+  object optForallCache extends InoxOptionDef[MutableMap[program.trees.Forall, Boolean]] {
     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
-    }
+    def default = MutableMap.empty
   }
 
-  val solver: SolverFactory[Solver]
+  def getSolver(opts: InoxOption[Any]*): Solver { val program: SolvingEvaluator.this.program.type }
 }
 
-/* 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
-  }
+trait SolvingEvalInterface {
+  val program: Program
+  import program._
+  import program.trees._
+  import program.symbols._
 
-  /* 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
-}
+  val evaluator: DeterministicEvaluator with SolvingEvaluator { val program: SolvingEvalInterface.this.program.type }
 
-case class Complete(success: Boolean) extends CheckStatus
-case object Pending extends CheckStatus
-case object NoCheck extends CheckStatus
+  private val specCache: MutableMap[Expr, Expr] = MutableMap.empty
+  private val forallCache: MutableMap[Forall, Expr] = MutableMap.empty
 
-object EvaluationBank {
-  def empty(p: Program): EvaluationBank { val program: p.type } = new EvaluationBank {
-    val program: p.type = p
-    val checkCache = MutableMap.empty
-  }
+  def onSpecInvocation(specs: Expr): Expr = specCache.getOrElseUpdate(specs, {
+    val Seq(free) = exprOps.variablesOf(specs).toSeq
+    val timer = ctx.timers.evaluators.specs.start()
 
-  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
-  }
-}
+    val solver = evaluator.getSolver(evaluator.options.options.collect {
+      case o @ InoxOption(opt, _) if opt == evaluator.optForallCache => o
+    }.toSeq : _*)
 
-trait EvaluationBank {
-  implicit val program: Program
-  import program._
-  import program.trees._
+    solver.assertCnstr(specs)
+    val res = solver.check(model = true)
+    timer.stop()
 
-  /* 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
-    })
-  }
+    res match {
+      case solver.Model(model) =>
+        valuateWithModel(model)(free.toVal)
 
-  /* Update the cache with the invariant check result for `cc` */
-  def invariantResult(cc: CaseClass, success: Boolean): Unit = synchronized {
-    checkCache(cc) = Complete(success)
-  }
+      case _ =>
+        throw new RuntimeException("Failed to evaluate specs " + specs.asString)
+    }
+  })
+
+  def onForallInvocation(forall: Forall): Expr = {
+    val cache = evaluator.options.findOption(evaluator.optForallCache).getOrElse {
+      throw new RuntimeException("Couldn't find evaluator's forall cache")
+    }
+    
+    BooleanLiteral(cache.getOrElse(forall, {
+      val timer = ctx.timers.evaluators.forall.start()
 
-  override def clone: EvaluationBank { val program: EvaluationBank.this.program.type } =
-    EvaluationBank(program)(checkCache.clone)
+      val solver = evaluator.getSolver(
+        InoxOption(optSilentErrors)(true),
+        InoxOption(optCheckModels)(false),
+        InoxOption(evaluator.optForallCache)(cache)
+      )
+
+      solver.assertCnstr(Not(forall.body))
+      val res = solver.check(model = true)
+      timer.stop()
+
+      res match {
+        case solver.Unsat() =>
+          cache(forall) = true
+          true
+
+        case solver.Model(model) =>
+          cache(forall) = false
+          evaluator.eval(Not(forall.body), model) match {
+            case EvaluationResults.Successful(BooleanLiteral(true)) => false
+            case _ => throw new RuntimeException("Forall model check failed")
+          }
+
+        case _ =>
+          throw new RuntimeException("Failed to evaluate forall " + forall.asString)
+      }
+    }))
+  }
 }
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index 549d5ca75a87b6ad49159b69e63c04ba3ea02138..20d6efe7a960285f7ca3c857bbecef3b5a801816 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -6,16 +6,21 @@ package solvers
 import utils._
 import evaluators._
 
-case class SolverOptions(options: Seq[InoxOption[Any]]) {
-  def set(opts: Seq[LeonOption[Any]]): SolverOptions = {
+case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions {
+  def set(opts: Seq[InoxOption[Any]]): SolverOptions = {
     val changed = opts.map(_.optionDef).toSet
     val remainingOpts = options.filter { case InoxOption(optDef, _) => !changed(optDef) }
     copy(options = remainingOpts ++ opts)
   }
+
+  def set(opt: InoxOption[Any], opts: InoxOption[Any]*): SolverOptions = set(opt +: opts)
 }
 
 case object DebugSectionSolver extends DebugSection("solver")
 
+object optCheckModels  extends InoxFlagOptionDef("checkmodels",  "Double-check counter-examples with evaluator", false)
+object optSilentErrors extends InoxFlagOptionDef("silenterrors", "Fail silently into UNKNOWN when encountering an error", false)
+
 trait Solver extends Interruptible {
   def name: String
   val program: Program
@@ -25,13 +30,55 @@ trait Solver extends Interruptible {
   import program.trees._
 
   sealed trait SolverResponse
-  sealed trait SolverCheckResponse extends SolverResponse
-  sealed trait SolverModelResponse extends SolverResponse
+  case object Unknown extends SolverResponse
+
+  sealed trait SolverUnsatResponse extends SolverResponse
+  case object UnsatResponse extends SolverUnsatResponse
+  case class UnsatResponseWithCores(cores: Set[Expr]) extends SolverUnsatResponse
+
+  sealed trait SolverSatResponse extends SolverResponse
+  case object SatResponse extends SolverSatResponse
+  case class SatResponseWithModel(model: Map[ValDef, Expr]) extends SolverSatResponse
+
+  object Check {
+    def unapply(resp: SolverResponse): Option[Boolean] = resp match {
+      case _: SolverUnsatResponse => Some(false)
+      case _: SolverSatResponse   => Some(true)
+      case Unknown => None
+    }
+  }
 
-  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 Sat {
+    def unapply(resp: SolverSatResponse): Boolean = resp match {
+      case SatResponse => true
+      case SatResponseWithModel(_) => throw FatalError("Unexpected sat response with model")
+      case _ => false
+    }
+  }
+
+  object Model {
+    def unapply(resp: SolverSatResponse): Option[Map[ValDef, Expr]] = resp match {
+      case SatResponseWithModel(model) => Some(model)
+      case SatResponse => throw FatalError("Unexpected sat response without model")
+      case _ => None
+    }
+  }
+
+  object Unsat {
+    def unapply(resp: SolverUnsatResponse): Boolean = resp match {
+      case UnsatResponse => true
+      case UnsatResponseWithCores(_) => throw FatalError("Unexpected unsat response with cores")
+      case _ => false
+    }
+  }
+
+  object Core {
+    def unapply(resp: SolverUnsatResponse): Option[Set[Expr]] = resp match {
+      case UnsatResponseWithCores(cores) => Some(cores)
+      case UnsatResponse => throw FatalError("Unexpected unsat response with cores")
+      case _ => None
+    }
+  }
 
   object SolverUnsupportedError {
     def msg(t: Tree, reason: Option[String]) = {
@@ -49,10 +96,9 @@ trait Solver extends Interruptible {
 
   def assertCnstr(expression: Expr): Unit
 
-  /** Returns Some(true) if it found a satisfying model, Some(false) if no model exists, and None otherwise */
-  def check: Option[Boolean]
-  /** Returns the model if it exists */
-  def getModel: Model
+  def check(model: Boolean = false, cores: Boolean = false): SolverResponse
+  def checkAssumptions(model: Boolean = false, cores: Boolean = false)(assumptions: Set[Expr]): SolverResponse
+  
   def getResultSolver: Option[Solver] = Some(this)
 
   def free()
@@ -62,9 +108,6 @@ trait Solver extends Interruptible {
   def push(): Unit
   def pop(): Unit
 
-  def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
-  def getUnsatCore: Set[Expr]
-
   protected def unsupported(t: Tree): Nothing = {
     val err = SolverUnsupportedError(t, None)
     reporter.warning(err.getMessage)