diff --git a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
index 622ead204..39381eb8b 100644
--- 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
new file mode 100644
index 000000000..948d44660
--- /dev/null
+++ 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()
+}
\ No newline at end of file