diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c07693a8af093988ccaa6ef2bb89e8f24bd00a09..84f196618d8fc6b84af18c7dfd83c1ae578a1fa0 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1210,8 +1210,8 @@ object ExprOps {
     simplePreTransform(pre)(expr)
   }
 
-  def simplifyPaths(sf: SolverFactory[Solver]): Expr => Expr = {
-    new SimplifierWithPaths(sf).transform
+  def simplifyPaths(sf: SolverFactory[Solver], initC: List[Expr] = Nil): Expr => Expr = {
+    new SimplifierWithPaths(sf, initC).transform
   }
 
   trait Traverser[T] {
@@ -2047,13 +2047,13 @@ object ExprOps {
   }
 
 
-  /** Collects correctness conditions from within an expression
-    * (taking into account the path condition).
+  /** Collects from within an expression all conditions under which the evaluation of the expression
+    * will not fail (e.g. by violating a function precondition or evaluating to an error).
     *
-    * Collection of preconditions of function invocations
-    * can be disabled (mainly for [[leon.verification.Tactic]]).
+    * Collection of preconditions of function invocations can be disabled
+    * (mainly for [[leon.verification.Tactic]]).
     *
-    * @param e The expression to traverse
+    * @param e The expression for which correctness conditions are calculated.
     * @param collectFIs Whether we also want to collect preconditions for function invocations
     * @return A sequence of pairs (expression, condition)
     */
@@ -2086,6 +2086,59 @@ object ExprOps {
   }
 
 
+  def simpleCorrectnessCond(e: Expr, path: List[Expr], sf: SolverFactory[Solver]): Expr = {
+    simplifyPaths(sf, path)(
+      andJoin( collectCorrectnessConditions(e) map { _._2 } )
+    )
+  }
+
 
 
 }
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index 9e33ba1f64171b1e622ef9b83a90bb78132d73f4..dc4dfce46aba691026123801b24285a216637ac5 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -10,11 +10,9 @@ import Extractors._
 import Constructors._
 import solvers._
 
-class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
+class SimplifierWithPaths(sf: SolverFactory[Solver], override val initC: List[Expr] = Nil) extends TransformerWithPC {
   type C = List[Expr]
 
-  val initC = Nil
-
   val solver = SimpleSolverAPI(sf)
 
   protected def register(e: Expr, c: C) = e :: c
@@ -97,10 +95,10 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
             case SimpleCase(p, rhs) =>
               SimpleCase(p, rec(rhs, cond))
             case GuardedCase(p, g, rhs) =>
-              // FIXME: This is quite a dirty hack. We just know matchCasePathConditions 
+              // @mk: This is quite a dirty hack. We just know matchCasePathConditions
               // returns the current guard as the last element.
               // We don't include it in the path condition when we recurse into itself.
-              val condWithoutGuard = try { cond.init } catch { case _ : UnsupportedOperationException => List() }
+              val condWithoutGuard = cond.dropRight(1)
               val newGuard = rec(g, condWithoutGuard)
               if (valid(newGuard))
                 SimpleCase(p, rec(rhs,cond))
@@ -135,6 +133,9 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
         BooleanLiteral(true).copiedFrom(e)
       }
 
+    case a @ Assert(pred, _, body) if impliedBy(pred, path) =>
+      body.copiedFrom(a)
+
     case b if b.getType == BooleanType && impliedBy(b, path) =>
       BooleanLiteral(true).copiedFrom(b)
 
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 7e6c3e880e0ed2d608b4d7711abd40ddae1134ee..a53ff8672082d03873141e21c1f11141281095fd 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -26,10 +26,10 @@ object ConvertHoles extends TransformationPhase {
    *
    * def foo(a: T) {
    *   require(..a..)
-   *   val h = choose { (h) => {
-   *     val res = expr(a, ???)
+   *   val h = choose ( h' =>
+   *     val res = expr(a, h')
    *     post(res)
-   *   }
+   *   )
    *   expr(a, h)
    * } ensuring { res =>
    *   post(res)
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 77691739f6d57488d7dd13a43261976e3ca4df6d..98af8cde056833cc316829d8b4319269696769f7 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -5,7 +5,6 @@ package verification
 
 import purescala.Definitions._
 import purescala.Expressions._
-import purescala.ExprOps._
 
 abstract class Tactic(vctx: VerificationContext) {
   val description : String