diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 8f48d8629a9019ebba5dfab6f0329f10da1acb1a..5ada9b2235518e8fe7a3cc49e329392813c0eb86 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -534,6 +534,9 @@ trait CodeExtraction extends Extractors {
             val tupleType = TupleType(tupleExprs.map(expr => bestRealType(expr.getType)))
             Tuple(tupleExprs).setType(tupleType)
           }
+          case ExErrorExpression(str) =>
+            Error(str).setType(scalaType2PureScala(unit, silent)(nextExpr.tpe))
+
           case ExTupleExtract(tuple, index) => {
             val tupleExpr = rec(tuple)
             val TupleType(tpes) = tupleExpr.getType
@@ -1051,6 +1054,7 @@ trait CodeExtraction extends Extractors {
       case tpe if tpe == IntClass.tpe => Int32Type
       case tpe if tpe == BooleanClass.tpe => BooleanType
       case tpe if tpe == UnitClass.tpe => UnitType
+      case tpe if tpe == NothingClass.tpe => BottomType
       case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) => SetType(rec(btt))
       case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) => MultisetType(rec(btt))
       case TypeRef(_, sym, btt :: Nil) if isOptionClassSym(sym) => OptionType(rec(btt))
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 8245195480b3ecf038e3e41fd209361c23ded5d7..e736f75368e3bede82826bb3fab346d7fc43d9ff 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -175,6 +175,22 @@ trait Extractors {
       }
     }
 
+    object ExIdNamed {
+      def unapply(id: Ident): Option[String] = Some(id.toString)
+    }
+    object ExNamed {
+      def unapply(name: Name): Option[String] = Some(name.toString)
+    }
+
+    object ExErrorExpression {
+      def unapply(tree: Apply) : Option[String] = tree match {
+        case a @ Apply(Select(Select(Select(ExIdNamed("scala"), ExNamed("sys")), ExNamed("package")), ExNamed("error")), List(lit : Literal)) =>
+          Some(lit.value.stringValue)
+        case _ =>
+          None
+      }
+    }
+
     object ExChooseExpression {
       def unapply(tree: Apply) : Option[(List[(Type, Symbol)], Type, Tree, Tree)] = tree match {
         case a @ Apply(
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 31f3e7305c11104972c33e42655a1db687b70ae5..fb1e147857944acfdfcd93f0ddffc81faa2cbcc8 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -426,7 +426,7 @@ object ScalaPrinter {
 
     case e @ Error(desc) => {
       var nsb = sb
-      nsb.append("error(\"" + desc + "\")")
+      nsb.append("sys.error(\"" + desc + "\")")
       nsb
     }
 
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2b5cda8ed885e2bc73b6129e602e7990d77931ba..d00857b9cf52fb0ec041bb8404454871df4699bc 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1173,6 +1173,10 @@ object TreeOps {
             (scrutinees.head, patterns.head)
           }
 
+          // We use searchAndReplace to replace the biggest match first
+          // (topdown).
+          // So replaceing using Map(a => b, CC(a) => d) will replace
+          // "CC(a)" by "d" and not by "CC(b)"
           val newThen = searchAndReplace(substMap.get)(then)
 
           MatchExpr(scrutinee, Seq(SimpleCase(pattern, newThen), SimpleCase(WildcardPattern(None), elze)))
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index ad19ba6c78528032af34f62e5125c58a288197a4..b761841826c82ef89f06bc5e184632dab46f5644 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -14,7 +14,7 @@ class FileInterface(reporter: Reporter, origFile: File) {
     origFile.getAbsolutePath() match {
       case FileExt(path, "scala") =>
         var i = 0
-        def savePath = path+"."+i+".scala"
+        def savePath = path+".scala."+i
         while (new File(savePath).isFile()) {
           i += 1
         }