diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index cf0c53a79209a51a5f05155d92770ea3b8d96c6b..5037781d4c3db3505a58671bc80f9027ba048f81 100644
--- a/src/main/scala/leon/purescala/TransformerWithPC.scala
+++ b/src/main/scala/leon/purescala/TransformerWithPC.scala
@@ -63,6 +63,10 @@ abstract class TransformerWithPC extends Transformer {
         se
       }).copiedFrom(e)
 
+    case i @ Implies(lhs, rhs) =>
+      val rc = rec(lhs, path)
+      Implies(rc, rec(rhs, register(rc, path))).copiedFrom(i)
+
     case o @ UnaryOperator(e, builder) =>
       builder(rec(e, path)).copiedFrom(o)