Merge pull request #718 from viperproject/meilers_fix_717

Fixing issue #717
viperproject · Jul 8, 2023 · 2e9bffc · 2e9bffc
2 parents 64016f1 + d12c26e
commit 2e9bffc
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
@@ -63,7 +63,7 @@ object ImpureAssumeRewriter {
         val insideWand = c.ancestorList.foldLeft[Boolean](false)((b, n) => b || n.isInstanceOf[MagicWand])
         val dummyVars = (LazyList.from(0) map (i => placeholderVar(i, pred.loc.loc(program).formalArgs(i).typ))) take pred.loc.args.length
         val eqs = (pred.loc.args zip dummyVars) map (a => EqCmp(a._1, a._2)())
-        val cond = eqs.tail.foldLeft[Exp](eqs.head)((a, e) => And(a,e)())
+        val cond = if (eqs.isEmpty) TrueLit()() else eqs.tail.foldLeft[Exp](eqs.head)((a, e) => And(a,e)())
         val newCtxFrame =  ((And(c.c, cond)(), dummyVars), pred.perm)
         val oldCtxFrames = collCont.getOrElse(pred.loc.loc(program), Seq())
         collCont += (pred.loc.loc(program) -> (oldCtxFrames :+ newCtxFrame))

diff --git a/src/test/resources/all/issues/silver/0717.vpr b/src/test/resources/all/issues/silver/0717.vpr
@@ -0,0 +1,8 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+predicate p()
+
+method client() {
+    assume p()
+}