diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 27ac8db615fabd1c9e6b489bdfa510b761d4ee5a..af0858fbc0020a898bed3e753b2feba6fd25b027 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -239,7 +239,12 @@ trait Printers {
     }
     case fs @ FiniteSet(rs, _) => p"{${rs.distinct}}"
     case fs @ FiniteBag(rs, _) => p"{${rs.toMap.toSeq}}"
-    case fm @ FiniteMap(rs, _, _, _) => p"{${rs.toMap.toSeq}}"
+    case fm @ FiniteMap(rs, dflt, _, _) =>
+      if (rs.isEmpty) {
+        p"{* -> $dflt}"
+      } else {
+        p"{${rs.toMap.toSeq}, * -> $dflt}"
+      }
     case Not(ElementOfSet(e, s)) => p"$e \u2209 $s"
     case ElementOfSet(e, s) => p"$e \u2208 $s"
     case SubsetOf(l, r) => p"$l \u2286 $r"
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index b90817b9339e84db5c276bd0337e6fecbd339b07..72b736e0c46b60c2be0161f3093065e0e9a572c0 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -39,15 +39,11 @@ trait AbstractSolver extends Interruptible {
     extends Unsupported(t, SolverUnsupportedError.msg(t,reason))
 
   protected def unsupported(t: Tree): Nothing = {
-    val err = SolverUnsupportedError(t, None)
-    reporter.warning(err.getMessage)
-    throw err
+    throw SolverUnsupportedError(t, None)
   }
 
   protected def unsupported(t: Tree, str: String): Nothing = {
-    val err = SolverUnsupportedError(t, Some(str))
-    reporter.warning(err.getMessage)
-    throw err
+    throw SolverUnsupportedError(t, Some(str))
   }
 
   def assertCnstr(expression: Trees): Unit
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index dfbeebdaa053d38f1598db89cde50a229112de93..ad9f5daf9523d16c402731c7da03311bee08eea9 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -322,8 +322,10 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
 
       case al @ MapApply(a, i) =>
         ArraysEx.Select(toSMT(a), toSMT(i))
+
       case al @ MapUpdated(map, k, v) =>
         ArraysEx.Store(toSMT(map), toSMT(k), toSMT(v))
+
       case ra @ FiniteMap(elems, default, keyTpe, valueType) =>
         val s = declareSort(ra.getType)