diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index d098bedf979fe8156f171a76b9b220bf45882603..f6dfaa543c4ce31d508461e195a5bbea8958490d 100644
--- a/src/main/scala/leon/purescala/TransformerWithPC.scala
+++ b/src/main/scala/leon/purescala/TransformerWithPC.scala
@@ -33,10 +33,11 @@ abstract class TransformerWithPC extends Transformer {
         val patternExprPos = conditionForPattern(rs, c.pattern, includeBinders = true)
         val patternExprNeg = conditionForPattern(rs, c.pattern, includeBinders = false)
         val map = mapForPattern(rs, c.pattern)
-        val guard = replaceFromIDs(map, c.optGuard.getOrElse(BooleanLiteral(true)))
+        val guardOrTrue = c.optGuard.getOrElse(BooleanLiteral(true))
+        val guardMapped = replaceFromIDs(map, guardOrTrue)
 
-        val subPath = register(patternExprPos, soFar)
-        soFar = register(not(and(patternExprNeg, guard)), soFar)
+        val subPath = register(and(patternExprPos, guardOrTrue), soFar)
+        soFar = register(not(and(patternExprNeg, guardMapped)), soFar)
         
         MatchCase(c.pattern, c.optGuard, rec(c.rhs,subPath)).copiedFrom(c)
 
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index b6cb7611728e2cbb5f1c92ec4aab18a7c291add0..105c61d6150eaff90a417f0ae759bc40e92b40c8 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -11,7 +11,6 @@ abstract class Tactic(vctx: VerificationContext) {
   val description : String
 
   def generateVCs(fd: FunDef): Seq[VC] = {
-    fd.fullBody = matchToIfThenElse(fd.fullBody)
     generatePostconditions(fd) ++
     generatePreconditions(fd) ++
     generateCorrectnessConditions(fd)