diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
index 64e1db3f4..063d14c76 100644
--- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -750,7 +750,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
     } else {
       n.info.getUniqueInfo[AnnotationInfo] match {
         case Some(ai) if ai.values.nonEmpty =>
-          val docs = ai.values.map(v => char('@') <> v._1 <> parens(ssep(v._2.map(v => text(s"\"${v}\"")), text(", ")))).toSeq
+          val docs = ai.values.filter(v => v._1 != "expandedMacro").map(v => char('@') <> v._1 <> parens(ssep(v._2.map(v => text(s"\"${v}\"")), text(", ")))).toSeq
           Some(ssep(docs, if (breakLines) line else space))
         case _ => None
       }
diff --git a/src/main/scala/viper/silver/parser/MacroExpander.scala b/src/main/scala/viper/silver/parser/MacroExpander.scala
index 0a5bcfee9..e6a4e9182 100644
--- a/src/main/scala/viper/silver/parser/MacroExpander.scala
+++ b/src/main/scala/viper/silver/parser/MacroExpander.scala
@@ -338,8 +338,11 @@ object MacroExpander {
       var bodyWithReplacedParams = replacer.execute[PNode](bodyWithRenamedVars, context)
       bodyWithReplacedParams = adaptPositions(bodyWithReplacedParams, pos)
 
-      // Return expanded macro's body
-      bodyWithReplacedParams
+      // Return expanded macro's body wrapped inside annotation
+      bodyWithReplacedParams match {
+        case b: PExp => PAnnotatedExp(PAnnotation(new PSym.At(PSym.At)(pos),PRawString("expandedMacro")(pos),PGrouped.impliedParen(PDelimited.empty))(pos),b)(pos)
+        case b: PStmt => PAnnotatedStmt(PAnnotation(new PSym.At(PSym.At)(pos),PRawString("expandedMacro")(pos),PGrouped.impliedParen(PDelimited.empty))(pos),b)(pos)
+      }
     }
 
     def ExpandMacroIfValid(macroCall: PNode, ctx: ContextA[PNode]): PNode = {
diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index 4ee3f6d45..2027b6ede 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -207,7 +207,7 @@ trait PartialVerificationError {
   def withReasonNodeTransformed(t : errors.ErrorNode => errors.ErrorNode) = {
     PartialVerificationError(
       (r:ErrorReason) =>
-      f(r.withNode(t(r.offendingNode)).asInstanceOf[ErrorReason])
+        f(r.withNode(t(r.offendingNode)).asInstanceOf[ErrorReason])
     )
   }
 
@@ -429,6 +429,14 @@ object errors {
   def PostconditionViolated(offendingNode: Exp, member: Contracted): PartialVerificationError =
     PartialVerificationError((reason: ErrorReason) => PostconditionViolated(offendingNode, member, reason))
 
+  case class PostconditionViolatedBranch(offendingNode: Exp, reason: ErrorReason, leftIsFatal: Boolean, rightIsFatal: Boolean, override val cached: Boolean = false) extends AbstractVerificationError {
+    val id = "postcondition.violated.branch"
+    val text = s"Branch fails."
+
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = PostconditionViolatedBranch(offendingNode.asInstanceOf[Exp], this.reason, leftIsFatal, rightIsFatal, this.cached)
+    def withReason(r: ErrorReason) = PostconditionViolatedBranch(offendingNode, r, leftIsFatal, rightIsFatal, cached)
+  }
+
   case class FoldFailed(offendingNode: Fold, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
     val id = "fold.failed"
     val text = s"Folding ${offendingNode.acc.loc} might fail."
@@ -610,7 +618,7 @@ object reasons {
   }
 
   case class UnexpectedNode(offendingNode: ErrorNode, explanation: String, stackTrace: Seq[StackTraceElement])
-      extends AbstractErrorReason {
+    extends AbstractErrorReason {
 
     val id = "unexpected.node"
     def readableMessage = s"$offendingNode occurred unexpectedly. $explanation"
@@ -625,6 +633,13 @@ object reasons {
     def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = AssertionFalse(offendingNode.asInstanceOf[Exp])
   }
 
+  case class AssertionFalseAtBranch(offendingNode: Exp, treeString: String) extends AbstractErrorReason {
+    val id = "assertion.false.branch"
+    def readableMessage = "\n" + treeString
+
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = AssertionFalseAtBranch(offendingNode.asInstanceOf[Exp], treeString)
+  }
+
   // Note: this class should be deprecated/removed - we no longer support epsilon permissions in the language
   case class EpsilonAsParam(offendingNode: Exp) extends AbstractErrorReason {
     val id = "epsilon.as.param"