Merge remote-tracking branch 'mine/format-rnode' into format-rnode

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 {

src/test/resources/all/issues/silicon/0883.vpr

@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+
+@moreJoins("2")
+method foo(x: Ref, xs: Set[Ref])
+    requires forall r: Ref :: { r in xs } r in xs ==> acc(r.f)
+{
+    var b: Bool
+    inhale acc(x.f, 1/2)
+    if (b) {
+        inhale acc(x.f, 1/2)
+    } else {
+        inhale acc(x.f, 1/2)
+    }
+
+    assert acc(x.f)
+}

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]