From 87adb0170f77c846285877407f1ef53fa4165edb Mon Sep 17 00:00:00 2001
From: gauravpartha <gaurav.parthasarathy@inf.ethz.ch>
Date: Tue, 25 Apr 2023 11:50:02 +0200
Subject: [PATCH 1/3] add UnexpectedOutput to example with permission
 introspection inside unfolding expression (connected to Carbon PR #457)

---
 src/test/resources/all/issues/carbon/0213.vpr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/test/resources/all/issues/carbon/0213.vpr b/src/test/resources/all/issues/carbon/0213.vpr
index d84404e21..944af41fd 100644
--- a/src/test/resources/all/issues/carbon/0213.vpr
+++ b/src/test/resources/all/issues/carbon/0213.vpr
@@ -11,5 +11,6 @@ method test(r:Ref)
   requires P(r)
   {
       assert perm(r.next) == none
+      //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/213/)
       assert (unfolding P(r) in perm(r.next) == write)
   }
\ No newline at end of file

From 8398cbde036c51accdbd10ea307b6e3d597c1c44 Mon Sep 17 00:00:00 2001
From: gauravpartha <gaurav.parthasarathy@inf.ethz.ch>
Date: Tue, 25 Apr 2023 11:51:06 +0200
Subject: [PATCH 2/3] add a test that checks permission introspection inside
 exhale statements

---
 src/test/resources/all/issues/carbon/0406.vpr | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 src/test/resources/all/issues/carbon/0406.vpr

diff --git a/src/test/resources/all/issues/carbon/0406.vpr b/src/test/resources/all/issues/carbon/0406.vpr
new file mode 100644
index 000000000..acca4a184
--- /dev/null
+++ b/src/test/resources/all/issues/carbon/0406.vpr
@@ -0,0 +1,24 @@
+field f: Ref
+
+method m1() {
+    var y: Ref
+    var z: Ref
+    inhale acc(y.f) && acc(z.f)
+    exhale acc(y.f) && forperm x: Ref [x.f] :: x != z ==> 0/0 == 0/0
+}
+
+method m2() {
+    var x: Ref
+
+    inhale acc(x.f)
+
+    //:: ExpectedOutput(exhale.failed:division.by.zero)
+    exhale acc(x.f) && (perm(x.f) == none ==> 0/0 == 0/0)
+}
+
+method m3() {
+    var x: Ref
+
+    inhale acc(x.f)
+    exhale acc(x.f) && (perm(x.f) != none ==> 0/0 == 0/0)
+}
\ No newline at end of file

From 1383e0fb2d9e8dbb2af1404683af309ba5d7e279 Mon Sep 17 00:00:00 2001
From: gauravpartha <gaurav.parthasarathy@inf.ethz.ch>
Date: Tue, 25 Apr 2023 11:51:43 +0200
Subject: [PATCH 3/3] disable linked-list with predicates example, since it
 does not seem to reliably terminate on the CI for Carbon

---
 .../resources/examples/vmcai2016/linked-list-predicates.vpr     | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/test/resources/examples/vmcai2016/linked-list-predicates.vpr b/src/test/resources/examples/vmcai2016/linked-list-predicates.vpr
index bc37467e9..2343d1e38 100644
--- a/src/test/resources/examples/vmcai2016/linked-list-predicates.vpr
+++ b/src/test/resources/examples/vmcai2016/linked-list-predicates.vpr
@@ -1,6 +1,8 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
+//:: IgnoreFile(/carbon/issue/280/)
+
 /*****************************************************************
  * List Nodes
  *****************************************************************/