diff --git a/src/main/scala/leon/LeonFatalError.scala b/src/main/scala/leon/LeonExceptions.scala
similarity index 59%
rename from src/main/scala/leon/LeonFatalError.scala
rename to src/main/scala/leon/LeonExceptions.scala
index 70646a94c0a8951707cdae55051474d299a64fc1..eeaadd09a736416aa6f6eeab93cc7e51a17e8072 100644
--- a/src/main/scala/leon/LeonFatalError.scala
+++ b/src/main/scala/leon/LeonExceptions.scala
@@ -2,8 +2,13 @@
 
 package leon
 
+import purescala.Common.Tree
+
 case class LeonFatalError(msg: Option[String]) extends Exception(msg.getOrElse(""))
 
 object LeonFatalError {
   def apply(msg: String) = new LeonFatalError(Some(msg))
 }
+
+class Unsupported(t: Tree, msg: String)(implicit ctx: LeonContext)
+  extends Exception(s"${t.asString}@${t.getPos} $msg")
\ No newline at end of file
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 3d7fbe17d48bedf12e60ca4044587a9a8d06ca99..54e3485d6cad2520f8d5dd03b64c9e3fedc60ce9 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -178,9 +178,12 @@ class CompilationUnit(val ctx: LeonContext,
       }
       l
 
-    // Just slightly overkill...
     case _ =>
-      compileExpression(e, Seq()).evalToJVM(Seq(),monitor)
+      throw LeonFatalError("Unexpected expression in exprToJVM")
+
+    // Just slightly overkill...
+    //case _ =>
+    //  compileExpression(e, Seq()).evalToJVM(Seq(),monitor)
   }
 
   // Note that this may produce untyped expressions! (typically: sets, maps)
@@ -274,9 +277,9 @@ class CompilationUnit(val ctx: LeonContext,
 
   var compiledN = 0
 
-  def compileExpression(e: Expr, args: Seq[Identifier]): CompiledExpression = {
+  def compileExpression(e: Expr, args: Seq[Identifier])(implicit ctx: LeonContext): CompiledExpression = {
     if(e.getType == Untyped) {
-      throw new IllegalArgumentException(s"Cannot compile untyped expression [$e].")
+      throw new Unsupported(e, s"Cannot compile untyped expression.")
     }
 
     compiledN += 1
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 72a905b82af310110c1aa83e72ec2409d4406fa7..0cf311562c9ffe37020186cf96365ba5b15b8178 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -236,7 +236,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
 
       val newExpr = replaceFromIDs(map, expression)
 
-      val ce = unit.compileExpression(newExpr, Seq(tid))
+      val ce = unit.compileExpression(newExpr, Seq(tid))(ctx)
 
       Some((args : Expr) => {
         try {
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index caf22c1e911e54870c89727b657cba718d6bc810..64456226b16815c056202738c7946c2e0cef9968 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -36,7 +36,7 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
 
     ctx.timers.evaluators.codegen.compilation.start()
     try {
-      val ce = unit.compileExpression(expression, argorder)
+      val ce = unit.compileExpression(expression, argorder)(ctx)
 
       Some((args : Seq[Expr]) => {
         try {
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 4399dc2bfd84fae98155006144b60e7c9a84a114..f04cbc99fa2b14391d8982ef108eb9b2ea47a868 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -33,8 +33,15 @@ object Common {
     * The name is stored in the decoded (source code) form rather than encoded (JVM) form.
     * The type may be left blank (Untyped) for Identifiers that are not variables.
     */
-  class Identifier private[Common](val name: String, val globalId: Int, val id: Int, val tpe: TypeTree, alwaysShowUniqueID: Boolean = false) extends Tree with Typed {
-    self : Serializable =>
+  class Identifier private[Common](
+    val name: String,
+    private[Common] val globalId: Int,
+    private[Common] val id: Int,
+    private val tpe: TypeTree,
+    private val alwaysShowUniqueID: Boolean = false
+  ) extends Tree with Typed with Ordered[Identifier] {
+
+    self: Serializable =>
 
     val getType = tpe
 
@@ -47,27 +54,27 @@ object Common {
     override def hashCode: Int = globalId
 
     override def toString: String = {
-      if(alwaysShowUniqueID) {
-        name + (if(id > 0) id else "")
+      if (alwaysShowUniqueID) {
+        name + (if (id > 0) id else "")
       } else {
         name
       }
     }
 
-    def uniqueName : String = name + id
+    def uniqueNameDelimited(delim: String) = name + delim + id
 
-    def toVariable : Variable = Variable(this)
+    def uniqueName: String = uniqueNameDelimited("")
 
-    def freshen: Identifier = FreshIdentifier(name, tpe, alwaysShowUniqueID).copiedFrom(this)
+    def toVariable: Variable = Variable(this)
 
-  }
-
-  implicit object IdentifierOrdering extends Ordering[Identifier] {
-    def compare(a: Identifier, b: Identifier) = {
-      val ord = implicitly[Ordering[Tuple3[String, Int, Int]]]
+    def freshen: Identifier = FreshIdentifier(name, tpe, alwaysShowUniqueID).copiedFrom(this)
 
-      ord.compare((a.name, a.id, a.globalId),
-                  (b.name, b.id, b.globalId))
+    override def compare(that: Identifier): Int = {
+      val ord = implicitly[Ordering[(String, Int, Int)]]
+      ord.compare(
+        (this.name, this.id, this.globalId),
+        (that.name, that.id, that.globalId)
+      )
     }
   }
 
diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala
index 3339fe2b79de7c8fa1d2b7c0509ffa2da1be4f75..e811feaa1dda6886fa9c9ad927c6f552efb7b7a1 100644
--- a/src/main/scala/leon/solvers/ADTManager.scala
+++ b/src/main/scala/leon/solvers/ADTManager.scala
@@ -49,9 +49,11 @@ class ADTManager(ctx: LeonContext) {
 
     if (conflicts(t)) {
       // There is no way to solve this, the type we requested is in conflict
-      reporter.warning(s"Encountered ADT '$t' that can't be defined.")
-      reporter.warning("It appears it has recursive references through non-structural types (such as arrays, maps, or sets).")
-      throw new IllegalArgumentException
+      val str = "Encountered ADT that can't be defined.\n" +
+        "It appears it has recursive references through non-structural types (such as arrays, maps, or sets)."
+      val err = new Unsupported(t, str)(ctx)
+      reporter.warning(err.getMessage)
+      throw err
     } else {
       // We might be able to define some despite conflicts
       if (conflicts.isEmpty) {
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 9f8aaace4a8ed890212cc57961471ed2d3a62c00..a9018b2defa113783cd88dd166d5a01c1e6256a4 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -5,7 +5,7 @@ package solvers
 
 import utils.{DebugSectionSolver, Interruptible}
 import purescala.Expressions._
-import purescala.Common.Identifier
+import leon.purescala.Common.{Tree, Identifier}
 import verification.VC
 
 trait Solver extends Interruptible {
@@ -33,6 +33,17 @@ trait Solver extends Interruptible {
   def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
   def getUnsatCore: Set[Expr]
 
+  protected def unsupported(t: Tree): Nothing = {
+    val err = SolverUnsupportedError(t, this, None)
+    leonContext.reporter.warning(err.getMessage)
+    throw err
+  }
+  protected def unsupported(t: Tree, str: String): Nothing = {
+    val err = SolverUnsupportedError(t, this, Some(str))
+    leonContext.reporter.warning(err.getMessage)
+    throw err
+  }
+
   implicit val debugSection = DebugSectionSolver
 
   private[solvers] def debugS(msg: String) = {
diff --git a/src/main/scala/leon/solvers/SolverUnsupportedError.scala b/src/main/scala/leon/solvers/SolverUnsupportedError.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5d519160d7aed9fce7a42584c8d53806e53e265a
--- /dev/null
+++ b/src/main/scala/leon/solvers/SolverUnsupportedError.scala
@@ -0,0 +1,15 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers
+
+import purescala.Common.Tree
+
+object SolverUnsupportedError {
+  def msg(t: Tree, s: Solver, reason: Option[String]) = {
+    s" is unsupported by solver ${s.name}" + reason.map(":\n  " + _ ).getOrElse("")
+  }
+}
+
+case class SolverUnsupportedError(t: Tree, s: Solver, reason: Option[String] = None)
+  extends Unsupported(t, SolverUnsupportedError.msg(t,s,reason))(s.leonContext)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 83076f8dc6c0bf3588697370e52d0f2d49bc4df4..86da0be80db1c8eec85f6dedc6972871ced49ad3 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -6,6 +6,7 @@ package solvers.smtlib
 import leon.purescala.Common.Identifier
 import leon.purescala.Definitions.Program
 import leon.purescala.Expressions.Expr
+import leon.solvers.SolverUnsupportedError
 import smtlib.parser.Commands.{Assert => SMTAssert}
 import smtlib.parser.Terms.{Exists => SMTExists}
 
@@ -31,7 +32,7 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
   override def assertCnstr(e: Expr) = try {
     sendCommand(SMTAssert(quantifiedTerm(SMTExists, e)))
   } catch {
-    case _: IllegalArgumentException =>
+    case _ : SolverUnsupportedError =>
       addError()
   }
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 6bc216b535c746664ae2cb4ace9fe591af206134..232867dcc3896a935fff05127dfe944a59f43822 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -3,6 +3,7 @@
 package leon
 package solvers.smtlib
 
+import leon.solvers.SolverUnsupportedError
 import purescala._
 import Expressions._
 import Definitions._
@@ -51,7 +52,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
 
         Seq(bodyAssert) ++ specAssert
       } catch {
-        case _ : IllegalArgumentException =>
+        case _ : SolverUnsupportedError =>
           addError()
           Seq()
       }
@@ -79,7 +80,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
           (p.id, id2sym(p.id): Term)
         }.toMap)
       } catch {
-        case _: IllegalArgumentException =>
+        case _: SolverUnsupportedError =>
           addError()
           toSMT(Error(tfd.body.get.getType, ""))(Map())
       }
@@ -101,7 +102,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
         try {
           sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)))
         } catch {
-          case _ : IllegalArgumentException =>
+          case _ : SolverUnsupportedError =>
             addError()
         }
       }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 801a71662c2c6b37e519c0f4bf43b79b61a11b72..fa11aa42159144eb8423a8dab8f5c98fe07d6aa7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -96,9 +96,9 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
       FiniteSet(se ++ selems, base)
 
     case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
-      FiniteSet(elems.map(fromSMT(_, tpe) match {
+      FiniteSet(elems.flatMap(fromSMT(_, tpe) match {
         case FiniteSet(elems, _) => elems
-      }).flatten.toSet, base)
+      }).toSet, base)
 
     // FIXME (nicolas)
     // some versions of CVC4 seem to generate array constants with "as const" notation instead of the __array_store_all__
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 25b7a6c0f7115ba3999ff536919502285883e366..29540f2f4cbb255dbd1f58d1070ef16b37620b69 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -28,7 +28,6 @@ import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
 import _root_.smtlib.theories._
 import _root_.smtlib.{Interpreter => SMTInterpreter}
 
-
 abstract class SMTLIBSolver(val context: LeonContext,
                             val program: Program) extends Solver with NaiveAssumptionSolver {
 
@@ -109,7 +108,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
   protected val library = program.library
 
-  protected def id2sym(id: Identifier): SSymbol = SSymbol(id.name+"!"+id.id)
+  protected def id2sym(id: Identifier): SSymbol = SSymbol(id.uniqueNameDelimited("!"))
 
   protected def freshSym(id: Identifier): SSymbol = freshSym(id.name)
   protected def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
@@ -160,7 +159,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
   protected def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
     case SetType(base) =>
       if (r.default != BooleanLiteral(false)) {
-        unsupported("Co-finite sets are not supported.")
+        unsupported(r, "Solver returned a co-finite set which is not supported.")
       }
       require(r.keyTpe == base, s"Type error in solver model, expected $base, found ${r.keyTpe}")
 
@@ -176,7 +175,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
       // We expect a RawArrayValue with keys in from and values in Option[to],
       // with default value == None
       if (r.default.getType != library.noneType(to)) {
-        unsupported("Co-finite maps are not supported.")
+        unsupported(r, "Solver returned a co-finite map which is not supported.")
       }
       require(r.keyTpe == from, s"Type error in solver model, expected $from, found ${r.keyTpe}")
 
@@ -186,13 +185,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
       }.toSeq
       FiniteMap(elems, from, to)
 
-    case _ =>
-      unsupported("Unable to extract from raw array for "+tpe)
-  }
-
-  protected def unsupported(str: String) = {
-    reporter.warning(s"Unsupported in smt-$targetName: $str")
-    throw new IllegalArgumentException(str)
+    case other =>
+      unsupported(other, "Unable to extract from raw array for "+tpe)
   }
 
   protected def declareSort(t: TypeTree): Sort = {
@@ -223,8 +217,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
         case _: ClassType | _: TupleType | _: ArrayType | UnitType =>
           declareStructuralSort(tpe)
 
-        case _ =>
-          unsupported("Sort "+t)
+        case other =>
+          unsupported(other, s"Could not transform $other into an SMT sort")
       }
     }
   }
@@ -565,7 +559,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
           )
         }
       case o =>
-        unsupported(s"Tree ${o.asString}")
+        unsupported(o, "")
     }
   }
 
@@ -605,7 +599,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
         case cct: CaseClassType =>
           CaseClass(cct, Nil)
         case t =>
-          unsupported("woot? for a single constructor for non-case-object: "+t.asString)
+          unsupported(t, "woot? for a single constructor for non-case-object")
       }
 
     case (SimpleSymbol(s), tpe) if lets contains s =>
@@ -613,7 +607,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
     case (SimpleSymbol(s), _) =>
       variables.getA(s).map(_.toVariable).getOrElse {
-        unsupported("Unknown symbol: "+s)
+        reporter.fatalError("Unknown symbol: "+s)
       }
 
     case (FunctionApplication(SimpleSymbol(SSymbol("ite")), Seq(cond, thenn, elze)), t) =>
@@ -649,7 +643,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
           }
 
         case t =>
-          unsupported("Woot? structural type that is non-structural: "+t)
+          unsupported(t, "Woot? structural type that is non-structural")
       }
 
     // EK: Since we have no type information, we cannot do type-directed
@@ -676,13 +670,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
           }
 
         case _ =>
-          unsupported("Function "+app+" not handled in fromSMT: "+s)
+          reporter.fatalError("Function "+app+" not handled in fromSMT: "+s)
       }
     }
     case (QualifiedIdentifier(id, sort), tpe) =>
-      unsupported("Unhandled case in fromSMT: " + id +": "+sort +" ("+tpe+")")
+      reporter.fatalError("Unhandled case in fromSMT: " + id +": "+sort +" ("+tpe+")")
     case _ =>
-      unsupported("Unhandled case in fromSMT: " + (s, tpe))
+      reporter.fatalError("Unhandled case in fromSMT: " + (s, tpe))
   }
 
 
@@ -719,7 +713,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
       val term = toSMT(expr)(Map())
       sendCommand(SMTAssert(term))
     } catch {
-      case i : IllegalArgumentException =>
+      case _ : SolverUnsupportedError =>
         // Store that there was an error. Now all following check()
         // invocations will return None
         addError()
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index b520dfe5be60f586ae05bda1e48f8bf82c0e70fc..2ec571f1ea2b0580cbb1eef697610256a1e61dc5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -3,6 +3,7 @@
 package leon
 package solvers.smtlib
 
+import leon.solvers.SolverUnsupportedError
 import purescala._
 import DefOps._
 import Definitions._
@@ -63,7 +64,7 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
       try {
         sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)))
       } catch {
-        case _ : IllegalArgumentException =>
+        case _ : SolverUnsupportedError =>
           addError()
       }
     }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 3a7b345fb4d0c4d8664c90a2904ca487bb1199fd..36c4523da55cb3a4fbd9b10d6273d0458d2ccfd1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -79,7 +79,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
         // Need to recover value form function model
         fromRawArray(extractRawArray(letDefs(k), tpe), tpe)
       } else {
-        unsupported(" as-array on non-function or unknown symbol "+k)
+        throw LeonFatalError("Array on non-function or unknown symbol "+k)
       }
 
     case (FunctionApplication(
@@ -141,7 +141,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
         case ArrayType(base) => (Int32Type, base)
         case FunctionType(args, ret) => (tupleTypeWrap(args), ret)
         case RawArrayType(from, to) => (from, to)
-        case _ => unsupported("Unsupported type for (un)packing into raw arrays: "+tpe +" (got kinds "+akind+" -> "+rkind+")")
+        case _ => unsupported(tpe, "Unsupported type for (un)packing into raw arrays (got kinds "+akind+" -> "+rkind+")")
       }
 
       def extractCases(e: Term): (Map[Expr, Expr], Expr) = e match {
@@ -157,7 +157,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
       RawArrayValue(argTpe, cases, default)
 
     case _ =>
-      unsupported("Unable to extract "+s)
+      throw LeonFatalError("Unable to extract "+s)
   }
 
   // EK: We use get-model instead in order to extract models for arrays
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9eb08e152d2b1692787a7974811b6f326692b1b0..9492e8b939d207e0c6150662586f5999773ee877 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -259,11 +259,7 @@ trait AbstractZ3Solver extends Solver {
       }
 
     case other =>
-      sorts.cachedB(other) {
-        reporter.warning(other.getPos, "Resorting to uninterpreted type for : " + other.asString)
-        val symbol = z3.mkIntSymbol(FreshIdentifier("unint").globalId)
-        z3.mkUninterpretedSort(symbol)
-      }
+      throw SolverUnsupportedError(other, this)
   }
 
   protected[leon] def toZ3Formula(expr: Expr, initialMap: Map[Identifier, Z3AST] = Map.empty): Z3AST = {
@@ -545,10 +541,8 @@ trait AbstractZ3Solver extends Solver {
       case gv @ GenericValue(tp, id) =>
         z3.mkApp(genericValueToDecl(gv))
 
-      case _ => {
-        reporter.warning(ex.getPos, "Can't handle this in translation to Z3: " + ex.asString)
-        throw new IllegalArgumentException
-      }
+      case other =>
+        unsupported(other)
     }
 
     rec(expr)
@@ -587,13 +581,11 @@ trait AbstractZ3Solver extends Solver {
                 tpe match {
                   case Int32Type => IntLiteral(hexa.toInt)
                   case CharType  => CharLiteral(hexa.toInt.toChar)
-                  case _ =>
-                    reporter.warning("Unexpected target type for BV value: " + tpe.asString)
-                    throw new IllegalArgumentException
+                  case other =>
+                    unsupported(other, "Unexpected target type for BV value")
                 }
               case None => {
-                reporter.warning("Z3NumeralIntAST with None: " + t)
-                throw new IllegalArgumentException
+                throw LeonFatalError(s"Could not translate hexadecimal Z3 numeral $t")
               }
             }
           } else {
@@ -607,12 +599,10 @@ trait AbstractZ3Solver extends Solver {
                   case Int32Type => IntLiteral(hexa.toInt)
                   case CharType  => CharLiteral(hexa.toInt.toChar)
                   case _ =>
-                    reporter.warning("Unexpected target type for BV value: " + tpe.asString)
-                    throw new IllegalArgumentException
+                    reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
                 }
             case None => {
-              reporter.warning("Z3NumeralIntAST with None: " + t)
-              throw new IllegalArgumentException
+              reporter.fatalError(s"Could not translate Z3NumeralIntAST numeral $t")
             }
           }
         }
@@ -648,12 +638,12 @@ trait AbstractZ3Solver extends Solver {
                   case (s : IntLiteral, RawArrayValue(_, elems, default)) =>
                     val entries = elems.map {
                       case (IntLiteral(i), v) => i -> v
-                      case _ => throw new IllegalArgumentException
+                      case _ => reporter.fatalError("Translation from Z3 to Array failed")
                     }
 
                     finiteArray(entries, Some(s, default), to)
                   case _ =>
-                    throw new IllegalArgumentException
+                    reporter.fatalError("Translation from Z3 to Array failed")
                 }
             }
           } else {
@@ -667,7 +657,7 @@ trait AbstractZ3Solver extends Solver {
                     }
 
                     RawArrayValue(from, entries, default)
-                  case None => throw new IllegalArgumentException
+                  case None => reporter.fatalError("Translation from Z3 to Array failed")
                 }
 
               case tp: TypeParameter =>
@@ -680,8 +670,7 @@ trait AbstractZ3Solver extends Solver {
                     // We expect a RawArrayValue with keys in from and values in Option[to],
                     // with default value == None
                     if (r.default.getType != library.noneType(to)) {
-                      reporter.warning("Co-finite maps are not supported. (Default was "+r.default.asString+")")
-                      throw new IllegalArgumentException
+                      unsupported(r, "Solver returned a co-finite set which is not supported.")
                     }
                     require(r.keyTpe == from, s"Type error in solver model, expected ${from.asString}, found ${r.keyTpe.asString}")
 
@@ -696,7 +685,7 @@ trait AbstractZ3Solver extends Solver {
 
               case FunctionType(fts, tt) =>
                 model.getArrayValue(t) match {
-                  case None => throw new IllegalArgumentException
+                  case None => reporter.fatalError("Translation from Z3 to function value failed")
                   case Some((map, elseZ3Value)) =>
                     val leonElseValue = rec(elseZ3Value, tt)
                     val leonMap = map.toSeq.map(p => rec(p._1, tupleTypeWrap(fts)) -> rec(p._2, tt))
@@ -705,7 +694,7 @@ trait AbstractZ3Solver extends Solver {
 
               case tpe @ SetType(dt) =>
                 model.getSetValue(t) match {
-                  case None => throw new IllegalArgumentException
+                  case None => reporter.fatalError("Translation from Z3 to set failed")
                   case Some(set) =>
                     val elems = set.map(e => rec(e, dt))
                     FiniteSet(elems, dt)
@@ -736,17 +725,17 @@ trait AbstractZ3Solver extends Solver {
             //      case OpIDiv =>    Division(rargs(0), rargs(1))
             //      case OpMod =>     Modulo(rargs(0), rargs(1))
                   case other =>
-                    reporter.warning("Don't know what to do with this declKind : " + other)
-                    reporter.warning("Expected type: " + tpe.asString)
-                    reporter.warning("Tree: " + t)
-                    reporter.warning("The arguments are : " + args)
-                    throw new IllegalArgumentException
+                    reporter.fatalError(
+                      s"""|Don't know what to do with this declKind: $other
+                          |Expected type: ${tpe.asString}
+                          |Tree: $t
+                          |The arguments are: $args""".stripMargin
+                    )
                 }
             }
           }
         case _ =>
-          reporter.warning("Can't handle "+t)
-          throw new IllegalArgumentException
+          reporter.fatalError(s"Don't know what to do with this Z3 tree: $t")
       }
     }
     rec(tree, tpe)
@@ -756,7 +745,7 @@ trait AbstractZ3Solver extends Solver {
     try {
       Some(fromZ3Formula(model, tree, tpe))
     } catch {
-      case e: IllegalArgumentException => None
+      case e: Unsupported => None
     }
   }
 
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index eef9ffb9071d1291831e41a69105e4884168a6aa..a1fc339daf96a9f1e9d47e011bc031cab7358aec 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -218,7 +218,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
         solver.assertCnstr(cl)
       }
     } catch {
-      case _: IllegalArgumentException =>
+      case _: SolverUnsupportedError =>
         addError()
     }
   }
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 48096077736b1cf6e842a5ca87a02ae81b67806b..f745abec94ff5a8f53c6c75aefc267924182df3e 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -192,7 +192,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           grammar.printProductions(printer)
         }
 
-        bsOrdered = bs.toSeq.sortBy(_.id)
+        bsOrdered = bs.toSeq.sorted
 
         setCExpr(computeCExpr())
       }
@@ -545,7 +545,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           for ((c, alts) <- cTree) {
             val activeBs = alts.map(_._1).filter(isBActive)
 
-            val either = for (a1 <- activeBs; a2 <- activeBs if a1.globalId < a2.globalId) yield {
+            val ord = implicitly[Ordering[Identifier]]
+            val either = for (a1 <- activeBs; a2 <- activeBs if a1 < a2) yield {
               Or(Not(a1.toVariable), Not(a2.toVariable))
             }
 
diff --git a/src/test/scala/leon/test/helpers/WithLikelyEq.scala b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
index aee9e7671d5f0d64e4e81bd0a6b82c6b514b2e20..d499f5617fb3edfbeae631836f1f4d07f604e0d5 100644
--- a/src/test/scala/leon/test/helpers/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
@@ -32,7 +32,7 @@ trait WithLikelyEq {
   def checkLikelyEq(ctx: LeonContext, pgm: Program = Program.empty)(e1: Expr, e2: Expr, pre: Option[Expr] = None, values: Map[Identifier, Expr] = Map()): Unit = {
     val evaluator = new DefaultEvaluator(ctx, pgm)
 
-    val freeVars = (variablesOf(e1) ++ variablesOf(e2)).toSeq.sortBy(_.globalId)
+    val freeVars = (variablesOf(e1) ++ variablesOf(e2)).toSeq.sorted
 
     if (freeVars.isEmpty) {
       val r1 = evaluator.eval(e1)