diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index 864f3ff285df43a9d49452c183b40b3874980f30..b9b5a2b7d6357773ac40e1418f142bebff1a092b 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -36,7 +36,7 @@ object LazyVerificationPhase {
       case fd if fd.postcondition.exists { exists(hasInstVar) } =>
         // remove the conjuncts that use instrumentation vars
         val Lambda(resdef, pbody) = fd.postcondition.get
-        val npost = pbody match {
+        val npost = simplifyByConstructors(pbody) match {
           case And(args) =>
             createAnd(args.filterNot(hasInstVar))
           case l: Let => // checks if the body of the let can be deconstructed as And