diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 08e25f437b895c788a86d1eaefe7048fa09451de..119ac9df4174060dfc28a0ec4bf8fe3079660399 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -286,7 +286,7 @@ trait Expressions { self: Trees =>
     require(exprs.size >= 2)
     protected def computeType(implicit s: Symbols): Type = {
       if (exprs forall (_.getType == BooleanType)) BooleanType
-      else bitVectorType(exprs.head.getType, exprs.tail.map(_.getType) : _*)
+      else Untyped
     }
   }
 
@@ -304,7 +304,7 @@ trait Expressions { self: Trees =>
     require(exprs.size >= 2)
     protected def computeType(implicit s: Symbols): Type = {
       if (exprs forall (_.getType == BooleanType)) BooleanType
-      else bitVectorType(exprs.head.getType, exprs.tail.map(_.getType) : _*)
+      else Untyped
     }
   }
 
@@ -333,7 +333,7 @@ trait Expressions { self: Trees =>
   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)
+      else Untyped
     }
   }
 
@@ -474,6 +474,12 @@ trait Expressions { self: Trees =>
 
 
   /* Bit-vector operations */
+
+  /** $encodingof `~...` $noteBitvector */
+  case class BVNot(e: Expr) extends Expr with CachingTyped {
+    protected def computeType(implicit s: Symbols): Type = bitVectorType(e.getType)
+  }
+
   /** $encodingof `... | ...` $noteBitvector */
   case class BVOr(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type = bitVectorType(lhs.getType, rhs.getType)
@@ -654,7 +660,7 @@ trait Expressions { self: Trees =>
       MapType(keyType, default.getType).unveilUntyped
   }
 
-  /** $encodingof `map.apply(key)` (or `map(key)`)*/
+  /** $encodingof `map.apply(key)` (or `map(key)`) */
   case class MapApply(map: Expr, key: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type = map.getType match {
       case MapType(from, to) => checkParamTypes(Seq(key.getType), Seq(from), to)
@@ -662,6 +668,7 @@ trait Expressions { self: Trees =>
     }
   }
 
+  /** $encodingof `map.updated(key, value)` (or `map + (key -> value)`) */
   case class MapUpdated(map: Expr, key: Expr, value: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols) = map.getType match {
       case mt@MapType(from, to) => checkParamTypes(Seq(key.getType, value.getType), Seq(from, to), mt)
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index 6c457f342220e4d1efbd6031770053e46220a883..0ae72adf1157c017f4516a73aaaeb27f7f39393c 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -96,7 +96,6 @@ trait RecursiveEvaluator
     case And(Seq(e1, e2)) =>
       (e(e1), e(e2)) match {
         case (BooleanLiteral(b1), BooleanLiteral(b2)) => BooleanLiteral(b1 && b2)
-        case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(i1 & i2, s1)
         case (le, re) => throw EvalError("Unexpected operation: (" + le.asString + ") && (" + re.asString + ")")
       }
 
@@ -106,7 +105,6 @@ trait RecursiveEvaluator
     case Or(Seq(e1, e2)) =>
       (e(e1), e(e2)) match {
         case (BooleanLiteral(b1), BooleanLiteral(b2)) => BooleanLiteral(b1 || b2)
-        case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(i1 | i2, s1)
         case (le, re) => throw EvalError("Unexpected operation: (" + le.asString + ") || (" + re.asString + ")")
       }
 
@@ -116,8 +114,6 @@ trait RecursiveEvaluator
     case Not(arg) =>
       e(arg) match {
         case BooleanLiteral(v) => BooleanLiteral(!v)
-        case BVLiteral(bs, s) =>
-          BVLiteral(BitSet.empty ++ (1 to s).flatMap(i => if (bs(i)) None else Some(i)), s)
         case other => throw EvalError(typeErrorMsg(other, BooleanType))
       }
 
@@ -296,6 +292,25 @@ trait RecursiveEvaluator
         case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") % (" + re.asString + ")")
       }
 
+    case BVNot(b) =>
+      e(b) match {
+        case BVLiteral(bs, s) =>
+          BVLiteral(BitSet.empty ++ (1 to s).flatMap(i => if (bs(i)) None else Some(i)), s)
+        case other => throw EvalError("Unexpected operation: ~(" + other.asString + ")")
+      }
+
+    case BVAnd(l, r) =>
+      (e(l), e(r)) match {
+        case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(i1 & i2, s1)
+        case (le, re) => throw EvalError("Unexpected operation: (" + le.asString + ") & (" + re.asString + ")")
+      }
+
+    case BVOr(l, r) =>
+      (e(l), e(r)) match {
+        case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(i1 | i2, s1)
+        case (le, re) => throw EvalError("Unexpected operation: (" + le.asString + ") | (" + re.asString + ")")
+      }
+
     case BVXOr(l,r) =>
       (e(l), e(r)) match {
         case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(i1 ^ i2, s1)
@@ -498,6 +513,14 @@ trait RecursiveEvaluator
         throw EvalError(typeErrorMsg(l, MapType(r.getType, g.getType)))
     }
 
+    case g @ MapUpdated(m, k, v) => (e(m), e(k), e(v)) match {
+      case (FiniteMap(ss, dflt, tpe), ek, ev) =>
+        FiniteMap((ss.toMap + (ek -> ev)).toSeq, dflt, tpe)
+      case (m,l,r) =>
+        throw EvalError("Unexpected operation: " + m.asString +
+          ".updated(" + l.asString + ", " + r.asString + ")")
+    }
+
     case gl: GenericValue => gl
     case fl : FractionLiteral => normalizeFraction(fl)
     case l : Literal[_] => l