diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 3d6d4064d3023d1d2cc11b31908fa58588db91cf..9c87a1acb16cb3ee23080ea9753e1558b968f399 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -466,25 +466,33 @@ trait Expressions { self: Trees =>
   /** $encodingof `... < ...`*/
   case class LessThan(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
+      if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType
+      else if (lhs.getType == CharType && rhs.getType == CharType) BooleanType
+      else Untyped
   }
 
   /** $encodingof `... > ...`*/
   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
+      if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType
+      else if (lhs.getType == CharType && rhs.getType == CharType) BooleanType
+      else Untyped
   }
 
   /** $encodingof `... <= ...`*/
   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
+      if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType
+      else if (lhs.getType == CharType && rhs.getType == CharType) BooleanType
+      else Untyped
   }
 
   /** $encodingof `... >= ...`*/
   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
+      if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType
+      else if (lhs.getType == CharType && rhs.getType == CharType) BooleanType
+      else Untyped
   }
 
 
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index bd013e591f919c9c7a9aa2c6816562c69fdb1b91..e180bc0f370fc5c27e0c2e00ea1dac4af42233e9 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -254,6 +254,7 @@ trait Printers {
     case BagAdd(b, e) => p"$b + $e"
     case MultiplicityInBag(e, b) => p"$b($e)"
     case MapApply(m, k) => p"$m($k)"
+    case MapUpdated(m, k, v) => p"$m.updated($k, $v)"
 
     case Not(expr) => p"\u00AC$expr"