diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index a64226761a0bafe2ac93947ff849e9da417f1088..78874c167980e0ea194be75da2bce015d4b60d5f 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -114,10 +114,7 @@ object Constructors {
       MatchExpr(scrutinee, filtered)
     else 
       Error(
-        cases match {
-          case Seq(hd, _*) => hd.rhs.getType
-          case Seq() => Untyped
-        },
+        cases.headOption.map{ _.rhs.getType }.getOrElse(Untyped),
         "No case matches the scrutinee"
       )
   } 
@@ -255,6 +252,8 @@ object Constructors {
   def minus(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match {
     case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => lhs
     case (_, IntLiteral(0)) => lhs
+    case (InfiniteIntegerLiteral(bi), _) if bi == 0 => UMinus(rhs)
+    case (IntLiteral(0), _) => BVUMinus(rhs)
     case (IsTyped(_, IntegerType), IsTyped(_, IntegerType)) => Minus(lhs, rhs)
     case (IsTyped(_, Int32Type), IsTyped(_, Int32Type)) => BVMinus(lhs, rhs)
   }
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index ed0d630c3df958574e7f7ac4c3f69b256da985e1..117d8ff5aed95da3d7ea91e79121d1114fb9448e 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -47,9 +47,9 @@ object Extractors {
       ))
       case Equals(t1,t2) => Some((t1,t2,Equals))
       case Implies(t1,t2) => Some((t1,t2, implies))
-      case Plus(t1,t2) => Some((t1,t2,Plus))
-      case Minus(t1,t2) => Some((t1,t2,Minus))
-      case Times(t1,t2) => Some((t1,t2,Times))
+      case Plus(t1,t2) => Some((t1,t2,plus))
+      case Minus(t1,t2) => Some((t1,t2,minus))
+      case Times(t1,t2) => Some((t1,t2,times))
       case Division(t1,t2) => Some((t1,t2,Division))
       case Remainder(t1,t2) => Some((t1,t2,Remainder))
       case Modulo(t1,t2) => Some((t1,t2,Modulo))
@@ -57,9 +57,9 @@ object Extractors {
       case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
       case LessEquals(t1,t2) => Some((t1,t2,LessEquals))
       case GreaterEquals(t1,t2) => Some((t1,t2,GreaterEquals))
-      case BVPlus(t1,t2) => Some((t1,t2,BVPlus))
-      case BVMinus(t1,t2) => Some((t1,t2,BVMinus))
-      case BVTimes(t1,t2) => Some((t1,t2,BVTimes))
+      case BVPlus(t1,t2) => Some((t1,t2,plus))
+      case BVMinus(t1,t2) => Some((t1,t2,minus))
+      case BVTimes(t1,t2) => Some((t1,t2,times))
       case BVDivision(t1,t2) => Some((t1,t2,BVDivision))
       case BVRemainder(t1,t2) => Some((t1,t2,BVRemainder))
       case BVAnd(t1,t2) => Some((t1,t2,BVAnd))