From 31a18040f7a442b97d36b1c30cfd559b6edf06f3 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Tue, 18 Oct 2022 16:51:27 +0200
Subject: [PATCH 1/6] adds support for forall quantifiers and wildcard
 permission amounts to the expression transformer

---
 .../transformation/ExpTransformer.scala       | 25 +++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
index bf8cae588..f5c9b080b 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
@@ -6,7 +6,7 @@
 
 package viper.silver.plugin.standard.termination.transformation
 
-import viper.silver.ast.{Exp, Stmt, _}
+import viper.silver.ast.{And, Exp, Stmt, _}
 import viper.silver.ast.utility.Statements.EmptyStmt
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.{ContextCustom, RepeatedStrategy, Strategy, Traverse}
@@ -15,7 +15,7 @@ import viper.silver.ast.utility.rewriter.{ContextCustom, RepeatedStrategy, Strat
  * A basic interface which helps to rewrite an expression (e.g. a function body) into a stmt (e.g. for a method body).
  * Some default transformations are already implemented.
  */
-trait ExpTransformer extends ErrorReporter {
+trait ExpTransformer extends ProgramManager with ErrorReporter {
 
   /**
    * Transforms an expression into a statement.
@@ -125,6 +125,8 @@ trait ExpTransformer extends ErrorReporter {
     case (_: Literal, _) => EmptyStmt
     case (_: AbstractLocalVar, _) => EmptyStmt
     case (_: AbstractConcretePerm, _) => EmptyStmt
+    case (_: WildcardPerm, _) => EmptyStmt
+    case (_: EpsilonPerm, _) => EmptyStmt
     case (_: LocationAccess, _) => EmptyStmt
 
     case (ap: AccessPredicate, c) =>
@@ -133,6 +135,22 @@ trait ExpTransformer extends ErrorReporter {
       val inhale = Inhale(ap)(ap.pos)
 
       Seqn(Seq(check, inhale), Nil)()
+    case (fa: Forall, c) =>
+      val declMapping = fa.variables.map(decl => decl -> uniqueName(decl.name))
+      val freshDecls = declMapping.map {
+        case (oldDecl, freshName) => LocalVarDecl(freshName, oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT)
+      }
+      val transformedExp = fa.exp.transform({
+        case v@LocalVar(name, typ) => declMapping
+          // check whether the local variable is in the map of variables that should be replaced:
+          .collectFirst { case (decl, freshName) if decl.name == name => freshName }
+          // replace it by a new local variable:
+          .map(freshName => LocalVar(freshName, typ)(v.pos, v.info, v.errT))
+          // keep the variable unchanged if no replacement should happen:
+          .getOrElse(v)
+      }, Traverse.TopDown)
+      val expressionStmt = transformExp(transformedExp, c)
+      Seqn(Seq(expressionStmt), freshDecls)(fa.pos)
     case (fa: FuncLikeApp, c) =>
       val argStmts = fa.args.map(transformExp(_, c))
       Seqn(argStmts, Nil)()
@@ -209,6 +227,9 @@ trait ExpTransformer extends ErrorReporter {
       If(Not(c)(c.pos), els, EmptyStmt)(i.pos, i.info, i.errT)
     case i@If(c1, Seqn(Seq(If(c2, thn, EmptyStmt)), Nil), EmptyStmt) => // combine nested if clauses
       If(And(c1, c2)(), thn, EmptyStmt)(i.pos, i.info, i.errT)
+    case If(TrueLit(), thn, _) => thn // remove trivial If conditions (in particular effective together with the next 2 simplifications)
+    case And(TrueLit(), rhs) => rhs // simplify conjunctions
+    case And(lhs, TrueLit()) => lhs // simplify conjunctions
   }, Traverse.BottomUp)
     .repeat
 }

From f6b1db65f7a71ae193230ff3d2e2d926105d7fe4 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Tue, 18 Oct 2022 17:40:08 +0200
Subject: [PATCH 2/6] adds support for sets and multisets to expression
 transformer

---
 .../transformation/ExpTransformer.scala       | 30 ++++++++++++++-----
 1 file changed, 23 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
index f5c9b080b..bc5374c2f 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
@@ -75,6 +75,29 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
           Seqn(Seq(right), Nil)()
       }
       Seqn(Seq(left, rightSCE), Nil)()
+    case (ase: AnySetExp, c) => ase match {
+      case AnySetCardinality(s) => Seqn(Seq(transformExp(s, c)), Nil)(ase.pos)
+      case AnySetUnion(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
+      case AnySetIntersection(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
+      case AnySetSubset(l ,r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
+      case AnySetMinus(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
+      case AnySetContains(elem, s) => Seqn(Seq(transformExp(elem, c), transformExp(s, c)), Nil)(ase.pos)
+      case MapDomain(base) => Seqn(Seq(transformExp(base, c)), Nil)(ase.pos)
+      case MapRange(base) => Seqn(Seq(transformExp(base, c)), Nil)(ase.pos)
+      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
+    }
+    case (st: SetExp, c) => st match {
+      // note that AnySetExp are handled above
+      case ExplicitSet(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(st.pos)
+      case EmptySet(_) => EmptyStmt
+      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
+    }
+    case (ms: MultisetExp, c) => ms match {
+      // note that AnySetExp are handled above
+      case EmptyMultiset(_) => EmptyStmt
+      case ExplicitMultiset(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(ms.pos)
+      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
+    }
     case (sq: SeqExp, c) => sq match {
       case ExplicitSeq(elems) =>
         Seqn(elems.map(transformExp(_, c)), Nil)(sq.pos)
@@ -104,7 +127,6 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
         Seqn(Seq(transformExp(s, c)), Nil)(sq.pos)
       case EmptySeq(_) => EmptyStmt
       case unsupportedExp => transformUnknownExp(unsupportedExp, c)
-        EmptyStmt
     }
     case (mp: MapExp, c) => mp match {
       case EmptyMap(_, _) => EmptyStmt
@@ -115,12 +137,6 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
       case MapLookup(base, key) => Seqn(Seq(transformExp(base, c), transformExp(key, c)), Nil)(mp.pos)
       case MapUpdate(base, key, value) => Seqn(Seq(transformExp(base, c), transformExp(key, c), transformExp(value, c)), Nil)(mp.pos)
     }
-    case (st: ExplicitSet, c) =>
-      Seqn(st.elems.map(transformExp(_, c)), Nil)(st.pos)
-    case (mst: ExplicitMultiset, c) =>
-      Seqn(mst.elems.map(transformExp(_, c)), Nil)(mst.pos)
-    case (md: MapDomain, c) => Seqn(Seq(transformExp(md.base, c)), Nil)(md.pos)
-    case (mr: MapRange, c) => Seqn(Seq(transformExp(mr.base, c)), Nil)(mr.pos)
     case (u: UnExp, c) => transformExp(u.exp, c)
     case (_: Literal, _) => EmptyStmt
     case (_: AbstractLocalVar, _) => EmptyStmt

From c073e44635bd394f44a4002c353549df12072d6d Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 19 Oct 2022 10:08:50 +0200
Subject: [PATCH 3/6] further extends the expr transformer's support to
 existentials

---
 .../transformation/ExpTransformer.scala       | 47 ++++++++++++-----
 .../functions/expressions/exists.vpr          | 51 +++++++++++++++++++
 .../functions/expressions/forall.vpr          | 25 +++++++++
 .../functions/expressions/wildcard.vpr        | 13 +++++
 4 files changed, 122 insertions(+), 14 deletions(-)
 create mode 100644 src/test/resources/termination/functions/expressions/exists.vpr
 create mode 100644 src/test/resources/termination/functions/expressions/forall.vpr
 create mode 100644 src/test/resources/termination/functions/expressions/wildcard.vpr

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
index bc5374c2f..8ddd040e4 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
@@ -152,21 +152,19 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
 
       Seqn(Seq(check, inhale), Nil)()
     case (fa: Forall, c) =>
-      val declMapping = fa.variables.map(decl => decl -> uniqueName(decl.name))
-      val freshDecls = declMapping.map {
-        case (oldDecl, freshName) => LocalVarDecl(freshName, oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT)
-      }
-      val transformedExp = fa.exp.transform({
-        case v@LocalVar(name, typ) => declMapping
-          // check whether the local variable is in the map of variables that should be replaced:
-          .collectFirst { case (decl, freshName) if decl.name == name => freshName }
-          // replace it by a new local variable:
-          .map(freshName => LocalVar(freshName, typ)(v.pos, v.info, v.errT))
-          // keep the variable unchanged if no replacement should happen:
-          .getOrElse(v)
-      }, Traverse.TopDown)
+      // we turn the quantified variables into local variables with arbitrary value and show that the expression holds
+      // for arbitrary values, which is similar to a forall introduction
+      val (freshDecls, transformedExp) = substituteWithFreshVars(fa.variables, fa.exp)
+      val expressionStmt = transformExp(transformedExp, c)
+      Seqn(Seq(expressionStmt), freshDecls)(fa.pos, fa.info, fa.errT)
+    case (ex: Exists, c) =>
+      // we perform existential elimination by retrieving witnesses for the quantified variables
+      val (freshDecls, transformedExp) = substituteWithFreshVars(ex.variables, ex.exp)
+      // we can't use an assume statement at this point because the `assume`s have already been rewritten
+      // furthermore, Viper only allows pure existentially quantified expressions
+      val inhaleWitnesses = Inhale(transformedExp)(ex.pos, ex.info, ex.errT)
       val expressionStmt = transformExp(transformedExp, c)
-      Seqn(Seq(expressionStmt), freshDecls)(fa.pos)
+      Seqn(Seq(inhaleWitnesses, expressionStmt), freshDecls)(ex.pos, ex.info, ex.errT)
     case (fa: FuncLikeApp, c) =>
       val argStmts = fa.args.map(transformExp(_, c))
       Seqn(argStmts, Nil)()
@@ -216,6 +214,27 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
     case Forall(_, _, exp) => Seq(exp)
   }
 
+  /**
+    * Turns `vars` into new local variable declarations with a unique name and replaces their occurrences in `exp`.
+    * The new local variables declarations and the transformed expression are returned
+    */
+  protected def substituteWithFreshVars(vars: Seq[LocalVarDecl], exp: Exp): (Seq[LocalVarDecl], Exp) = {
+    val declMapping = vars.map(decl => decl -> uniqueName(decl.name))
+    val freshDecls = declMapping.map {
+      case (oldDecl, freshName) => LocalVarDecl(freshName, oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT)
+    }
+    val transformedExp = exp.transform({
+      case v@LocalVar(name, typ) => declMapping
+        // check whether the local variable is in the map of variables that should be replaced:
+        .collectFirst { case (decl, freshName) if decl.name == name => freshName }
+        // replace it by a new local variable:
+        .map(freshName => LocalVar(freshName, typ)(v.pos, v.info, v.errT))
+        // keep the variable unchanged if no replacement should happen:
+        .getOrElse(v)
+    }, Traverse.TopDown)
+    (freshDecls, transformedExp)
+  }
+
 
   /**
    * The simplifyStmts Strategy can be used to simplify statements
diff --git a/src/test/resources/termination/functions/expressions/exists.vpr b/src/test/resources/termination/functions/expressions/exists.vpr
new file mode 100644
index 000000000..fd7fb48bc
--- /dev/null
+++ b/src/test/resources/termination/functions/expressions/exists.vpr
@@ -0,0 +1,51 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+
+function test(x: Ref): Bool
+    decreases
+{
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    exists x2: Ref :: x == x2 && nonTerminating(x2)
+}
+
+function test2(): Bool
+    decreases
+{
+    // in general `partiallyTerminating` is non-terminating
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    exists x2: Int :: partiallyTerminating(x2)
+}
+
+function test3(x: Int): Bool
+    decreases
+    requires x == 42
+{
+    // `partiallyTerminating` terminates for input `42` so this is fine
+    exists x2: Int :: x == x2 && partiallyTerminating(x2)
+}
+
+function test4(x: Int): Bool
+    decreases
+{
+    // in general `partiallyTerminating` is non-terminating
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    (exists x2: Int :: x == x2) && partiallyTerminating(x)
+}
+
+function test5(x: Int): Bool
+    decreases
+{
+    // this is fine due to short-circuiting
+    (exists x2: Int :: x == x2 && x != x2) && partiallyTerminating(x)
+}
+
+function nonTerminating(x: Ref): Bool
+    decreases *
+
+function partiallyTerminating(x: Int): Bool
+    decreases if x == 42
+    decreases *
diff --git a/src/test/resources/termination/functions/expressions/forall.vpr b/src/test/resources/termination/functions/expressions/forall.vpr
new file mode 100644
index 000000000..e1ebb0c82
--- /dev/null
+++ b/src/test/resources/termination/functions/expressions/forall.vpr
@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+
+function test(x: Ref): Bool
+    decreases
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    requires forall x2: Ref :: x == x2 ==> acc(x2.f) && nonTerminating(x2)
+{
+    true
+}
+
+function test2(x: Ref): Bool
+    decreases
+    // this is fine because `nonTerminating(x2)` is not reachable
+    requires forall x2: Ref :: x == x2 ==> false && nonTerminating(x2)
+{
+    true
+}
+
+function nonTerminating(x: Ref): Bool
+    decreases *
diff --git a/src/test/resources/termination/functions/expressions/wildcard.vpr b/src/test/resources/termination/functions/expressions/wildcard.vpr
new file mode 100644
index 000000000..852d807b1
--- /dev/null
+++ b/src/test/resources/termination/functions/expressions/wildcard.vpr
@@ -0,0 +1,13 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+
+function test(x: Ref): Bool
+    decreases
+    requires acc(x.f, wildcard)
+{
+    true
+}

From 5daeb7bad81cc6a9cac2a3dbd0390015b877040d Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 20 Oct 2022 15:43:55 +0200
Subject: [PATCH 4/6] adds missing expressions to the expression transformer

---
 .../transformation/ExpTransformer.scala       | 182 +++++++++---------
 .../transformation/FunctionCheck.scala        |  21 +-
 .../functions/expressions/forperm.vpr         |  26 +++
 .../functions/expressions/unfolding.vpr       |  40 ++++
 4 files changed, 155 insertions(+), 114 deletions(-)
 create mode 100644 src/test/resources/termination/functions/expressions/forperm.vpr

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
index 8ddd040e4..57e1f65bb 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
@@ -6,10 +6,11 @@
 
 package viper.silver.plugin.standard.termination.transformation
 
-import viper.silver.ast.{And, Exp, Stmt, _}
+import viper.silver.ast.{And, AnySetExp, Exp, Stmt, _}
 import viper.silver.ast.utility.Statements.EmptyStmt
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.{ContextCustom, RepeatedStrategy, Strategy, Traverse}
+import viper.silver.verifier.ConsistencyError
 
 /**
  * A basic interface which helps to rewrite an expression (e.g. a function body) into a stmt (e.g. for a method body).
@@ -22,8 +23,8 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
    *
    * @return a statement representing the expression.
    */
-  def transformExp: PartialFunction[(Exp, ExpressionContext), Stmt] = {
-    case (CondExp(cond, thn, els), c) =>
+  def transformExp(e: Exp, c: ExpressionContext): Stmt = e match {
+    case CondExp(cond, thn, els) =>
       val condStmt = transformExp(cond, c)
       val thnStmt = transformExp(thn, c)
       val elsStmt = transformExp(els, c)
@@ -32,7 +33,7 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
 
       val stmts = Seq(condStmt, ifStmt)
       Seqn(stmts, Nil)()
-    case (Unfolding(acc, unfBody), c) =>
+    case Unfolding(acc, unfBody) =>
       val permCheck = transformExp(acc.perm, c)
       val unfoldBody = transformExp(unfBody, c)
       // only unfold and fold if body contains something
@@ -40,7 +41,15 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
 
       val stmts = Seq(permCheck, unfold, unfoldBody, fold)
       Seqn(stmts, Nil)()
-    case (inex: InhaleExhaleExp, c) =>
+    case Applying(wand, body) =>
+      // note that this case is untested -- it's not possible to write a function with an `applying` expression
+      val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT)
+      val bodyStmt = transformExp(body, c)
+      val killBranchStmt = Inhale(FalseLit()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
+      val thnStmt = Seqn(Seq(Apply(wand)(e.pos, e.info, e.errT), bodyStmt, killBranchStmt), Nil)()
+      val ifStmt = If(nonDetVarDecl.localVar, thnStmt, EmptyStmt)(e.pos, e.info, e.errT)
+      Seqn(Seq(ifStmt), Seq(nonDetVarDecl))(e.pos, e.info, e.errT)
+    case inex: InhaleExhaleExp =>
       val inhaleStmt = transformExp(inex.in, c)
       val exhaleStmt = transformExp(inex.ex, c)
 
@@ -48,7 +57,7 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
         case Some(conditionVar) => If(conditionVar.localVar, Seqn(Seq(inhaleStmt), Nil)(), Seqn(Seq(exhaleStmt), Nil)())()
         case None => Seqn(Seq(inhaleStmt, exhaleStmt), Nil)()
       }
-    case (letExp: Let, c) =>
+    case letExp: Let =>
       val expressionStmt = transformExp(letExp.exp, c)
       val localVarDecl = letExp.variable
 
@@ -58,7 +67,7 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
 
       Seqn(Seq(expressionStmt, inhaleEq, bodyStmt), Seq(localVarDecl))()
 
-    case (b: BinExp, c) =>
+    case b: BinExp =>
       val left = transformExp(b.left, c)
       val right = transformExp(b.right, c)
 
@@ -75,112 +84,90 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
           Seqn(Seq(right), Nil)()
       }
       Seqn(Seq(left, rightSCE), Nil)()
-    case (ase: AnySetExp, c) => ase match {
-      case AnySetCardinality(s) => Seqn(Seq(transformExp(s, c)), Nil)(ase.pos)
-      case AnySetUnion(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
-      case AnySetIntersection(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
-      case AnySetSubset(l ,r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
-      case AnySetMinus(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
-      case AnySetContains(elem, s) => Seqn(Seq(transformExp(elem, c), transformExp(s, c)), Nil)(ase.pos)
+    case ase: AnySetExp => ase match {
+      case exp: AnySetUnExp => Seqn(Seq(transformExp(exp.exp, c)), Nil)(ase.pos)
+      case exp: AnySetBinExp => Seqn(Seq(transformExp(exp.left, c), transformExp(exp.right, c)), Nil)(ase.pos)
       case MapDomain(base) => Seqn(Seq(transformExp(base, c)), Nil)(ase.pos)
       case MapRange(base) => Seqn(Seq(transformExp(base, c)), Nil)(ase.pos)
-      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
     }
-    case (st: SetExp, c) => st match {
-      // note that AnySetExp are handled above
-      case ExplicitSet(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(st.pos)
-      case EmptySet(_) => EmptyStmt
-      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
-    }
-    case (ms: MultisetExp, c) => ms match {
-      // note that AnySetExp are handled above
-      case EmptyMultiset(_) => EmptyStmt
-      case ExplicitMultiset(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(ms.pos)
-      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
-    }
-    case (sq: SeqExp, c) => sq match {
-      case ExplicitSeq(elems) =>
-        Seqn(elems.map(transformExp(_, c)), Nil)(sq.pos)
-      case RangeSeq(low, high) =>
-        Seqn(Seq(transformExp(low, c),
-          transformExp(high, c)), Nil)(sq.pos)
-      case SeqAppend(left, right) =>
-        Seqn(Seq(transformExp(left, c),
-          transformExp(right, c)), Nil)(sq.pos)
-      case SeqIndex(s, idx) =>
-        Seqn(Seq(transformExp(s, c),
-          transformExp(idx, c)), Nil)(sq.pos)
-      case SeqTake(s, n) =>
-        Seqn(Seq(transformExp(s, c),
-          transformExp(n, c)), Nil)(sq.pos)
-      case SeqDrop(s, n) =>
-        Seqn(Seq(transformExp(s, c),
-          transformExp(n, c)), Nil)(sq.pos)
-      case SeqContains(elem, s) =>
-        Seqn(Seq(transformExp(elem, c),
-          transformExp(s, c)), Nil)(sq.pos)
-      case SeqUpdate(s, idx, elem) =>
-        Seqn(Seq(transformExp(s, c),
-          transformExp(idx, c),
-          transformExp(elem, c)), Nil)(sq.pos)
-      case SeqLength(s) =>
-        Seqn(Seq(transformExp(s, c)), Nil)(sq.pos)
-      case EmptySeq(_) => EmptyStmt
-      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
-    }
-    case (mp: MapExp, c) => mp match {
-      case EmptyMap(_, _) => EmptyStmt
-      case ExplicitMap(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(mp.pos)
-      case Maplet(key, value) => Seqn(Seq(transformExp(key, c), transformExp(value, c)), Nil)(mp.pos)
-      case MapCardinality(base) => Seqn(Seq(transformExp(base, c)), Nil)(mp.pos)
-      case MapContains(key, base) => Seqn(Seq(transformExp(key, c), transformExp(base, c)), Nil)(mp.pos)
-      case MapLookup(base, key) => Seqn(Seq(transformExp(base, c), transformExp(key, c)), Nil)(mp.pos)
-      case MapUpdate(base, key, value) => Seqn(Seq(transformExp(base, c), transformExp(key, c), transformExp(value, c)), Nil)(mp.pos)
-    }
-    case (u: UnExp, c) => transformExp(u.exp, c)
-    case (_: Literal, _) => EmptyStmt
-    case (_: AbstractLocalVar, _) => EmptyStmt
-    case (_: AbstractConcretePerm, _) => EmptyStmt
-    case (_: WildcardPerm, _) => EmptyStmt
-    case (_: EpsilonPerm, _) => EmptyStmt
-    case (_: LocationAccess, _) => EmptyStmt
+    // remaining `SetExp`:
+    case EmptySet(_) => EmptyStmt
+    case e@ExplicitSet(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(e.pos)
+    // remaining `MultisetExp`:
+    case EmptyMultiset(_) => EmptyStmt
+    case e@ExplicitMultiset(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(e.pos)
+    // remaining `SeqExp`:
+    case EmptySeq(_) => EmptyStmt
+    case e@ExplicitSeq(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(e.pos)
+    case e@RangeSeq(low, high) => Seqn(Seq(transformExp(low, c), transformExp(high, c)), Nil)(e.pos)
+    case e@SeqAppend(left, right) => Seqn(Seq(transformExp(left, c), transformExp(right, c)), Nil)(e.pos)
+    case e@SeqIndex(s, idx) => Seqn(Seq(transformExp(s, c), transformExp(idx, c)), Nil)(e.pos)
+    case e@SeqTake(s, n) => Seqn(Seq(transformExp(s, c), transformExp(n, c)), Nil)(e.pos)
+    case e@SeqDrop(s, n) => Seqn(Seq(transformExp(s, c), transformExp(n, c)), Nil)(e.pos)
+    case e@SeqContains(elem, s) => Seqn(Seq(transformExp(elem, c), transformExp(s, c)), Nil)(e.pos)
+    case e@SeqUpdate(s, idx, elem) => Seqn(Seq(transformExp(s, c), transformExp(idx, c), transformExp(elem, c)), Nil)(e.pos)
+    case e@SeqLength(s) => Seqn(Seq(transformExp(s, c)), Nil)(e.pos)
+    // remaining `MapExp`:
+    case EmptyMap(_, _) => EmptyStmt
+    case e@ExplicitMap(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(e.pos)
+    case e@Maplet(key, value) => Seqn(Seq(transformExp(key, c), transformExp(value, c)), Nil)(e.pos)
+    case e@MapCardinality(base) => Seqn(Seq(transformExp(base, c)), Nil)(e.pos)
+    case e@MapContains(key, base) => Seqn(Seq(transformExp(key, c), transformExp(base, c)), Nil)(e.pos)
+    case e@MapLookup(base, key) => Seqn(Seq(transformExp(base, c), transformExp(key, c)), Nil)(e.pos)
+    case e@MapUpdate(base, key, value) => Seqn(Seq(transformExp(base, c), transformExp(key, c), transformExp(value, c)), Nil)(e.pos)
 
-    case (ap: AccessPredicate, c) =>
-      val check = transformExp(ap.perm, c)
+    case u: UnExp => transformExp(u.exp, c)
+    case _: Literal => EmptyStmt
+    case _: AbstractLocalVar => EmptyStmt
+    case _: AbstractConcretePerm => EmptyStmt
+    case _: WildcardPerm => EmptyStmt
+    case _: EpsilonPerm => EmptyStmt
+    case _: CurrentPerm => EmptyStmt
+    case _: LocationAccess => EmptyStmt
 
+    case ap: AccessPredicate =>
+      val check = transformExp(ap.perm, c)
       val inhale = Inhale(ap)(ap.pos)
-
       Seqn(Seq(check, inhale), Nil)()
-    case (fa: Forall, c) =>
+    case fa: Forall =>
       // we turn the quantified variables into local variables with arbitrary value and show that the expression holds
       // for arbitrary values, which is similar to a forall introduction
-      val (freshDecls, transformedExp) = substituteWithFreshVars(fa.variables, fa.exp)
+      val (freshDecls, transformedExp, _) = substituteWithFreshVars(fa.variables, fa.exp)
       val expressionStmt = transformExp(transformedExp, c)
       Seqn(Seq(expressionStmt), freshDecls)(fa.pos, fa.info, fa.errT)
-    case (ex: Exists, c) =>
+    case fp: ForPerm =>
+      // let's pick arbitrary values for the quantified variables and check the body given that the current heap has
+      // sufficient permissions
+      val (freshDecls, transformedExp, varMapping) = substituteWithFreshVars(fp.variables, fp.exp)
+      val transformedRes = substituteVars(varMapping, fp.resource)
+      val expressionStmt = transformExp(transformedExp, c)
+      val killBranchStmt = Inhale(FalseLit()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
+      val thnStmt = Seqn(Seq(expressionStmt, killBranchStmt), Nil)(e.pos, e.info, e.errT)
+      val ifCond = GtCmp(CurrentPerm(transformedRes)(e.pos, e.info, e.errT), NoPerm()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
+      val ifStmt = If(ifCond, thnStmt, EmptyStmt)(e.pos, e.info, e.errT)
+      Seqn(Seq(ifStmt), freshDecls)(e.pos, e.info, e.errT)
+    case ex: Exists =>
       // we perform existential elimination by retrieving witnesses for the quantified variables
-      val (freshDecls, transformedExp) = substituteWithFreshVars(ex.variables, ex.exp)
+      val (freshDecls, transformedExp, _) = substituteWithFreshVars(ex.variables, ex.exp)
       // we can't use an assume statement at this point because the `assume`s have already been rewritten
       // furthermore, Viper only allows pure existentially quantified expressions
       val inhaleWitnesses = Inhale(transformedExp)(ex.pos, ex.info, ex.errT)
       val expressionStmt = transformExp(transformedExp, c)
       Seqn(Seq(inhaleWitnesses, expressionStmt), freshDecls)(ex.pos, ex.info, ex.errT)
-    case (fa: FuncLikeApp, c) =>
+    case fa: FuncLikeApp =>
       val argStmts = fa.args.map(transformExp(_, c))
       Seqn(argStmts, Nil)()
-    case (unknownExp, c) =>
-      transformUnknownExp(unknownExp, c)
+    case e: ExtensionExp => reportUnsupportedExp(e)
   }
 
   /**
-   * Expression transformer if no default is defined.
-   * Calls transformExp on all subExps of e.
-   * To change or extend the default transformer for unknown expressions
-   * override this method (and possibly combine it with super.transformUnknownExp).
-   */
-  def transformUnknownExp(e: Exp, c: ExpressionContext): Stmt = {
-    val sub = e.subExps.map(transformExp(_, c))
-    Seqn(sub, Nil)()
+    * Issues a consistency error for unsupported expressions.
+    *
+    * @param unsupportedExp to be reported.
+    */
+  def reportUnsupportedExp(unsupportedExp: Exp): Stmt = {
+    reportError(ConsistencyError("Unsupported expression detected: " + unsupportedExp + ", " + unsupportedExp.getClass, unsupportedExp.pos))
+    EmptyStmt
   }
 
   /**
@@ -218,13 +205,18 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
     * Turns `vars` into new local variable declarations with a unique name and replaces their occurrences in `exp`.
     * The new local variables declarations and the transformed expression are returned
     */
-  protected def substituteWithFreshVars(vars: Seq[LocalVarDecl], exp: Exp): (Seq[LocalVarDecl], Exp) = {
+  protected def substituteWithFreshVars(vars: Seq[LocalVarDecl], exp: Exp): (Seq[LocalVarDecl], Exp, Seq[(LocalVarDecl, String)]) = {
     val declMapping = vars.map(decl => decl -> uniqueName(decl.name))
     val freshDecls = declMapping.map {
       case (oldDecl, freshName) => LocalVarDecl(freshName, oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT)
     }
-    val transformedExp = exp.transform({
-      case v@LocalVar(name, typ) => declMapping
+    val transformedExp = substituteVars(declMapping, exp)
+    (freshDecls, transformedExp, declMapping)
+  }
+
+  protected def substituteVars[T <: Node](varMapping: Seq[(LocalVarDecl, String)], n: T): T = {
+    n.transform({
+      case v@LocalVar(name, typ) => varMapping
         // check whether the local variable is in the map of variables that should be replaced:
         .collectFirst { case (decl, freshName) if decl.name == name => freshName }
         // replace it by a new local variable:
@@ -232,10 +224,8 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
         // keep the variable unchanged if no replacement should happen:
         .getOrElse(v)
     }, Traverse.TopDown)
-    (freshDecls, transformedExp)
   }
 
-
   /**
    * The simplifyStmts Strategy can be used to simplify statements
    * by e.g. removing or combining nested Seqn or If clauses.
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
index 80b616451..d0b20fd54 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
@@ -12,7 +12,6 @@ import viper.silver.ast.utility.rewriter.Traverse
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.{And, Bool, ErrTrafo, Exp, FalseLit, FuncApp, Function, LocalVarDecl, Method, Node, NodeTrafo, Old, Result, Seqn, Stmt}
 import viper.silver.plugin.standard.termination.{DecreasesSpecification, FunctionTerminationError}
-import viper.silver.verifier.ConsistencyError
 import viper.silver.verifier.errors.AssertFailed
 
 trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransformer with NestedPredicates with ErrorReporter {
@@ -137,8 +136,8 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
    *
    * @return a statement representing the expression
    */
-  override val transformExp: PartialFunction[(Exp, ExpressionContext), Stmt] = {
-    case (functionCall: FuncApp, context: FunctionContext) =>
+  override def transformExp(e: Exp, c: ExpressionContext): Stmt = (e, c) match {
+    case (functionCall: FuncApp, context: FunctionContext @unchecked) =>
       val stmts = collection.mutable.ArrayBuffer[Stmt]()
 
       // check the arguments
@@ -219,21 +218,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         // should not happen
       }
       Seqn(stmts.toSeq, Nil)()
-    case default => super.transformExp(default)
-  }
-
-  override def transformUnknownExp(e: Exp, c: ExpressionContext): Stmt = {
-    reportUnsupportedExp(e)
-    EmptyStmt
-  }
-
-  /**
-   * Issues a consistency error for unsupported expressions.
-   *
-   * @param unsupportedExp to be reported.
-   */
-  def reportUnsupportedExp(unsupportedExp: Exp): Unit = {
-    reportError(ConsistencyError("Unsupported expression detected: " + unsupportedExp + ", " + unsupportedExp.getClass, unsupportedExp.pos))
+    case _ => super.transformExp(e, c)
   }
 
   // context creator
diff --git a/src/test/resources/termination/functions/expressions/forperm.vpr b/src/test/resources/termination/functions/expressions/forperm.vpr
new file mode 100644
index 000000000..b329d47c9
--- /dev/null
+++ b/src/test/resources/termination/functions/expressions/forperm.vpr
@@ -0,0 +1,26 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+
+function test(x: Ref): Bool
+    decreases
+    requires acc(x.f)
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    requires [forperm x2: Ref [x2.f] :: nonTerminating(x2.f), true]
+{
+    true
+}
+
+function test2(x: Ref): Bool
+    decreases
+    // current heap does not hold any permissions so `nonTermination` is not evaluated
+    requires [forperm x2: Ref [x2.f] :: nonTerminating(x2.f), true]
+{
+    true
+}
+
+function nonTerminating(v: Int): Bool
+    decreases *
diff --git a/src/test/resources/termination/functions/expressions/unfolding.vpr b/src/test/resources/termination/functions/expressions/unfolding.vpr
index e69de29bb..37569e073 100644
--- a/src/test/resources/termination/functions/expressions/unfolding.vpr
+++ b/src/test/resources/termination/functions/expressions/unfolding.vpr
@@ -0,0 +1,40 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+
+predicate foo(x: Ref)
+{
+    acc(x.f) && x.f == 42
+}
+
+function test(x: Ref): Bool
+    decreases
+    requires foo(x)
+{
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    unfolding foo(x) in nonTerminating(x)
+}
+
+function test2(x: Ref): Bool
+    decreases
+    requires foo(x)
+{
+    unfolding foo(x) in partiallyTerminating(x)
+}
+
+function test3(x: Ref): Bool
+    decreases
+    requires foo(x)
+    // `unfolding` should indeed only temporarily unfold the predicate such that `nonTerminating(x)` is not reachable:
+    requires [true, (unfolding foo(x) in true) && (perm(x.f) > none ? nonTerminating(x) : true)]
+
+function nonTerminating(x: Ref): Bool
+    decreases *
+
+function partiallyTerminating(x: Ref): Bool
+    requires acc(x.f, wildcard)
+    decreases if x.f == 42
+    decreases *

From eec7cb1a59bca3e03a56157756f720846ecc8f2e Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 20 Oct 2022 17:47:35 +0200
Subject: [PATCH 5/6] moves the non-problematic simplifications from the
 termination plugin to the Simplifier

---
 .../viper/silver/ast/utility/Simplifier.scala |  17 ++-
 .../transformation/ExpTransformer.scala       | 123 +++++-------------
 .../transformation/FunctionCheck.scala        |   8 +-
 .../functions/expressions/access.vpr          |  25 ++++
 4 files changed, 72 insertions(+), 101 deletions(-)
 create mode 100644 src/test/resources/termination/functions/expressions/access.vpr

diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
index a64ab3023..fa731b5d3 100644
--- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -6,6 +6,7 @@
 
 package viper.silver.ast.utility
 
+import viper.silver.ast.utility.Statements.EmptyStmt
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter._
 
@@ -15,14 +16,15 @@ import viper.silver.ast.utility.rewriter._
 object Simplifier {
 
   /**
-   * Simplify `expression`, in particular by making use of literals. For
+   * Simplify `n`, in particular by making use of literals. For
    * example, `!true` is replaced by `false`. Division and modulo with divisor
    * 0 are not treated. Note that an expression with non-terminating evaluation due to endless recursion
    * might be transformed to terminating expression.
    */
-  def simplify(expression: Exp): Exp = {
+  def simplify[N <: Node](n: N): N = {
     /* Always simplify children first, then treat parent. */
     StrategyBuilder.Slim[Node]({
+      // expression simplifications
       case root @ Not(BoolLit(literal)) =>
         BoolLit(!literal)(root.pos, root.info)
       case Not(Not(single)) => single
@@ -112,7 +114,16 @@ object Simplifier {
         IntLit(left / right)(root.pos, root.info)
       case root @ Mod(IntLit(left), IntLit(right)) if right != bigIntZero =>
         IntLit((right.abs + (left % right)) % right.abs)(root.pos, root.info)
-    }, Traverse.BottomUp) execute[Exp](expression)
+
+      // statement simplifications
+      case Seqn(EmptyStmt, _) => EmptyStmt // remove empty Seqn (including unnecessary scopedDecls)
+      case s@Seqn(ss, scopedDecls) if ss.contains(EmptyStmt) => // remove empty statements
+        val newSS = ss.filterNot(_ == EmptyStmt)
+        Seqn(newSS, scopedDecls)(s.pos, s.info, s.errT)
+      case If(_, EmptyStmt, EmptyStmt) => EmptyStmt // remove empty If clause
+      case If(TrueLit(), thn, _) => thn // remove trivial If conditions
+      case If(FalseLit(), _, els) => els // remove trivial If conditions
+    }, Traverse.BottomUp) execute n
   }
 
   private val bigIntZero = BigInt(0)
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
index 57e1f65bb..e8b5fc324 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
@@ -6,10 +6,10 @@
 
 package viper.silver.plugin.standard.termination.transformation
 
-import viper.silver.ast.{And, AnySetExp, Exp, Stmt, _}
+import viper.silver.ast._
 import viper.silver.ast.utility.Statements.EmptyStmt
-import viper.silver.ast.utility.ViperStrategy
-import viper.silver.ast.utility.rewriter.{ContextCustom, RepeatedStrategy, Strategy, Traverse}
+import viper.silver.ast.utility.{Expressions, ViperStrategy}
+import viper.silver.ast.utility.rewriter.{ContextCustom, Strategy, Traverse}
 import viper.silver.verifier.ConsistencyError
 
 /**
@@ -84,39 +84,7 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
           Seqn(Seq(right), Nil)()
       }
       Seqn(Seq(left, rightSCE), Nil)()
-    case ase: AnySetExp => ase match {
-      case exp: AnySetUnExp => Seqn(Seq(transformExp(exp.exp, c)), Nil)(ase.pos)
-      case exp: AnySetBinExp => Seqn(Seq(transformExp(exp.left, c), transformExp(exp.right, c)), Nil)(ase.pos)
-      case MapDomain(base) => Seqn(Seq(transformExp(base, c)), Nil)(ase.pos)
-      case MapRange(base) => Seqn(Seq(transformExp(base, c)), Nil)(ase.pos)
-    }
-    // remaining `SetExp`:
-    case EmptySet(_) => EmptyStmt
-    case e@ExplicitSet(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(e.pos)
-    // remaining `MultisetExp`:
-    case EmptyMultiset(_) => EmptyStmt
-    case e@ExplicitMultiset(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(e.pos)
-    // remaining `SeqExp`:
-    case EmptySeq(_) => EmptyStmt
-    case e@ExplicitSeq(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(e.pos)
-    case e@RangeSeq(low, high) => Seqn(Seq(transformExp(low, c), transformExp(high, c)), Nil)(e.pos)
-    case e@SeqAppend(left, right) => Seqn(Seq(transformExp(left, c), transformExp(right, c)), Nil)(e.pos)
-    case e@SeqIndex(s, idx) => Seqn(Seq(transformExp(s, c), transformExp(idx, c)), Nil)(e.pos)
-    case e@SeqTake(s, n) => Seqn(Seq(transformExp(s, c), transformExp(n, c)), Nil)(e.pos)
-    case e@SeqDrop(s, n) => Seqn(Seq(transformExp(s, c), transformExp(n, c)), Nil)(e.pos)
-    case e@SeqContains(elem, s) => Seqn(Seq(transformExp(elem, c), transformExp(s, c)), Nil)(e.pos)
-    case e@SeqUpdate(s, idx, elem) => Seqn(Seq(transformExp(s, c), transformExp(idx, c), transformExp(elem, c)), Nil)(e.pos)
-    case e@SeqLength(s) => Seqn(Seq(transformExp(s, c)), Nil)(e.pos)
-    // remaining `MapExp`:
-    case EmptyMap(_, _) => EmptyStmt
-    case e@ExplicitMap(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(e.pos)
-    case e@Maplet(key, value) => Seqn(Seq(transformExp(key, c), transformExp(value, c)), Nil)(e.pos)
-    case e@MapCardinality(base) => Seqn(Seq(transformExp(base, c)), Nil)(e.pos)
-    case e@MapContains(key, base) => Seqn(Seq(transformExp(key, c), transformExp(base, c)), Nil)(e.pos)
-    case e@MapLookup(base, key) => Seqn(Seq(transformExp(base, c), transformExp(key, c)), Nil)(e.pos)
-    case e@MapUpdate(base, key, value) => Seqn(Seq(transformExp(base, c), transformExp(key, c), transformExp(value, c)), Nil)(e.pos)
 
-    case u: UnExp => transformExp(u.exp, c)
     case _: Literal => EmptyStmt
     case _: AbstractLocalVar => EmptyStmt
     case _: AbstractConcretePerm => EmptyStmt
@@ -132,32 +100,36 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
     case fa: Forall =>
       // we turn the quantified variables into local variables with arbitrary value and show that the expression holds
       // for arbitrary values, which is similar to a forall introduction
-      val (freshDecls, transformedExp, _) = substituteWithFreshVars(fa.variables, fa.exp)
+      val (localDeclMapping, transformedExp) = substituteWithFreshVars(fa.variables, fa.exp)
       val expressionStmt = transformExp(transformedExp, c)
-      Seqn(Seq(expressionStmt), freshDecls)(fa.pos, fa.info, fa.errT)
+      Seqn(Seq(expressionStmt), localDeclMapping.map(_._2))(fa.pos, fa.info, fa.errT)
     case fp: ForPerm =>
       // let's pick arbitrary values for the quantified variables and check the body given that the current heap has
       // sufficient permissions
-      val (freshDecls, transformedExp, varMapping) = substituteWithFreshVars(fp.variables, fp.exp)
-      val transformedRes = substituteVars(varMapping, fp.resource)
+      val (localDeclMapping, transformedExp) = substituteWithFreshVars(fp.variables, fp.exp)
+      val transformedRes = applySubstitution(localDeclMapping, fp.resource)
       val expressionStmt = transformExp(transformedExp, c)
       val killBranchStmt = Inhale(FalseLit()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
       val thnStmt = Seqn(Seq(expressionStmt, killBranchStmt), Nil)(e.pos, e.info, e.errT)
       val ifCond = GtCmp(CurrentPerm(transformedRes)(e.pos, e.info, e.errT), NoPerm()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
       val ifStmt = If(ifCond, thnStmt, EmptyStmt)(e.pos, e.info, e.errT)
-      Seqn(Seq(ifStmt), freshDecls)(e.pos, e.info, e.errT)
+      Seqn(Seq(ifStmt), localDeclMapping.map(_._2))(e.pos, e.info, e.errT)
     case ex: Exists =>
       // we perform existential elimination by retrieving witnesses for the quantified variables
-      val (freshDecls, transformedExp, _) = substituteWithFreshVars(ex.variables, ex.exp)
+      val (localDeclMapping, transformedExp) = substituteWithFreshVars(ex.variables, ex.exp)
       // we can't use an assume statement at this point because the `assume`s have already been rewritten
       // furthermore, Viper only allows pure existentially quantified expressions
       val inhaleWitnesses = Inhale(transformedExp)(ex.pos, ex.info, ex.errT)
       val expressionStmt = transformExp(transformedExp, c)
-      Seqn(Seq(inhaleWitnesses, expressionStmt), freshDecls)(ex.pos, ex.info, ex.errT)
+      Seqn(Seq(inhaleWitnesses, expressionStmt), localDeclMapping.map(_._2))(ex.pos, ex.info, ex.errT)
     case fa: FuncLikeApp =>
       val argStmts = fa.args.map(transformExp(_, c))
       Seqn(argStmts, Nil)()
     case e: ExtensionExp => reportUnsupportedExp(e)
+
+    case _ =>
+      val sub = e.subExps.map(transformExp(_, c))
+      Seqn(sub, Nil)()
   }
 
   /**
@@ -202,63 +174,26 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
   }
 
   /**
-    * Turns `vars` into new local variable declarations with a unique name and replaces their occurrences in `exp`.
-    * The new local variables declarations and the transformed expression are returned
+    * Turns `vars` into new local variable declarations with a unique name and replaces the corresponding local variable uses in `exp`.
+    * Returns a mapping of old variable declarations to new ones and the transformed expression
     */
-  protected def substituteWithFreshVars(vars: Seq[LocalVarDecl], exp: Exp): (Seq[LocalVarDecl], Exp, Seq[(LocalVarDecl, String)]) = {
-    val declMapping = vars.map(decl => decl -> uniqueName(decl.name))
-    val freshDecls = declMapping.map {
-      case (oldDecl, freshName) => LocalVarDecl(freshName, oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT)
-    }
-    val transformedExp = substituteVars(declMapping, exp)
-    (freshDecls, transformedExp, declMapping)
-  }
-
-  protected def substituteVars[T <: Node](varMapping: Seq[(LocalVarDecl, String)], n: T): T = {
-    n.transform({
-      case v@LocalVar(name, typ) => varMapping
-        // check whether the local variable is in the map of variables that should be replaced:
-        .collectFirst { case (decl, freshName) if decl.name == name => freshName }
-        // replace it by a new local variable:
-        .map(freshName => LocalVar(freshName, typ)(v.pos, v.info, v.errT))
-        // keep the variable unchanged if no replacement should happen:
-        .getOrElse(v)
-    }, Traverse.TopDown)
+  protected def substituteWithFreshVars[E <: Exp](vars: Seq[LocalVarDecl], exp: E): (Seq[(LocalVarDecl, LocalVarDecl)], E) = {
+    val declMapping = vars.map(oldDecl =>
+      oldDecl -> LocalVarDecl(uniqueName(oldDecl.name), oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT))
+    val transformedExp = applySubstitution(declMapping, exp)
+    (declMapping, transformedExp)
   }
 
   /**
-   * The simplifyStmts Strategy can be used to simplify statements
-   * by e.g. removing or combining nested Seqn or If clauses.
-   * This is in particular useful for the expression to statement transformer
-   * because this often creates nested and empty Seqn and If clauses.
-   *
-   * This is a repeating strategy because the removal of unneccessary unfold/fold statements requires EmptyStmts
-   * to be removed beforehand. Therefore, it should only be used with an maximum number of iterations (2).
-   *
-   */
-  val simplifyStmts: RepeatedStrategy[Node] = ViperStrategy.Slim({
-    case Seqn(EmptyStmt, _) => // remove empty Seqn (including unnecessary scopedDecls)
-      EmptyStmt
-    case s@Seqn(Seq(Seqn(ss, scopedDecls2)), scopedDecls1) => // combine nested Seqn
-      Seqn(ss, scopedDecls1 ++ scopedDecls2)(s.pos, s.info, s.errT)
-    case s@Seqn(ss, scopedDecls) if ss.contains(EmptyStmt) => // remove empty statements
-      val newSS = ss.filterNot(_ == EmptyStmt)
-      Seqn(newSS, scopedDecls)(s.pos, s.info, s.errT)
-    case Seqn(Seq(Unfold(acc1), Fold(acc2)), _) if acc1 == acc2 => // remove unfold/fold with nothing in between
-      EmptyStmt
-    case If(_, EmptyStmt, EmptyStmt) => // remove empty If clause
-      EmptyStmt
-    case i@If(c, EmptyStmt, els) => // change If with only els to If with only thn
-      If(Not(c)(c.pos), els, EmptyStmt)(i.pos, i.info, i.errT)
-    case i@If(c1, Seqn(Seq(If(c2, thn, EmptyStmt)), Nil), EmptyStmt) => // combine nested if clauses
-      If(And(c1, c2)(), thn, EmptyStmt)(i.pos, i.info, i.errT)
-    case If(TrueLit(), thn, _) => thn // remove trivial If conditions (in particular effective together with the next 2 simplifications)
-    case And(TrueLit(), rhs) => rhs // simplify conjunctions
-    case And(lhs, TrueLit()) => lhs // simplify conjunctions
-  }, Traverse.BottomUp)
-    .repeat
+    * Replaces uses of local variables in `exp` based on `mapping`.
+    * `mapping` maps local variable declarations to new declarations and this transformation replaces the corresponding
+    * local variable uses.
+    */
+  protected def applySubstitution[E <: Exp](mapping: Seq[(LocalVarDecl, LocalVarDecl)], exp: E): E = {
+    Expressions.instantiateVariables(exp, mapping.map(_._1.localVar), mapping.map(_._2.localVar))
+  }
 }
 
 trait ExpressionContext {
   val conditionInEx: Option[LocalVarDecl]
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
index d0b20fd54..6fe62e5b9 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
@@ -9,7 +9,7 @@ package viper.silver.plugin.standard.termination.transformation
 import org.jgrapht.graph.{DefaultDirectedGraph, DefaultEdge}
 import viper.silver.ast.utility.Statements.EmptyStmt
 import viper.silver.ast.utility.rewriter.Traverse
-import viper.silver.ast.utility.ViperStrategy
+import viper.silver.ast.utility.{Simplifier, ViperStrategy}
 import viper.silver.ast.{And, Bool, ErrTrafo, Exp, FalseLit, FuncApp, Function, LocalVarDecl, Method, Node, NodeTrafo, Old, Result, Seqn, Stmt}
 import viper.silver.plugin.standard.termination.{DecreasesSpecification, FunctionTerminationError}
 import viper.silver.verifier.errors.AssertFailed
@@ -53,7 +53,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         val context = FContext(f)
 
         val proofMethodBody: Stmt = {
-          val stmt: Stmt = simplifyStmts.execute(transformExp(f.body.get, context))
+          val stmt: Stmt = Simplifier.simplify(transformExp(f.body.get, context))
           if (requireNestedInfo) {
             addNestedPredicateInformation.execute(stmt)
           } else {
@@ -88,7 +88,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
           .reduce((e, p) => And(e, p)())
 
         val proofMethodBody: Stmt = {
-          val stmt: Stmt = simplifyStmts.execute(transformExp(posts, context))
+          val stmt: Stmt = Simplifier.simplify(transformExp(posts, context))
           if (requireNestedInfo) {
             addNestedPredicateInformation.execute(stmt)
           } else {
@@ -113,7 +113,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         // concatenate all pres
         val pres = f.pres.reduce((e, p) => And(e, p)())
 
-        val proofMethodBody: Stmt = simplifyStmts.execute(transformExp(pres, context))
+        val proofMethodBody: Stmt = Simplifier.simplify(transformExp(pres, context))
 
         if (proofMethodBody != EmptyStmt) {
           val proofMethod = Method(proofMethodName, f.formalArgs, Nil, Nil, Nil,
diff --git a/src/test/resources/termination/functions/expressions/access.vpr b/src/test/resources/termination/functions/expressions/access.vpr
new file mode 100644
index 000000000..9227fa31d
--- /dev/null
+++ b/src/test/resources/termination/functions/expressions/access.vpr
@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+field g: Int
+
+function test1(x: Ref): Bool
+    decreases
+    requires acc(x.f) && acc(x.g)
+{
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    nonTerminating(x)
+}
+
+function test2(x: Ref): Bool
+    decreases
+    requires acc(x.f) && acc(x.f) && acc(x.g)
+{
+    nonTerminating(x)
+}
+
+function nonTerminating(x: Ref): Bool
+    decreases *

From 1121e53debe2b4e33cd0583f57a30ebd00ecb7b6 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Fri, 21 Oct 2022 16:49:29 +0200
Subject: [PATCH 6/6] fixes unit tests for carbon

---
 .../termination/functions/expressions/unfolding.vpr         | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/src/test/resources/termination/functions/expressions/unfolding.vpr b/src/test/resources/termination/functions/expressions/unfolding.vpr
index 37569e073..b6eabf713 100644
--- a/src/test/resources/termination/functions/expressions/unfolding.vpr
+++ b/src/test/resources/termination/functions/expressions/unfolding.vpr
@@ -25,12 +25,6 @@ function test2(x: Ref): Bool
     unfolding foo(x) in partiallyTerminating(x)
 }
 
-function test3(x: Ref): Bool
-    decreases
-    requires foo(x)
-    // `unfolding` should indeed only temporarily unfold the predicate such that `nonTerminating(x)` is not reachable:
-    requires [true, (unfolding foo(x) in true) && (perm(x.f) > none ? nonTerminating(x) : true)]
-
 function nonTerminating(x: Ref): Bool
     decreases *