From 6ddaa1b33e78876b73f7eb8cc05092dc09d46bf9 Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Mon, 30 Dec 2024 16:15:57 +0100
Subject: [PATCH] Test for Carbon issue #391 (#829)

---
 src/test/resources/all/issues/carbon/0391.vpr  | 18 ++++++++++++++++++
 src/test/resources/all/issues/silicon/0595.vpr |  1 -
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 src/test/resources/all/issues/carbon/0391.vpr

diff --git a/src/test/resources/all/issues/carbon/0391.vpr b/src/test/resources/all/issues/carbon/0391.vpr
new file mode 100644
index 000000000..a82559224
--- /dev/null
+++ b/src/test/resources/all/issues/carbon/0391.vpr
@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+predicate p()
+
+method mmmm()
+{
+ //:: ExpectedOutput(exhale.failed:qp.not.injective)
+ //:: ExpectedOutput(exhale.failed:insufficient.permission)
+ //:: MissingOutput(exhale.failed:insufficient.permission, /silicon/issue/34/)
+ exhale forall i: Int :: p()
+}
+
+method mmmm2()
+{
+ //:: ExpectedOutput(inhale.failed:qp.not.injective)
+ inhale forall i: Int :: p()
+}
\ No newline at end of file
diff --git a/src/test/resources/all/issues/silicon/0595.vpr b/src/test/resources/all/issues/silicon/0595.vpr
index 7105b18a1..852e47845 100644
--- a/src/test/resources/all/issues/silicon/0595.vpr
+++ b/src/test/resources/all/issues/silicon/0595.vpr
@@ -7,7 +7,6 @@ predicate P()
 
 method test()
   requires P()
-   //:: IgnoreFile(/carbon/issue/391/)
   ensures forall i: Int :: i == 0 ==> P()
 {}