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 cb028f3ac..ba2e09119 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
@@ -98,7 +98,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
 
         if (proofMethodBody != EmptyStmt) {
           val proofMethod = Method(proofMethodName, f.formalArgs, Nil, f.pres, Nil,
-            Option(Seqn(Seq(proofMethodBody), Seq(resultVariable))()))(info = f.info)
+            Option(Seqn(Seq(proofMethodBody), Seq(resultVariable, context.conditionInEx.get))()))(info = f.info)
 
           Seq(proofMethod)
         } else {
diff --git a/src/test/resources/all/issues/silicon/0883.vpr b/src/test/resources/all/issues/silicon/0883.vpr
index cb06b8d63..4992b7476 100644
--- a/src/test/resources/all/issues/silicon/0883.vpr
+++ b/src/test/resources/all/issues/silicon/0883.vpr
@@ -1,3 +1,7 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
 field f: Int
 
 @moreJoins("2")
diff --git a/src/test/resources/all/issues/silicon/0886.vpr b/src/test/resources/all/issues/silicon/0886.vpr
new file mode 100644
index 000000000..c0a9fd59c
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0886.vpr
@@ -0,0 +1,10 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+function foo(): Bool
+  decreases
+
+function bar(): Int
+  decreases
+  ensures [foo(), true]