diff --git a/library/lang/package.scala b/library/lang/package.scala
index c10c025828309a313abb3e02d4d40737737192d4..9c3c72d42efee9268251c2bf9d63091c8460608e 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -70,10 +70,12 @@ package object lang {
   }
   
   implicit class StringDecorations(val underlying: String) {
-    @ignore
-    def bigLength = BigInt(underlying.length)
-    @ignore
-    def bigsubstring(start: BigInt, end: BigInt): String = underlying.substring(start.toInt, end.toInt)
+    @ignore @inline
+    def bigLength() = BigInt(underlying.length)
+    @ignore @inline
+    def bigSubstring(start: BigInt): String = underlying.substring(start.toInt)
+    @ignore @inline
+    def bigSubstring(start: BigInt, end: BigInt): String = underlying.substring(start.toInt, end.toInt)
   }
 
   @ignore
diff --git a/library/theories/String.scala b/library/theories/String.scala
index 7455015784f45fb8e8b0e8d9f239b426be4ce0a1..8057c2d2a72700349574a95e56293ee6a2e9620d 100644
--- a/library/theories/String.scala
+++ b/library/theories/String.scala
@@ -11,7 +11,7 @@ sealed abstract class String {
   }) ensuring (_ >= 0)
   
   def sizeI: Int = this match {
-    case StringCons(_, tail) => 1 + tail.length
+    case StringCons(_, tail) => 1 + tail.sizeI
     case StringNil() => 0
   }
 
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 45ddea6adce805ad06d0326dd3b1e3946a1781cb..02a58ad2930ff51e80d19f22b41029f30d3f999c 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -185,6 +185,39 @@ trait ASTExtractors {
         case _ => None
        }
     }
+    
+    /** Matches the `bigLength` expression at the end of any string expression, and returns the expression.*/
+    object ExBigLengthExpression {
+      def unapply(tree: Apply) : Option[Tree] = tree match {
+        case Apply(Select(
+          Apply(ExSelected("leon", "lang", "package", "StringDecorations"), stringExpr :: Nil),
+          ExNamed("bigLength")), Nil)
+          => Some(stringExpr)
+        case _ => None
+       }
+    }
+    
+    /** Matches the `bigSubstring` method at the end of any string expression, and returns the expression and the start index expression.*/
+    object ExBigSubstringExpression {
+      def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+        case Apply(Select(
+          Apply(ExSelected("leon", "lang", "package", "StringDecorations"), stringExpr :: Nil),
+          ExNamed("bigSubstring")), startExpr :: Nil)
+           => Some(stringExpr, startExpr)
+        case _ => None
+       }
+    }
+    
+    /** Matches the `bigSubstring` expression at the end of any string expression, and returns the expression, the start and end index expressions.*/
+    object ExBigSubstring2Expression {
+      def unapply(tree: Apply) : Option[(Tree, Tree, Tree)] = tree match {
+        case Apply(Select(
+          Apply(ExSelected("leon", "lang", "package", "StringDecorations"), stringExpr :: Nil),
+          ExNamed("bigSubstring")), startExpr :: endExpr :: Nil)
+           => Some(stringExpr, startExpr, endExpr)
+        case _ => None
+       }
+    }
 
     /** Matches an implication `lhs ==> rhs` and returns (lhs, rhs)*/
     object ExImplies {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9c3e4b393792474d8cfcf4e3229d3aeacf1e749c..e37ce4c9816598b07f181b341c426984e5d5e23d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1195,6 +1195,23 @@ trait CodeExtraction extends ASTExtractors {
 
           Ensuring(output_expr, post)
 
+        case t @ ExBigLengthExpression(input) =>
+          val input_expr  =  extractTreeOrNoTree(input).setPos(input.pos)
+          StringBigLength(input_expr)
+        case t @ ExBigSubstringExpression(input, start) =>
+          val input_expr  =  extractTreeOrNoTree(input).setPos(input.pos)
+          val start_expr = extractTreeOrNoTree(start).setPos(start.pos)
+          val s = FreshIdentifier("s", StringType)
+          let(s, input_expr, 
+            BigSubString(Variable(s), start_expr, StringBigLength(Variable(s)))
+          )
+          
+        case t @ ExBigSubstring2Expression(input, start, end) =>
+          val input_expr  =  extractTreeOrNoTree(input).setPos(input.pos)
+          val start_expr = extractTreeOrNoTree(start).setPos(start.pos)
+          val end_expr = extractTreeOrNoTree(end).setPos(end.pos)
+          BigSubString(input_expr, start_expr, end_expr)
+
         case ExAssertExpression(contract, oerr) =>
           val const = extractTree(contract)
           val b     = rest.map(extractTreeOrNoTree).getOrElse(UnitLiteral())
@@ -1728,17 +1745,14 @@ trait CodeExtraction extends ASTExtractors {
               StringConcat(converter(a1), a2)
             case (IsTyped(a1, StringType), "length", List()) =>
               StringLength(a1)
-            case (IsTyped(a1, StringType), "bigLength", List()) =>
-              StringBigLength(a1)
             case (IsTyped(a1, StringType), "substring", List(IsTyped(start, Int32Type))) =>
-              SubString(a1, start, StringLength(a1))
+              val s = FreshIdentifier("s", StringType)
+              let(s, a1,
+              SubString(Variable(s), start, StringLength(Variable(s)))
+              )
             case (IsTyped(a1, StringType), "substring", List(IsTyped(start, Int32Type), IsTyped(end, Int32Type))) =>
               SubString(a1, start, end)
-            case (IsTyped(a1, StringType), "bigSubstring", List(IsTyped(start, IntegerType))) =>
-              BigSubString(a1, start, StringBigLength(a1))
-            case (IsTyped(a1, StringType), "bigSubstring", List(IsTyped(start, IntegerType), IsTyped(end, IntegerType))) =>
-              BigSubString(a1, start, end)
-
+            
             //BigInt methods
             case (IsTyped(a1, IntegerType), "+", List(IsTyped(a2, IntegerType))) =>
               Plus(a1, a2)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index bda0e061258e8f542c21e0fe4f40e5df369984aa..b812bcf573bf5c9d8cbb3942c15b4f4056b15e5d 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -86,6 +86,12 @@ class PrettyPrinter(opts: PrinterOptions,
 
       case Variable(id) =>
         p"$id"
+        
+      case Let(id, expr, SubString(Variable(id2), start, StringLength(Variable(id3)))) if id == id2 && id2 == id3 =>
+        p"$expr.substring($start)"
+        
+      case Let(id, expr, BigSubString(Variable(id2), start, StringLength(Variable(id3)))) if id == id2 && id2 == id3 =>
+        p"$expr.bigSubstring($start)"
 
       case Let(b,d,e) =>
         p"""|val $b = $d