diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 199fd866942e3700f08da56413330ee192714ee6..40f745a332bee265ffafc5de6336040fa9058e7e 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -904,7 +904,7 @@ trait CodeGeneration {
         mkExpr(a, ch)
         mkExpr(start, ch)
         mkExpr(end, ch)
-        ch << InvokeStatic(StrOpsClass, "bigSubstring", s"(L$JavaStringClass;II)L$JavaStringClass;")
+        ch << InvokeStatic(StrOpsClass, "bigSubstring", s"(L$JavaStringClass;L$BigIntClass;L$BigIntClass;)L$JavaStringClass;")
         
       // Arithmetic
       case Plus(l, r) =>
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 63afebf484e3c354693a39cb54e0be00e583ec34..ae2774a7e33e3da3b9563860880a395ee65a58bd 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1934,7 +1934,7 @@ object ExprOps extends GenTreeOps[Expr] {
 
   /** Returns the precondition of an expression wrapped in Option */
   def preconditionOf(expr: Expr): Option[Expr] = expr match {
-    case Let(i, e, b)                 => preconditionOf(b).map(Let(i, e, _))
+    case Let(i, e, b)                 => preconditionOf(b).map(Let(i, e, _).copiedFrom(expr))
     case Require(pre, _)              => Some(pre)
     case Ensuring(Require(pre, _), _) => Some(pre)
     case b                            => None
@@ -1942,7 +1942,7 @@ object ExprOps extends GenTreeOps[Expr] {
 
   /** Returns the postcondition of an expression wrapped in Option */
   def postconditionOf(expr: Expr): Option[Expr] = expr match {
-    case Let(i, e, b)      => postconditionOf(b).map(Let(i, e, _))
+    case Let(i, e, b)      => postconditionOf(b).map(Let(i, e, _).copiedFrom(expr))
     case Ensuring(_, post) => Some(post)
     case _                 => None
   }
diff --git a/src/main/scala/leon/purescala/GenTreeOps.scala b/src/main/scala/leon/purescala/GenTreeOps.scala
index a8ced270426bde209a0448e848e9cbe9f7a4280f..286b1ae23b93b5d392668568ae1e2ecf6f6c6b7b 100644
--- a/src/main/scala/leon/purescala/GenTreeOps.scala
+++ b/src/main/scala/leon/purescala/GenTreeOps.scala
@@ -415,6 +415,23 @@ trait GenTreeOps[SubTree <: Tree]  {
     fold[Int]{ (_, sub) => 1 + (0 +: sub).max }(e)
   }
 
+  /** Given a tree `toSearch` present in `treeToLookInto`, if `treeToLookInto` has the same shape as `treeToExtract`,
+   *  returns the matching expression in `treeToExtract``.*/
+  def lookup[T](checker: SubTree => Boolean, toExtract: SubTree => T)(treeToLookInto: SubTree, treeToExtract: SubTree): Option[T] = {
+    if(checker(treeToLookInto)) return Some(toExtract(treeToExtract))
+    
+    val Deconstructor(childrenToLookInto, _) = treeToLookInto
+    val Deconstructor(childrenToReturn, _) = treeToExtract
+    if(childrenToLookInto.size != childrenToReturn.size) return None
+    for((l, r) <- childrenToLookInto.zip(childrenToReturn)) {
+      lookup(checker, toExtract)(l, r) match {
+        case s@Some(n) => return s
+        case _ =>
+      }
+    }
+    return None
+  }
+
   object Same {
     def unapply(tt: (SubTree, SubTree)): Option[(SubTree, SubTree)] = {
       if (tt._1.getClass == tt._2.getClass) {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index bd1ef544856123a9a940179f432b6b235c404ab8..4e24f6c8e82c398336da6b1301afcfa5025e089d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -178,7 +178,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
     case StringConcat(a, b)        => Strings.Concat(toSMT(a), toSMT(b))
     case SubString(a, start, BVPlus(start2, length)) if start == start2  =>
                                       Strings.Substring(toSMT(a),toSMT(start),toSMT(length))
-    case SubString(a, start, end)  => Strings.Substring(toSMT(a),toSMT(start),toSMT(Minus(end, start)))
+    case SubString(a, start, end)  => Strings.Substring(toSMT(a),toSMT(start),toSMT(BVMinus(end, start)))
     case BigSubString(a, start, Plus(start2, length)) if start == start2  =>
                                       Strings.Substring(toSMT(a),toSMT(start),toSMT(length))
     case BigSubString(a, start, end)  => Strings.Substring(toSMT(a),toSMT(start),toSMT(Minus(end, start)))
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index d7850d079e88ce3d8cc37dc4338a817d42d4b40a..117380725d27e06afddfa577ed105186982a0216 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -6,6 +6,7 @@ import leon.purescala.Expressions._
 import leon.purescala.Definitions._
 import leon.purescala.Types._
 import leon.purescala.PrettyPrinter
+import leon.purescala.ExprOps
 import leon.utils.Positioned
 import leon.solvers._
 import leon.LeonContext
@@ -16,6 +17,16 @@ case class VC(condition: Expr, fd: FunDef, kind: VCKind) extends Positioned {
   override def toString = {
     fd.id.name +" - " +kind.toString
   }
+  // If the two functions are the same but have different positions, used to transfer one to the other.
+  def copyTo(newFun: FunDef) = {
+    val thisPos = this.getPos
+    val newPos = ExprOps.lookup(_.getPos == thisPos, _.getPos)(fd.fullBody, newFun.fullBody) match {
+      case Some(position) => position
+      case None => newFun.getPos
+    }
+    val newCondition = ExprOps.lookup(condition == _, i => i)(fd.fullBody, newFun.fullBody).getOrElse(condition)
+    VC(newCondition, newFun, kind).setPos(newPos)
+  }
 }
 
 abstract class VCKind(val name: String, val abbrv: String) {