Ordering on characters

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
   }
 
 

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"