Avoiding folds in the encoding of unfolding expressions (#773)

* Avoiding folds in the encoding of unfolding expressions * Removed outdated comment * Fixed missing variable declaration --------- Co-authored-by: João Pereira <[email protected]>
viperproject · Feb 19, 2024 · 12076ff · 12076ff
1 parent 5bf505f
commit 12076ff
Showing 1 changed file with 6 additions and 5 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
@@ -57,11 +57,12 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
     case Unfolding(acc, unfBody) =>
       val permCheck = transformExp(acc.perm, c, false)
       val unfoldBody = transformExp(unfBody, c, inhaleExp)
-      // only unfold and fold if body contains something
-      val (unfold, fold) = (Unfold(acc)(), Fold(acc)())
-
-      val stmts = Seq(permCheck, unfold, unfoldBody, fold)
-      Seqn(stmts, Nil)()
+      val unfold = Unfold(acc)()
+      val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT)
+      val assumeFalse = Inhale(FalseLit()())()
+      val thenBranch = Seqn(Seq(permCheck, unfold, unfoldBody, assumeFalse), Nil)()
+      val elseBranch = if (inhaleExp) Seqn(Seq(Inhale(e)(e.pos, e.info)), Nil)() else EmptyStmt
+      Seqn(Seq(If(nonDetVarDecl.localVar, thenBranch, elseBranch)()), Seq(nonDetVarDecl))()
     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)