diff --git a/src/main/scala/leon/invariant/structure/FunctionUtils.scala b/src/main/scala/leon/invariant/structure/FunctionUtils.scala
index 3d56016892223b5c30ce293857716c4decc53c70..eb36720b93b678724d8c8bf13a1d4d8b8d4dd720 100644
--- a/src/main/scala/leon/invariant/structure/FunctionUtils.scala
+++ b/src/main/scala/leon/invariant/structure/FunctionUtils.scala
@@ -110,7 +110,7 @@ object FunctionUtils {
       if (fd.postcondition.isDefined) {
         val Lambda(_, postBody) = fd.postcondition.get
         // collect all terms with question marks and convert them to a template
-        val postWoQmarks = postBody match {
+        val postWoQmarks = simplifyByConstructors(postBody) match {
           case And(args) if args.exists(exists(isQMark)) =>
             val (tempExprs, otherPreds) = args.partition(exists(isQMark))
             //println(s"Otherpreds: $otherPreds ${qmarksToTmplFunction(createAnd(tempExprs))}")
@@ -172,4 +172,4 @@ object FunctionUtils {
       info
     })
   }
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index b9b5a2b7d6357773ac40e1418f142bebff1a092b..14b84a116802d3ec938af03824b2eb9833a5a551 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -176,7 +176,7 @@ object LazyVerificationPhase {
   def collectAntsPostTmpl(fd: FunDef) = {
     val Lambda(Seq(resdef), _) = fd.postcondition.get
     val (pbody, tmpl) = (fd.getPostWoTemplate, fd.template)
-    val (instPost, assumptions) = pbody match {
+    val (instPost, assumptions) = simplifyByConstructors(pbody) match {
       case And(args) =>
         val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
         (createAnd(instSpecs), createAnd(rest))