diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 0d206d9ae..68d179f4c 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -285,16 +285,18 @@ object AccessPredicate {
 }
 
 /** An accessibility predicate for a field location. */
-case class FieldAccessPredicate(loc: FieldAccess, perm: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+case class FieldAccessPredicate(loc: FieldAccess, permExp: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+  val perm = permExp.getOrElse(FullPerm()(pos, NoInfo, NoTrafos))
   override lazy val check : Seq[ConsistencyError] =
-    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq()) ++ Consistency.checkWildcardUsage(perm)
+    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq())
   val typ: Bool.type = Bool
 }
 
 /** An accessibility predicate for a predicate location. */
-case class PredicateAccessPredicate(loc: PredicateAccess, perm: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+case class PredicateAccessPredicate(loc: PredicateAccess, permExp: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+  val perm = permExp.getOrElse(FullPerm()(pos, NoInfo, NoTrafos))
   override lazy val check : Seq[ConsistencyError] =
-    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq()) ++ Consistency.checkWildcardUsage(perm)
+    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq())
   val typ: Bool.type = Bool
 }
 
@@ -499,6 +501,11 @@ case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition,
   lazy val typ = body.typ
 }
 
+case class Asserting(a: Exp, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
+  override lazy val check: Seq[ConsistencyError] = Consistency.checkPure(body)
+  lazy val typ = body.typ
+}
+
 // --- Old expressions
 
 sealed trait OldExp extends UnExp {
diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index 1ea501bef..3eb934129 100644
--- a/src/main/scala/viper/silver/ast/Program.scala
+++ b/src/main/scala/viper/silver/ast/Program.scala
@@ -361,7 +361,7 @@ case class Field(name: String, typ: Type)(val pos: Position = NoPosition, val in
 /** A predicate declaration. */
 case class Predicate(name: String, formalArgs: Seq[LocalVarDecl], body: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Location {
   override lazy val check : Seq[ConsistencyError] =
-    (if (body.isDefined) Consistency.checkNonPostContract(body.get) else Seq()) ++
+    (if (body.isDefined) Consistency.checkNonPostContract(body.get) ++ Consistency.checkWildcardUsage(body.get, false) else Seq()) ++
     (if (body.isDefined && !Consistency.noOld(body.get))
       Seq(ConsistencyError("Predicates must not contain old expressions.",body.get.pos))
      else Seq()) ++
@@ -426,7 +426,8 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
     body.fold(Seq.empty[ConsistencyError])(Consistency.checkNoArgsReassigned(formalArgs, _)) ++
     (if (!((formalArgs ++ formalReturns) forall (_.typ.isConcrete))) Seq(ConsistencyError("Formal args and returns must have concrete types.", pos)) else Seq()) ++
     (pres ++ posts).flatMap(Consistency.checkNoPermForpermExceptInhaleExhale) ++
-    checkReturnsNotUsedInPreconditions
+    checkReturnsNotUsedInPreconditions ++
+    (pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, false))
 
   lazy val checkReturnsNotUsedInPreconditions: Seq[ConsistencyError] = {
     val varsInPreconditions: Seq[LocalVar] = pres flatMap {_.deepCollect {case l: LocalVar => l}}
@@ -454,6 +455,7 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres
     posts.flatMap(p=>{ if(!Consistency.noOld(p))
       Seq(ConsistencyError("Function post-conditions must not have old expressions.", p.pos)) else Seq()}) ++
     (pres ++ posts).flatMap(Consistency.checkNoPermForpermExceptInhaleExhale) ++
+    (pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, true)) ++
     (if(!(body forall (_ isSubtype typ))) Seq(ConsistencyError("Type of function body must match function type.", pos)) else Seq() ) ++
     (posts flatMap (p => if (!Consistency.noPerm(p) || !Consistency.noForPerm(p)) Seq(ConsistencyError("perm and forperm expressions are not allowed in function postconditions", p.pos)) else Seq() )) ++
     pres.flatMap(Consistency.checkPre) ++
@@ -471,7 +473,8 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres
         }).execute[Node](pre)
       })
       errors
-    }
+    } ++
+    Consistency.warnAboutFunctionPermissionAmounts(this)
 
   val scopedDecls: Seq[Declaration] = formalArgs
   /**
diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
index 2003fd387..64e1db3f4 100644
--- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -771,6 +771,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
         group(parens(text("unfolding") <+> nest(defaultIndent, show(acc)) <+> "in" <> nest(defaultIndent, line <> show(exp))))
       case Applying(wand, exp) =>
         parens(text("applying") <+> nest(defaultIndent, show(wand)) <+> "in" <> nest(defaultIndent, line <> show(exp)))
+      case Asserting(ass, exp) =>
+        parens(text("asserting") <+> nest(defaultIndent, parens(show(ass))) <+> "in" <> nest(defaultIndent, line <> show(exp)))
       case Old(exp) =>
         text("old") <> parens(show(exp))
       case LabelledOld(exp,label) =>
diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala
index cb68e36c4..7e18f152c 100644
--- a/src/main/scala/viper/silver/ast/utility/Consistency.scala
+++ b/src/main/scala/viper/silver/ast/utility/Consistency.scala
@@ -15,6 +15,10 @@ import viper.silver.{FastMessage, FastMessaging}
 /** An utility object for consistency checking. */
 object Consistency {
   var messages: FastMessaging.Messages = Nil
+
+  // Set to enable legacy mode where permission amounts in function preconditions have their usual meaning instead
+  // of just just being treated as a kind of wildcard.
+  private var respectFunctionPrePermAmounts: Boolean = false
   def recordIfNot(suspect: Positioned, property: Boolean, message: String): Unit = {
     if (!property) {
       val pos = suspect.pos
@@ -23,6 +27,14 @@ object Consistency {
     }
   }
 
+  /** Use this method to enable consistency checks suitable for the legacy mode where permission amounts in function
+    * preconditions have their standard meaning, instead of always meaning a kind of wildcard.
+    * In other words, this should be set iff the command line flag "--respectFunctionPrePermAmounts" is set.
+    * */
+  def setFunctionPreconditionLegacyMode(enableLegacyMode: Boolean) = {
+    respectFunctionPrePermAmounts = enableLegacyMode
+  }
+
   def resetMessages(): Unit = { this.messages = Nil }
   @inline
   def recordIf(suspect: Positioned, property: Boolean, message: String): Unit =
@@ -184,6 +196,28 @@ object Consistency {
     (if(!noResult(e)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", e.pos)) else Seq())
   }
 
+  def warnAboutFunctionPermissionAmounts(f: Function): Seq[ConsistencyError] = {
+    if (respectFunctionPrePermAmounts)
+      return Seq()
+    def hasSpecificPermAmounts(e: Exp): Boolean = e match {
+      case CondExp(_, thn, els) => hasSpecificPermAmounts(thn) || hasSpecificPermAmounts(els)
+      case _: FractionalPerm => true
+      case _: FullPerm => true
+      case _: PermAdd | _: PermSub | _: PermMinus | _: PermMul | _: IntPermMul | _: PermDiv | _: PermPermDiv => true
+      case _ => false
+    }
+    def collectWarnings(e: Exp): Seq[ConsistencyError] = e.collect{
+      case FieldAccessPredicate(_, Some(perm)) if hasSpecificPermAmounts(perm) =>
+        ConsistencyError("Function contains specific permission amount that will be treated like wildcard.", perm.pos, false)
+      case PredicateAccessPredicate(_, Some(perm)) if hasSpecificPermAmounts(perm) =>
+        ConsistencyError("Function contains specific permission amount that will be treated like wildcard.", perm.pos, false)
+    }.toSeq
+
+    val preWarnings = f.pres.flatMap(collectWarnings)
+    val bodyWarnings = f.body.toSeq.flatMap(collectWarnings)
+    preWarnings ++ bodyWarnings
+  }
+
   /** Check all properties required for a contract expression that is not a postcondition (precondition, invariant, predicate) */
   def checkNonPostContract(e: Exp) : Seq[ConsistencyError]  = {
     (if(!(e isSubtype Bool)) Seq(ConsistencyError(s"Contract $e: ${e.typ} must be boolean.", e.pos)) else Seq()) ++
@@ -196,18 +230,28 @@ object Consistency {
     (if(!noLabelledOld(e)) Seq(ConsistencyError("Labelled-old expressions are not allowed in postconditions.", e.pos)) else Seq())
   }
 
-  def checkWildcardUsage(e: Exp): Seq[ConsistencyError] = {
-    val containedWildcards = e.shallowCollect{
-      case w: WildcardPerm => w
-    }
-    if (containedWildcards.nonEmpty) {
-      e match {
-        case _: WildcardPerm => Seq()
-        case _ => Seq(ConsistencyError("Wildcard occurs inside compound expression (should only occur directly in an accessibility predicate).", e.pos))
+  def checkWildcardUsage(n: Node, inFunction: Boolean): Seq[ConsistencyError] = {
+    if (!respectFunctionPrePermAmounts && inFunction)
+      return Seq()
+
+    def checkValidUse(e: Exp): Seq[ConsistencyError] = {
+      val containedWildcards = e.shallowCollect {
+        case w: WildcardPerm => w
+      }
+      if (containedWildcards.nonEmpty) {
+        e match {
+          case _: WildcardPerm => Seq()
+          case _ => Seq(ConsistencyError("Wildcard occurs inside compound expression (should only occur directly in an accessibility predicate).", e.pos))
+        }
+      } else {
+        Seq()
       }
-    } else {
-      Seq()
     }
+
+    n.collect{
+      case FieldAccessPredicate(_, Some(prm)) => checkValidUse(prm)
+      case PredicateAccessPredicate(_, Some(prm)) => checkValidUse(prm)
+    }.flatten.toSeq
   }
 
   /** checks that all quantified variables appear in all triggers */
diff --git a/src/main/scala/viper/silver/ast/utility/Expressions.scala b/src/main/scala/viper/silver/ast/utility/Expressions.scala
index b4fa7c980..736074da9 100644
--- a/src/main/scala/viper/silver/ast/utility/Expressions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Expressions.scala
@@ -25,6 +25,7 @@ object Expressions {
     case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
     case unf: Unfolding => isPure(unf.body)
     case app: Applying => isPure(app.body)
+    case Asserting(a, e) => isPure(e)
     case QuantifiedExp(_, e0) => isPure(e0)
     case Let(_, _, body) => isPure(body)
     case e: ExtensionExp => e.extensionIsPure
@@ -96,9 +97,10 @@ object Expressions {
   def asBooleanExp(e: Exp): Exp = {
     e.transform({
       case _: AccessPredicate | _: MagicWand => TrueLit()()
-      case fa@Forall(vs,ts,body) => Forall(vs,ts,asBooleanExp(body))(fa.pos,fa.info)
+      case fa@Forall(vs,ts,body) => Forall(vs, ts, asBooleanExp(body))(fa.pos, fa.info, fa.errT)
       case Unfolding(_, exp) => asBooleanExp(exp)
       case Applying(_, exp) => asBooleanExp(exp)
+      case ass@Asserting(a, exp) => Asserting(asBooleanExp(a), asBooleanExp(exp))(ass.pos, ass.info, ass.errT)
     })
   }
 
@@ -191,7 +193,7 @@ object Expressions {
         }
         // Conditions for the current node.
         val conds: Seq[Exp] = n match {
-          case f@FieldAccess(rcv, _) => List(NeCmp(rcv, NullLit()(p))(p), FieldAccessPredicate(f, WildcardPerm()(p))(p))
+          case f@FieldAccess(rcv, _) => List(NeCmp(rcv, NullLit()(p))(p), FieldAccessPredicate(f, Some(WildcardPerm()(p)))(p))
           case f: FuncApp => prog.findFunction(f.funcname).pres
           case Div(_, q) => List(NeCmp(q, IntLit(0)(p))(p))
           case Mod(_, q) => List(NeCmp(q, IntLit(0)(p))(p))
@@ -199,6 +201,7 @@ object Expressions {
           case MapLookup(m, k) => List(MapContains(k, m)(p))
           case Unfolding(pred, _) => List(pred)
           case Applying(wand, _) => List(wand)
+          case Asserting(a, _) => List(a)
           case _ => Nil
         }
         // Only use non-trivial conditions for the subnodes.
diff --git a/src/main/scala/viper/silver/ast/utility/InverseFunctions.scala b/src/main/scala/viper/silver/ast/utility/InverseFunctions.scala
index e8ebe3e36..b778f8464 100644
--- a/src/main/scala/viper/silver/ast/utility/InverseFunctions.scala
+++ b/src/main/scala/viper/silver/ast/utility/InverseFunctions.scala
@@ -37,11 +37,11 @@ object InverseFunctions {
             val axiom1 = Forall(qvars, forall.triggers, Implies(cond, equalities)(pos, info, errT))(pos, info, errT)
             var condReplaced = cond
             var rcvReplaced = fap.loc.rcv
-            var permReplaced = fap.perm
+            var permReplaced = fap.permExp
             for (i <- 0 until qvars.length){
               condReplaced = condReplaced.replace(qvars(i).localVar, invsOfR(i))
               rcvReplaced = rcvReplaced.replace(qvars(i).localVar, invsOfR(i))
-              permReplaced = permReplaced.replace(qvars(i).localVar, invsOfR(i))
+              permReplaced = permReplaced.map(_.replace(qvars(i).localVar, invsOfR(i)))
             }
             val axiom2 = Forall(Seq(r), Seq(Trigger(invsOfR)(pos, info, errT)), Implies(condReplaced, EqCmp(rcvReplaced, r.localVar)(pos, info, errT))(pos, info, errT))(pos, info, errT)
             val acc1 = FieldAccessPredicate(FieldAccess(r.localVar, fap.loc.field)(), permReplaced)()
@@ -65,7 +65,7 @@ object InverseFunctions {
             val axiom2 = Forall(formalArgs, Seq(Trigger(invsOfFormalArgs)(pos, info, errT)), Implies(cond.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap), invArgsConj)(pos, info, errT))(pos, info, errT)
 
             val cond1 = cond.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap)
-            val acc1 = PredicateAccessPredicate(PredicateAccess(formalArgs map (_.localVar), pred.name)(pos, info, errT), pap.perm.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap))(pos, info, errT)
+            val acc1 = PredicateAccessPredicate(PredicateAccess(formalArgs map (_.localVar), pred.name)(pos, info, errT), pap.permExp.map(_.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap)))(pos, info, errT)
             val forall1 = Forall(formalArgs, Seq(Trigger(invsOfFormalArgs)(pos, info, errT)), Implies(cond1, acc1)(pos, info, errT))(pos, info, errT)
 
             val domain = Domain(domName, invs, Seq())(pos, info, errT)
diff --git a/src/main/scala/viper/silver/ast/utility/Nodes.scala b/src/main/scala/viper/silver/ast/utility/Nodes.scala
index 0dc99d7dd..4384d22bd 100644
--- a/src/main/scala/viper/silver/ast/utility/Nodes.scala
+++ b/src/main/scala/viper/silver/ast/utility/Nodes.scala
@@ -80,9 +80,10 @@ object Nodes {
           case _: AbstractLocalVar => Nil
           case FieldAccess(rcv, _) => Seq(rcv)
           case PredicateAccess(params, _) => params
-          case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc, perm)
+          case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc) ++ perm.toSeq
           case Unfolding(acc, body) => Seq(acc, body)
           case Applying(wand, body) => Seq(wand, body)
+          case Asserting(ass, body) => Seq(ass, body)
           case Old(exp) => Seq(exp)
           case CondExp(cond, thn, els) => Seq(cond, thn, els)
           case Let(v, exp, body) => Seq(v, exp, body)
diff --git a/src/main/scala/viper/silver/ast/utility/Permissions.scala b/src/main/scala/viper/silver/ast/utility/Permissions.scala
index 858756002..bf4caee5a 100644
--- a/src/main/scala/viper/silver/ast/utility/Permissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Permissions.scala
@@ -31,12 +31,21 @@ object Permissions {
            "Internal error: attempted to permission-scale expression " + e.toString +
                " by non-permission-typed expression " + permFactor.toString)
 
-    if(permFactor.isInstanceOf[FullPerm])
+    def multiplyPermOpt(op: Option[Exp]): Option[Exp] = op match {
+      case Some(p) => Some(PermMul(p, permFactor)(p.pos, p.info))
+      case None => Some(permFactor)
+    }
+
+    if (permFactor.isInstanceOf[FullPerm]) {
       e
-    else
-      e.transform({
-        case fa@FieldAccessPredicate(loc,p) => FieldAccessPredicate(loc,PermMul(p,permFactor)(p.pos,p.info))(fa.pos,fa.info)
-        case pa@PredicateAccessPredicate(loc,p) => PredicateAccessPredicate(loc,PermMul(p,permFactor)(p.pos,p.info))(pa.pos,pa.info)
+    } else {
+      e.transform{
+        case fa@FieldAccessPredicate(loc, p) =>
+          FieldAccessPredicate(loc, multiplyPermOpt(p))(fa.pos, fa.info)
+        case pa@PredicateAccessPredicate(loc, p) =>
+          PredicateAccessPredicate(loc, multiplyPermOpt(p))(pa.pos, pa.info)
         case _: MagicWand => sys.error("Cannot yet permission-scale magic wands")
-      })}
+      }
+    }
+  }
 }
diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
index 69820bc6c..3462335e6 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
@@ -139,6 +139,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = false
   )
 
+  val respectFunctionPrePermAmounts = opt[Boolean]("respectFunctionPrePermAmounts",
+    descr = "Respects precise permission amounts in function preconditions instead of only checking read access.",
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
   val submitForEvaluation = opt[Boolean](name = "submitForEvaluation",
     descr = "Whether to allow storing the current program for future evaluation.",
     default = Some(false),
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index caf49316f..486b27282 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -374,12 +374,18 @@ trait SilFrontend extends DefaultFrontend {
   }
 
   def doConsistencyCheck(input: Program): Result[Program] = {
+    if (config != null) {
+      Consistency.setFunctionPreconditionLegacyMode(config.respectFunctionPrePermAmounts())
+    }
     var errors = input.checkTransitively
     if (backendTypeFormat.isDefined)
       errors = errors ++ Consistency.checkBackendTypes(input, backendTypeFormat.get)
-    if (errors.isEmpty) {
+    val (actualErrors, warnings) = errors partition (_.isError)
+    if (warnings.nonEmpty)
+      reporter.report(ConsistencyWarnings(warnings))
+    if (actualErrors.isEmpty) {
       Succ(input)
     } else
-      Fail(errors)
+      Fail(actualErrors)
   }
 }
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index dfc503ef5..eae845045 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -152,7 +152,7 @@ object FastParserCompanion {
     // maps
     PKw.Map, PKwOp.Range, PKwOp.Domain,
     // prover hint expressions
-    PKwOp.Unfolding, PKwOp.In, PKwOp.Applying,
+    PKwOp.Unfolding, PKwOp.In, PKwOp.Applying, PKwOp.Asserting,
     // old expression
     PKwOp.Old, PKw.Lhs,
     // other expressions
@@ -365,7 +365,7 @@ class FastParser {
   def atomReservedKw[$: P]: P[PExp] = {
     reservedKwMany(
       StringIn("true", "false", "null", "old", "result", "acc", "none", "wildcard", "write", "epsilon", "perm", "let", "forall", "exists", "forperm",
-        "unfolding", "applying", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
+        "unfolding", "applying", "asserting", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
       str => pos => str match {
         case "true" => Pass.map(_ => PBoolLit(PReserved(PKw.True)(pos))(_))
         case "false" => Pass.map(_ => PBoolLit(PReserved(PKw.False)(pos))(_))
@@ -384,6 +384,7 @@ class FastParser {
         case "forperm" => forperm.map(_(PReserved(PKw.Forperm)(pos)))
         case "unfolding" => unfolding.map(_(PReserved(PKwOp.Unfolding)(pos)))
         case "applying" => applying.map(_(PReserved(PKwOp.Applying)(pos)))
+        case "asserting" => asserting.map(_(PReserved(PKwOp.Asserting)(pos)))
         case "Set" => setConstructor.map(_(PReserved(PKwOp.Set)(pos)))
         case "Seq" => seqConstructor.map(_(PReserved(PKwOp.Seq)(pos)))
         case "Multiset" => multisetConstructor.map(_(PReserved(PKwOp.Multiset)(pos)))
@@ -652,6 +653,10 @@ class FastParser {
       PApplying(_, wand.inner, op, b)
   }
 
+  def asserting[$: P]: P[PKwOp.Asserting => Pos => PExp] = P(exp.parens ~ PKwOp.In ~ exp).map {
+    case (a, in, b) => PAsserting(_, a.inner, in, b)
+  }
+
   def predicateAccessAssertion[$: P]: P[PAccAssertion] = P(accessPred | predAcc)
 
   def setConstructor[$: P]: P[PKwOp.Set => Pos => PExp] =
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 4e59f54c4..9f2134825 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1080,6 +1080,12 @@ case class PApplying(applying: PKwOp.Applying, wand: PExp, in: PKwOp.In, exp: PE
     List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
 }
 
+case class PAsserting(asserting: PKwOp.Asserting, a: PExp, in: PKwOp.In, exp: PExp)(val pos: (Position, Position)) extends PHeapOpApp {
+  override val args = Seq(a, exp)
+  override val signatures: List[PTypeSubstitution] =
+    List(Map(POpApp.pArgS(0) -> Impure, POpApp.pResS -> POpApp.pArg(1)))
+}
+
 sealed trait PBinder extends PExp with PScope {
   def boundVars: Seq[PLogicalVarDecl]
 
@@ -1198,7 +1204,8 @@ case class PAccPred(op: PKwOp.Acc, amount: PGrouped.Paren[PMaybePairArgument[PLo
     Map(POpApp.pArgS(1) -> Perm, POpApp.pResS -> Impure),
   )
   def loc = amount.inner.first
-  def perm = amount.inner.second.map(_._2).getOrElse(PFullPerm.implied())
+  def perm = permExp.getOrElse(PFullPerm.implied())
+  def permExp: Option[PExp] = amount.inner.second.map(_._2)
   override val args = Seq(loc, perm)
 }
 
diff --git a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
index 646c14819..daed9a67f 100644
--- a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
+++ b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
@@ -494,6 +494,8 @@ object PKwOp {
   type Unfolding = PReserved[Unfolding.type]
   case object Applying    extends PKwOp("applying")                 with PKeywordAtom with RightSpace
   type Applying = PReserved[Applying.type]
+  case object Asserting   extends PKwOp("asserting")                with PKeywordAtom with RightSpace
+  type Asserting = PReserved[Asserting.type]
   case object Let         extends PKwOp("let")                      with PKeywordAtom with RightSpace
   type Let = PReserved[Let.type]
 
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 4a6f469d2..c03893c06 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -307,7 +307,7 @@ case class Translator(program: PProgram) {
         // A PrediateAccessPredicate is a PredicateResourceAccess combined with
         // a Permission. Havoc expects a ResourceAccess. To make types match,
         // we must extract the PredicateResourceAccess.
-        assert(perm.isInstanceOf[FullPerm])
+        assert(perm.isEmpty || perm.get.isInstanceOf[FullPerm])
         (newLhs, predAccess)
       case exp: MagicWand => (newLhs, exp)
       case _ => sys.error("Can't havoc this kind of expression")
@@ -504,8 +504,7 @@ case class Translator(program: PProgram) {
             }
           case _: Predicate =>
             val inner = PredicateAccess(args.inner.toSeq map exp, findPredicate(func).name) (pos, info)
-            val fullPerm = FullPerm()(pos, info)
-            PredicateAccessPredicate(inner, fullPerm) (pos, info)
+            PredicateAccessPredicate(inner, None) (pos, info)
           case _ => sys.error("unexpected reference to non-function")
         }
       case PNewExp(_, _) => sys.error("unexpected `new` expression")
@@ -513,6 +512,8 @@ case class Translator(program: PProgram) {
         Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos, info)
       case PApplying(_, wand, _, e) =>
         Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos, info)
+      case PAsserting(_, a, _, e) =>
+        Asserting(exp(a), exp(e))(pos, info)
       case pl@PLet(_, _, _, exp1, _, PLetNestedScope(body)) =>
         Let(liftLogicalDecl(pl.decl), exp(exp1.inner), exp(body))(pos, info)
       case _: PLetNestedScope =>
@@ -568,7 +569,7 @@ case class Translator(program: PProgram) {
       case PEpsilon(_) =>
         EpsilonPerm()(pos, info)
       case acc: PAccPred =>
-        val p = exp(acc.perm)
+        val p = acc.permExp.map(exp)
         exp(acc.loc) match {
           case loc@FieldAccess(_, _) =>
             FieldAccessPredicate(loc, p)(pos, info)
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
index b8816e3b0..450f72ff5 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
@@ -68,7 +68,7 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
             Function(piFunctionName,
               pred.formalArgs,
               DomainType(PredicateInstanceDomain.get, Map()),
-              Seq(PredicateAccessPredicate(PredicateAccess(pred.formalArgs.map(_.localVar), pred.name)(), WildcardPerm()())(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)),
+              Seq(PredicateAccessPredicate(PredicateAccess(pred.formalArgs.map(_.localVar), pred.name)(), Some(WildcardPerm()()))(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)),
               Seq(),
               None
             )(PredicateInstanceDomain.get.pos, PredicateInstanceDomain.get.info)
diff --git a/src/main/scala/viper/silver/reporter/Message.scala b/src/main/scala/viper/silver/reporter/Message.scala
index 441810eee..d4479eef2 100644
--- a/src/main/scala/viper/silver/reporter/Message.scala
+++ b/src/main/scala/viper/silver/reporter/Message.scala
@@ -269,6 +269,11 @@ case class WarningsDuringTypechecking(warnings: Seq[TypecheckerWarning]) extends
   override val name: String = "warnings_during_typechecking"
 }
 
+case class ConsistencyWarnings(warnings: Seq[ConsistencyError]) extends Message {
+  override lazy val toString: String = s"consistency_warnings(warnings=${warnings.toString})"
+  override val name: String = "consistency_warnings"
+}
+
 case class WarningsDuringVerification(warnings: Seq[VerifierWarning]) extends Message {
   override lazy val toString: String = s"warnings_during_verification(warnings=${warnings.toString})"
   override val name: String = "warnings_during_verification"
diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala
index 0c51bd50d..8f013e178 100644
--- a/src/main/scala/viper/silver/reporter/Reporter.scala
+++ b/src/main/scala/viper/silver/reporter/Reporter.scala
@@ -56,6 +56,10 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
         warnings.foreach(report => {
           csv_file.write(s"WarningsDuringVerification,${report}\n")
         })
+      case ConsistencyWarnings(warnings) =>
+        warnings.foreach(report => {
+          csv_file.write(s"ConsistencyWarnings,${report}\n")
+        })
       case InvalidArgumentsReport(_, errors) =>
         errors.foreach(error => {
           csv_file.write(s"WarningsDuringParsing,${error}\n")
@@ -150,6 +154,9 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
       case WarningsDuringVerification(warnings) =>
         warnings.foreach(println)
 
+      case ConsistencyWarnings(warnings) =>
+        warnings.foreach(println)
+
       case AnnotationWarning(text) =>
         println(s"Annotation warning: ${text}")
 
diff --git a/src/main/scala/viper/silver/testing/BackendTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
index 0f973825d..3b070fe09 100644
--- a/src/main/scala/viper/silver/testing/BackendTypeTest.scala
+++ b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
@@ -33,7 +33,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val p2_decl = LocalVarDecl("lol", SetType(t))()
     val p2_ref= p2_decl.localVar
     val fieldAcc = FieldAccess(p1_ref, field)()
-    val perm = FieldAccessPredicate(fieldAcc, FullPerm()())()
+    val perm = FieldAccessPredicate(fieldAcc, Some(FullPerm()()))()
     val element_in_param = AnySetContains(fieldAcc, p2_ref)()
 
     val getPerm = Inhale(perm)()
@@ -51,7 +51,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val setParam = LocalVarDecl("refs", SetType(Ref))()
     val floatParam = LocalVarDecl("val", fp.typ)()
     val x = LocalVarDecl("x", Ref)()
-    val qpBody = Implies(AnySetContains(x.localVar, setParam.localVar)(), FieldAccessPredicate(FieldAccess(x.localVar, fld)(), FullPerm()())())()
+    val qpBody = Implies(AnySetContains(x.localVar, setParam.localVar)(), FieldAccessPredicate(FieldAccess(x.localVar, fld)(), None)())()
     val qp = Forall(Seq(x), Seq(), qpBody)()
     val inhaleQp = Inhale(qp)()
     val fieldInfoBody = Implies(AnySetContains(x.localVar, setParam.localVar)(), NeCmp(FieldAccess(x.localVar, fld)(), floatParam.localVar)())()
@@ -151,14 +151,14 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val field = Field("val_float", fp.typ)()
     val selfVar = LocalVarDecl("self", Ref)()
     val fieldAcc = FieldAccess(selfVar.localVar, field)()
-    val fieldAccPred = FieldAccessPredicate(fieldAcc, FullPerm()())()
+    val fieldAccPred = FieldAccessPredicate(fieldAcc, Some(FullPerm()()))()
     val pred = Predicate("f64", Seq(selfVar), Some(fieldAccPred))()
 
     val inhale = Inhale(fieldAccPred)()
     val fpVal = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(value)()))()))()
     val assign = FieldAssign(fieldAcc, fpVal)()
     val predAcc = PredicateAccess(Seq(selfVar.localVar), pred.name)()
-    val predAccPred = PredicateAccessPredicate(predAcc, FullPerm()())()
+    val predAccPred = PredicateAccessPredicate(predAcc, None)()
     val fold = Fold(predAccPred)()
     val exhale = Exhale(predAccPred)()
 
diff --git a/src/main/scala/viper/silver/verifier/VerificationResult.scala b/src/main/scala/viper/silver/verifier/VerificationResult.scala
index 95980f6c5..8631b8690 100644
--- a/src/main/scala/viper/silver/verifier/VerificationResult.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationResult.scala
@@ -106,9 +106,9 @@ case class VerifierWarning(message: String, override val pos: Position)
 }
 
 /** An error during consistency-checking an AST node */
-case class ConsistencyError(message: String, pos:Position) extends AbstractError {
+case class ConsistencyError(message: String, pos:Position, isError: Boolean = true) extends AbstractError {
   def fullId = "consistency.error"
-  def readableMessage: String = s"Consistency error: $message ($pos)"
+  def readableMessage: String = s"Consistency ${if (isError) "error" else "warning"}: $message ($pos)"
 }
 
 /** A typechecker error. */
diff --git a/src/test/resources/all/asserting/function.vpr b/src/test/resources/all/asserting/function.vpr
new file mode 100644
index 000000000..144a7e4ab
--- /dev/null
+++ b/src/test/resources/all/asserting/function.vpr
@@ -0,0 +1,38 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function fplusone(x: Ref, y: Ref): Int
+    requires acc(x.f)
+{
+  asserting (x != null) in (x.f + 1)
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fplusone2(x: Ref, y: Ref): Int
+    requires acc(x.f)
+{
+  asserting (x != y) in (x.f + 1)
+}
+
+method main()
+{
+  var x: Ref
+  x := new(f)
+
+  var hmm: Int
+  hmm := fplusone(x, x)
+  hmm := asserting (hmm == x.f + 1) in hmm
+}
+
+method main2()
+{
+  var x: Ref
+  x := new(f)
+
+  var hmm: Int
+  hmm := fplusone(x, x)
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  hmm := asserting (hmm == x.f) in hmm
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/other-fail.vpr b/src/test/resources/all/asserting/other-fail.vpr
new file mode 100644
index 000000000..465a83c9e
--- /dev/null
+++ b/src/test/resources/all/asserting/other-fail.vpr
@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field x: Int
+
+method test1() {
+  //:: ExpectedOutput(assert.failed:division.by.zero)
+  assert asserting (1 / 0 == 0) in true
+}
+
+method test2() {
+  //:: ExpectedOutput(assert.failed:division.by.zero)
+  assert asserting (true) in (1 / 0 == 0)
+}
+
+method test3(r: Ref) {
+  //:: ExpectedOutput(assert.failed:insufficient.permission)
+  assert asserting (true && acc(r.x)) in true
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/qp.vpr b/src/test/resources/all/asserting/qp.vpr
new file mode 100644
index 000000000..474714a95
--- /dev/null
+++ b/src/test/resources/all/asserting/qp.vpr
@@ -0,0 +1,44 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method m1(s: Set[Ref])
+  requires |s| > 0
+{
+  inhale forall x: Ref :: x in (asserting(|s| > 0) in s) ==> acc(x.f)
+}
+
+method m1Fail(s: Set[Ref])
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in (asserting(|s| > 0) in s) ==> acc(x.f)
+}
+
+method m2(s: Set[Ref])
+  requires |s| > 0
+  requires !(null in s)
+{
+  inhale forall x: Ref :: x in s ==> acc((asserting (x != null) in x).f)
+}
+
+method m2Fail(s: Set[Ref])
+  requires |s| > 0
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in s ==> acc((asserting (x != null) in x).f)
+}
+
+method m3(s: Set[Ref])
+  requires |s| > 0
+  requires !(null in s)
+{
+  inhale forall x: Ref :: x in s ==> acc(x.f, asserting (x != null) in write)
+}
+
+method m3Fail(s: Set[Ref])
+  requires |s| > 0
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in s ==> acc(x.f, asserting (x != null) in write)
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/simple-fail.vpr b/src/test/resources/all/asserting/simple-fail.vpr
new file mode 100644
index 000000000..5c5791f5d
--- /dev/null
+++ b/src/test/resources/all/asserting/simple-fail.vpr
@@ -0,0 +1,73 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method assign() {
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (false) in 0
+}
+
+method assign2(i: Int) {
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (i > 0) in 0
+}
+
+method assign3(i: Int)
+  requires i > 5
+{
+  var x: Int := asserting (i > 0) in 0
+}
+
+method pres()
+  //:: ExpectedOutput(not.wellformed:assertion.false)
+  requires asserting (false) in false
+{
+  assert false
+}
+
+method pres2(x: Ref)
+  //:: ExpectedOutput(not.wellformed:insufficient.permission)
+  requires asserting (acc(x.f)) in false
+{
+  assert false
+}
+
+method pres3(x: Ref)
+  requires acc(x.f)
+  requires asserting (acc(x.f)) in false
+{
+  assert false
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun(): Int
+{
+  asserting (false) in 0
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function fun2(x: Ref): Int
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun3(x: Ref): Int
+  requires acc(x.f)
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+function fun4(x: Ref): Int
+  requires acc(x.f) && x.f > 8
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+method stateUnchanged(x: Ref)
+  requires acc(x.f)
+{
+  var y: Int := asserting (acc(x.f)) in x.f
+  assert acc(x.f)
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/trigger.vpr b/src/test/resources/all/asserting/trigger.vpr
new file mode 100644
index 000000000..f27f14fab
--- /dev/null
+++ b/src/test/resources/all/asserting/trigger.vpr
@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function trigger(i: Int): Bool
+{
+  true
+}
+
+method triggerUse(s: Seq[Int])
+  requires |s| > 0
+  requires forall i: Int :: {trigger(i)} 0 <= i < |s| ==> s[i] > 0
+{
+  assert asserting (trigger(0)) in s[0] > 0
+}
+
+method triggerUse2(s: Seq[Int])
+  requires |s| > 0
+  requires forall i: Int :: {trigger(i)} 0 <= i < |s| ==> s[i] > 0
+{
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert s[0] > 0
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/wand.vpr b/src/test/resources/all/asserting/wand.vpr
new file mode 100644
index 000000000..67a026f8e
--- /dev/null
+++ b/src/test/resources/all/asserting/wand.vpr
@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+field g: Int
+
+method test0(x: Ref)
+{
+    package acc(x.f) && (asserting (acc(x.f)) in (x.f == 0)) --* acc(x.f) {}
+}
+
+method test1(x: Ref)
+{
+    //:: ExpectedOutput(package.failed:insufficient.permission)
+    package acc(x.f) && (asserting (acc(x.g)) in (x.f == 0)) --* acc(x.f) {}
+}
+
diff --git a/src/test/resources/all/functions/function_precondition_perms.vpr b/src/test/resources/all/functions/function_precondition_perms.vpr
new file mode 100644
index 000000000..d9e5dc8c1
--- /dev/null
+++ b/src/test/resources/all/functions/function_precondition_perms.vpr
@@ -0,0 +1,444 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+field g: Int
+
+predicate P(x: Ref) {
+    acc(x.f)
+}
+
+function foo(x: Ref): Int
+  requires acc(x.f)
+
+function foop(x: Ref): Int
+  requires P(x)
+
+function foo2(x: Ref, b: Bool): Int
+  requires acc(x.f, b ? write : none)
+
+function foo2w(x: Ref, b: Bool): Int
+  requires acc(x.f, b ? wildcard : none)
+
+function foo3(x: Ref): Int
+  requires acc(x.f, wildcard)
+
+function foo4(x: Ref): Int
+  requires acc(x.f) && acc(x.f)
+
+function foo5(x: Ref): Int
+  requires forall z: Ref :: z == x ==> acc(z.f)
+
+function foo5w(x: Ref): Int
+  requires forall z: Ref :: z == x ==> acc(z.f, wildcard)
+
+function foo5p(x: Ref): Int
+  requires forall z: Ref :: z == x ==> P(z)
+
+function foo5pw(x: Ref): Int
+  requires forall z: Ref :: z == x ==> acc(P(z), wildcard)
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function nonAliasF(x: Ref, y: Ref): Int
+  requires acc(x.f) && acc(y.f)
+{
+    asserting (x != y) in x.f
+}
+
+predicate nonAliasPred(x: Ref, y: Ref) {
+    acc(x.f) && acc(y.f) && asserting (x != y) in true
+}
+
+method nonAliasM(x: Ref, y: Ref) {
+    inhale acc(x.f) && acc(y.f)
+    assert x != y
+}
+
+function bar(x: Ref): Int
+  requires acc(P(x), 1/4)
+{
+  unfolding acc(P(x), 1/2) in foo(x)
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function bar2(x: Ref): Int
+  requires acc(P(x), none)
+{
+  unfolding acc(P(x), 1/2) in foo(x)
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function bar3(x: Ref): Int
+  requires acc(P(x), write)
+{
+  unfolding acc(P(x), 1/2) in x.g
+}
+
+function bar4(x: Ref): Int
+  requires acc(P(x), 1/2) && unfolding P(x) in x.f > 0
+
+
+function bar5(x: Ref): Int
+  //:: ExpectedOutput(not.wellformed:insufficient.permission)
+  requires unfolding P(x) in x.f > 0
+
+function foo6(x: Ref): Int
+  requires forall z: Ref :: false ==> acc(z.f)
+  requires acc(x.f)
+
+method test0(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo(x)
+}
+
+@exhaleMode("mce")
+method test0mce(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo(x)
+}
+
+method test0qp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, 1/2)
+   var tmp: Int
+   tmp := foo(x)
+}
+
+method test0p(x: Ref)
+{
+   inhale acc(P(x), 1/2)
+   var tmp: Int
+   tmp := foop(x)
+}
+
+@exhaleMode("mce")
+method test0pmce(x: Ref)
+{
+   inhale acc(P(x), 1/2)
+   var tmp: Int
+   tmp := foop(x)
+}
+
+method test0pqp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(P(y), 1/2)
+   var tmp: Int
+   tmp := foop(x)
+}
+
+method test1(x: Ref)
+{
+   inhale acc(x.f, none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo(x)
+}
+
+@exhaleMode("mce")
+method test1mce(x: Ref)
+{
+   inhale acc(x.f, none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo(x)
+}
+
+method test1qp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo(x)
+}
+
+method test1p(x: Ref)
+{
+   inhale acc(P(x), none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foop(x)
+}
+
+@exhaleMode("mce")
+method test1pmce(x: Ref)
+{
+   inhale acc(P(x), none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foop(x)
+}
+
+method test1pqp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(P(y), none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foop(x)
+}
+
+method test2(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2(x, b)
+}
+
+@exhaleMode("mce")
+method test2mce(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2(x, b)
+}
+
+method test2qp(x: Ref, b: Bool)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2(x, b)
+}
+
+
+method test3(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo2(x, !b)
+}
+
+@exhaleMode("mce")
+method test3mce(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo2(x, !b)
+}
+
+method test3qp(x: Ref, b: Bool)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, b ? 1/2 : none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo2(x, !b)
+}
+
+method test2w(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2w(x, b)
+}
+
+@exhaleMode("mce")
+method test2mcew(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2w(x, b)
+}
+
+method test2qpw(x: Ref, b: Bool)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2w(x, b)
+}
+
+
+method test3w(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo2w(x, !b)
+}
+
+@exhaleMode("mce")
+method test3mcew(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo2w(x, !b)
+}
+
+method test3qpw(x: Ref, b: Bool)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, b ? 1/2 : none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo2w(x, !b)
+}
+
+method test4(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo3(x)
+}
+
+@exhaleMode("mce")
+method test4mce(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo3(x)
+}
+
+method test4qp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, 1/2)
+   var tmp: Int
+   tmp := foo3(x)
+}
+
+method test4f(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo3(x)
+}
+
+@exhaleMode("mce")
+method test4mcef(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo3(x)
+}
+
+method test4qpf(x: Ref)
+{
+   inhale forall y: Ref :: false ==> acc(y.f, 1/2)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo3(x)
+}
+
+method test5(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo4(x)
+}
+
+@exhaleMode("mce")
+method test5mce(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo4(x)
+}
+
+method test5qp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, 1/2)
+   var tmp: Int
+   tmp := foo4(x)
+}
+
+method test5f(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo4(x)
+}
+
+@exhaleMode("mce")
+method test5mcef(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo4(x)
+}
+
+method test5qpf(x: Ref)
+{
+   inhale forall y: Ref :: false ==> acc(y.f, 1/2)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo4(x)
+}
+
+method test6(x: Ref)
+{
+   inhale acc(x.f, 1/4)
+   assume x.f == 4
+   fold acc(P(x), 1/4)
+   var tmp: Int
+   tmp := bar4(x)
+}
+
+method test6f(x: Ref)
+{
+   inhale acc(x.f, 1/4)
+   assume x.f == -2
+   fold acc(P(x), 1/4)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:assertion.false)
+   tmp := bar4(x)
+}
+
+
+method test7(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo5(x)
+}
+
+method test7f(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo5(x)
+}
+
+method test7p(x: Ref)
+{
+   inhale acc(P(x), 1/2)
+   var tmp: Int
+   tmp := foo5p(x)
+}
+
+method test7pf(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo5p(x)
+}
+
+method test8(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo5w(x)
+}
+
+method test8f(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo5w(x)
+}
+
+method test8p(x: Ref)
+{
+   inhale acc(P(x), 1/2)
+   var tmp: Int
+   tmp := foo5pw(x)
+}
+
+method test8pf(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo5pw(x)
+}
\ No newline at end of file
diff --git a/src/test/resources/all/issues/carbon/0196.vpr b/src/test/resources/all/issues/carbon/0196.vpr
index fad99ad12..8aac168c3 100644
--- a/src/test/resources/all/issues/carbon/0196.vpr
+++ b/src/test/resources/all/issues/carbon/0196.vpr
@@ -33,7 +33,7 @@ method pred1(r: Ref)
     fold acc(P(r), wildcard)
     unfold acc(P(r), wildcard)
     var r2 : Ref := tester(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerFull(get(r))
 }
 
@@ -44,7 +44,7 @@ method pred2(r: Ref)
     fold acc(P(r))
     unfold acc(P(r))
     var r2 : Ref := tester(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerFull(get(r))
 }
 
@@ -55,7 +55,7 @@ method pred3(r: Ref)
     fold acc(P(r), 1/2)
     unfold acc(P(r), 1/2)
     var r2 : Ref := tester(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerFull(get(r))
 }
 
@@ -66,7 +66,7 @@ method pred4(r: Ref)
     fold acc(P2(r), wildcard)
     unfold acc(P2(r), wildcard)
     var r2 : Ref := tester(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerFull(get(r))
 }
 
@@ -77,7 +77,7 @@ method func1(r: Ref)
     fold acc(R(r), wildcard)
     unfold acc(R(r), wildcard)
     var r2 : Ref := testerfield(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerfieldFull(get(r))
 }
 
@@ -88,7 +88,7 @@ method func2(r: Ref)
     fold acc(R(r))
     unfold acc(R(r))
     var r2 : Ref := testerfield(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerfieldFull(get(r))
 }
 
@@ -99,7 +99,7 @@ method func3(r: Ref)
     fold acc(R(r), 1/2)
     unfold acc(R(r), 1/2)
     var r2 : Ref := testerfield(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerfieldFull(get(r))
 }
 
@@ -110,6 +110,6 @@ method func4(r: Ref)
     fold acc(R2(r), wildcard)
     unfold acc(R2(r), wildcard)
     var r2 : Ref := testerfield(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerfieldFull(get(r))
 }
diff --git a/src/test/resources/all/issues/carbon/0223.vpr b/src/test/resources/all/issues/carbon/0223.vpr
index f8a0aa193..4870d1282 100644
--- a/src/test/resources/all/issues/carbon/0223.vpr
+++ b/src/test/resources/all/issues/carbon/0223.vpr
@@ -11,7 +11,7 @@ predicate bar(x:Ref) {
 function get(x: Ref) : Int
   requires forall w:Ref :: {w in Set(x)} w in Set(x) ==> acc(bar(w))
   {
-    unfolding bar(x) in x.val
+    asserting (x in Set(x)) in unfolding bar(x) in x.val
   }
 
 method set(x:Ref, i:Int) 
diff --git a/src/test/resources/all/issues/silicon/0030.vpr b/src/test/resources/all/issues/silicon/0030.vpr
index 48c2165d6..48b05a221 100644
--- a/src/test/resources/all/issues/silicon/0030.vpr
+++ b/src/test/resources/all/issues/silicon/0030.vpr
@@ -1,12 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-function C__g(diz: Ref): Int
-   requires diz != null
-   requires acc(C__P(diz), wildcard)
-   requires acc(C__P(diz), 1 / 2)
-
-
 predicate C__P(diz: Ref)
 
 /** In Viper, exhale should proceed from left to write (earlier Carbon
@@ -16,10 +10,9 @@ Thus, exhale acc(x.f, wildcard) && acc(x.f, 1/2) is expected to fail.  */
 method C__main(diz: Ref)
    requires diz != null
    requires acc(C__P(diz), write)
-   //:: ExpectedOutput(application.precondition:insufficient.permission)
-   requires C__g(diz) > 0
 {
-
+   //:: ExpectedOutput(exhale.failed:insufficient.permission)
+   exhale acc(C__P(diz), wildcard) && acc(C__P(diz), 1 / 2)
 }
 
 method test(diz:Ref)
diff --git a/src/test/resources/all/issues/silicon/0240.vpr b/src/test/resources/all/issues/silicon/0240.vpr
index 3b2ef394d..b258a614b 100644
--- a/src/test/resources/all/issues/silicon/0240.vpr
+++ b/src/test/resources/all/issues/silicon/0240.vpr
@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
  field next: Ref
  field data: Int
 
@@ -54,7 +54,7 @@ method test04a(this: Ref)
 method test04b(this: Ref)
   requires acc(bla(this), 1/2)
 {
-  //:: ExpectedOutput(application.precondition:insufficient.permission)
+
   assert unfolding acc(bla(this), 1/2) in foo(this)
 }
 
@@ -98,6 +98,6 @@ method test04a_qp(xs: Set[Ref])
 method test04b_qp(xs: Set[Ref])
   requires acc(bla_qp(xs), 1/2)
 {
-  //:: ExpectedOutput(application.precondition:insufficient.permission)
+
   assert unfolding acc(bla_qp(xs), 1/2) in foo_qp(xs)
 }
diff --git a/src/test/resources/all/issues/silicon/0376.vpr b/src/test/resources/all/issues/silicon/0376.vpr
index 29d1c0842..9fed00943 100644
--- a/src/test/resources/all/issues/silicon/0376.vpr
+++ b/src/test/resources/all/issues/silicon/0376.vpr
@@ -23,6 +23,7 @@ field f: Int
 
 function foo(x: Ref): Int
   requires acc(x.f) && acc(x.f)
+  //:: ExpectedOutput(postcondition.violated:assertion.false)
   ensures false
 { x.f }
 
diff --git a/src/test/scala/ChopperTests.scala b/src/test/scala/ChopperTests.scala
index f954432c6..a20742ae8 100644
--- a/src/test/scala/ChopperTests.scala
+++ b/src/test/scala/ChopperTests.scala
@@ -223,7 +223,7 @@ class ChopperTests extends AnyFunSuite with Matchers with Inside {
     val callee = calleeStub.copy(body = Some(ast.TrueLit()()))(ast.NoPosition, ast.NoInfo, ast.NoTrafos)
     val call = ast.PredicateAccess(Seq.empty, predicateName = callee.name)()
     val caller1 = callerStub1.copy(body = Some(call))(ast.NoPosition, ast.NoInfo, ast.NoTrafos)
-    val unfolding = ast.Unfolding(ast.PredicateAccessPredicate(call, ast.FullPerm()())(), ast.TrueLit()())()
+    val unfolding = ast.Unfolding(ast.PredicateAccessPredicate(call, None)(), ast.TrueLit()())()
     val caller2 = callerStub2.copy(body = Some(unfolding))(ast.NoPosition, ast.NoInfo, ast.NoTrafos)
 
     val program = ast.Program(Seq.empty, Seq.empty, Seq.empty, Seq(callee, caller1, caller2), Seq.empty, Seq.empty)()
diff --git a/src/test/scala/ConsistencyTests.scala b/src/test/scala/ConsistencyTests.scala
index 3def23bdd..a44505272 100644
--- a/src/test/scala/ConsistencyTests.scala
+++ b/src/test/scala/ConsistencyTests.scala
@@ -157,11 +157,11 @@ class ConsistencyTests extends AnyFunSuite with Matchers {
     val callerPosts =
       Seq(
         // Wrong: zero arguments
-        PredicateAccessPredicate(PredicateAccess(Seq(), "P")(), FullPerm()())(),
+        PredicateAccessPredicate(PredicateAccess(Seq(), "P")(), Some(FullPerm()()))(),
         // Wrong: wrong argument type
-        PredicateAccessPredicate(PredicateAccess(Seq(callerBoolVar), "P")(), FullPerm()())(),
+        PredicateAccessPredicate(PredicateAccess(Seq(callerBoolVar), "P")(), None)(),
         // Correct
-        PredicateAccessPredicate(PredicateAccess(Seq(callerIntVar), "P")(), FullPerm()())()
+        PredicateAccessPredicate(PredicateAccess(Seq(callerIntVar), "P")(), None)()
       )
 
     val caller =
@@ -250,7 +250,7 @@ class ConsistencyTests extends AnyFunSuite with Matchers {
   test("Testing if Forall AST nodes have implication as expression") {
 
     val f = Field("f", Int)()
-    val forall = Forall(Seq(LocalVarDecl("i", Int)()), Seq(), CondExp(FalseLit()(), TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("r", Ref)(), f)(), FullPerm()())())())()
+    val forall = Forall(Seq(LocalVarDecl("i", Int)()), Seq(), CondExp(FalseLit()(), TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("r", Ref)(), f)(), Some(FullPerm()()))())())()
 
     forall.checkTransitively shouldBe Seq(
       ConsistencyError("Quantified permissions must have an implication as expression, with the access predicate in its right-hand side.", NoPosition)
diff --git a/src/test/scala/FeatureCombinationsTests.scala b/src/test/scala/FeatureCombinationsTests.scala
index a2164a5bf..e1951c84e 100644
--- a/src/test/scala/FeatureCombinationsTests.scala
+++ b/src/test/scala/FeatureCombinationsTests.scala
@@ -30,7 +30,7 @@ class FeatureCombinationsTests extends AnyFunSuite with Matchers {
   }
 
   test("Forall of the Quantified Permissions form") {
-    val q0 = Forall( Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), FullPerm()())() )() )()
+    val q0 = Forall( Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), None)() )() )()
 
     assert(q0.isValid)
   }
@@ -46,7 +46,7 @@ class FeatureCombinationsTests extends AnyFunSuite with Matchers {
   test("Forall with predicate application in body expression") {
     val pred = PredicateAccess(Seq(LocalVar("x", Ref)()), "pred")(NoPosition, NoInfo, NoTrafos)
     val perm = FullPerm()()
-    val q1 = Forall(Seq(LocalVarDecl("i", Int)()), Seq(), PredicateAccessPredicate(pred, perm)())()
+    val q1 = Forall(Seq(LocalVarDecl("i", Int)()), Seq(), PredicateAccessPredicate(pred, Some(perm))())()
 
     assert(!q1.isValid)
   }
@@ -103,8 +103,8 @@ class FeatureCombinationsTests extends AnyFunSuite with Matchers {
   }
 
   test("Magic wand with Quantified Permissions") {
-    val wand1 = MagicWand(TrueLit()(), Forall(Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), FullPerm()())())() )())()
-    val wand2 = MagicWand(Forall(Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), FullPerm()())())() )(), TrueLit()())()
+    val wand1 = MagicWand(TrueLit()(), Forall(Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), None)())() )())()
+    val wand2 = MagicWand(Forall(Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), Some(FullPerm()()))())() )(), TrueLit()())()
 
     assert(!wand1.isValid)
     assert(!wand2.isValid)
diff --git a/src/test/scala/MethodDependencyTests.scala b/src/test/scala/MethodDependencyTests.scala
index 497c7fc66..d9639433e 100644
--- a/src/test/scala/MethodDependencyTests.scala
+++ b/src/test/scala/MethodDependencyTests.scala
@@ -94,24 +94,24 @@ class MethodDependencyTests extends AnyFunSuite with Matchers {
   val fun1: Function = Function("fun1", Seq(), Bool, Seq(), Seq(), None)()
   val fun2: Function = Function("fun2", Seq(), Bool, Seq(), Seq(), None)()
   val fun3: Function = Function("fun3", Seq(), Bool, Seq(), Seq(), None)()
-  val fun4: Function = Function("fun4", Seq(LocalVarDecl("x", Ref)()), Bool, Seq(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("f4", Bool)())(),FullPerm()())()), Seq(), None)()
+  val fun4: Function = Function("fun4", Seq(LocalVarDecl("x", Ref)()), Bool, Seq(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("f4", Bool)())(), None)()), Seq(), None)()
   val p0: Predicate = Predicate("p0", Seq(), None)()
   val p1: Predicate = Predicate("p1", Seq(), None)()
   val p2: Predicate = Predicate("p2", Seq(), None)()
   val p3: Predicate = Predicate("p3", Seq(), None)()
   val p4: Predicate = Predicate("p4", Seq(LocalVarDecl("x", Ref)()), Some(FuncApp(fun4, Seq(LocalVar("x", Ref)()))()))()
   val m1: Method = Method("m1", Seq(), Seq(), Seq(), Seq(), Some(Seqn(Seq(), Seq())()))()
-  val m0: Method = Method("m0", Seq(LocalVarDecl("x", Ref)()), Seq(), Seq(PredicateAccessPredicate(PredicateAccess(Seq(LocalVar("x", Ref)()), p4.name)(), FullPerm()())()), Seq(), Some(Seqn(Seq(MethodCall(m1,Seq(),Seq())()), Seq())()))()
+  val m0: Method = Method("m0", Seq(LocalVarDecl("x", Ref)()), Seq(), Seq(PredicateAccessPredicate(PredicateAccess(Seq(LocalVar("x", Ref)()), p4.name)(), Some(FullPerm()()))()), Seq(), Some(Seqn(Seq(MethodCall(m1,Seq(),Seq())()), Seq())()))()
   val test: Method = Method("test",
     Seq(LocalVarDecl("x", Ref)()),
     Seq(),
     // preconditions:
-    Seq(And(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), f0)(), FullPerm()())(), And(FuncApp(fun0, Seq())(), PredicateAccessPredicate(PredicateAccess(Seq(), p0.name)(), FullPerm()())())())()),
+    Seq(And(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), f0)(), None)(), And(FuncApp(fun0, Seq())(), PredicateAccessPredicate(PredicateAccess(Seq(), p0.name)(), Some(FullPerm()()))())())()),
     // postconditions:
-    Seq(And(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), f1)(), FullPerm()())(), And(FuncApp(fun1, Seq())(), PredicateAccessPredicate(PredicateAccess(Seq(), p1.name)(), FullPerm()())())())()),
+    Seq(And(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), f1)(), Some(FullPerm()()))(), And(FuncApp(fun1, Seq())(), PredicateAccessPredicate(PredicateAccess(Seq(), p1.name)(), None)())())()),
     // body of the method:
     Some(Seqn(Seq(
-      Unfold(PredicateAccessPredicate(PredicateAccess(Seq(), p2.name)(), FullPerm()())())(),
+      Unfold(PredicateAccessPredicate(PredicateAccess(Seq(), p2.name)(), None)())(),
       While(TrueLit()(), Seq(FieldAccess(LocalVar("x", Ref)(), f2)()), Seqn(Seq(
         // body of the outer loop
         While(TrueLit()(), Seq(FuncApp(fun2, Seq())()), Seqn(Seq(
diff --git a/src/test/scala/SimplifierTests.scala b/src/test/scala/SimplifierTests.scala
index 896862a9a..a6bbec1d0 100644
--- a/src/test/scala/SimplifierTests.scala
+++ b/src/test/scala/SimplifierTests.scala
@@ -19,7 +19,7 @@ class SimplifierTests extends AnyFunSuite with Matchers {
     val b = LocalVar("a", Bool)()
     val acc = PredicateAccessPredicate(
       PredicateAccess(Nil, "pred")(),
-      FullPerm()()
+      None
     )()
     val tru = TrueLit()()
 
diff --git a/src/test/scala/UtilityTests.scala b/src/test/scala/UtilityTests.scala
index 950723562..c98e62f92 100644
--- a/src/test/scala/UtilityTests.scala
+++ b/src/test/scala/UtilityTests.scala
@@ -15,7 +15,7 @@ class UtilityTests extends AnyFunSuite with Matchers {
   /* These tests exercise utility methods on the AST (transformers, visitors, rewriters etc.) */
 
   test("Assume rewriter (direct)"){ // assume acc(x.f) -> rewritten to -> assume perm(x.f) >= write
-    val assumeBody = FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(),Field("f",Int)(NoPosition))(NoPosition), FullPerm()(NoPosition))(NoPosition)
+    val assumeBody = FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(),Field("f",Int)(NoPosition))(NoPosition), Some(FullPerm()(NoPosition)))(NoPosition)
     val testMethod : Method = Method("m1", Seq(), Seq(), Seq(), Seq(),
       Some(Seqn(Seq(
         Assume(assumeBody)(NoPosition)