From 170ed858c33268201d75bbd03c4ecdf93a119c40 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Wed, 12 Feb 2025 16:16:36 +0100
Subject: [PATCH 1/2] Test for Silicon issues 410 and the new example from 338

---
 .../resources/all/issues/silicon/0338.vpr     | 19 ++++++++++
 .../resources/all/issues/silicon/0410.vpr     | 35 +++++++++++++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 src/test/resources/all/issues/silicon/0410.vpr

diff --git a/src/test/resources/all/issues/silicon/0338.vpr b/src/test/resources/all/issues/silicon/0338.vpr
index 7da5843bd..b8f140d65 100644
--- a/src/test/resources/all/issues/silicon/0338.vpr
+++ b/src/test/resources/all/issues/silicon/0338.vpr
@@ -45,4 +45,23 @@ method bar(x: Ref)
     }
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert false
+}
+
+
+field x: Int
+field y: Int
+
+method unsound(a: Ref)
+requires acc(a.x) && acc(a.y)
+ensures false
+{
+    package acc(a.x) --* (acc(a.x) && acc(a.y))
+
+    package acc(a.x) --* (acc(a.x) && acc(a.y)) {
+        assert acc(a.x, 2/1)
+        assert false // necessary to trigger unsoundness
+    }
+
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    assert acc(a.x) // shouldn't hold as we should have zero permissions
 }
\ No newline at end of file
diff --git a/src/test/resources/all/issues/silicon/0410.vpr b/src/test/resources/all/issues/silicon/0410.vpr
new file mode 100644
index 000000000..db723504a
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0410.vpr
@@ -0,0 +1,35 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field data: Int
+field f: Int
+
+
+method foo1(x: Ref)
+    requires acc(x.data)
+{
+    package acc(x.data) --* false {
+        assert acc(x.data) && acc(x.data)
+        assert false
+    }
+
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    assert acc(x.data)
+}
+
+
+
+method foo2(x: Ref)
+    requires acc(x.data)
+{
+
+    var y: Int
+    package acc(x.data) --* false {
+        assert acc(x.data) && acc(x.data)
+        assert x.f > 0
+    }
+
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    assert acc(x.data)
+}
\ No newline at end of file

From 9e1e6de918aa586ddd3a6b8a035d4c42db6ec369 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Wed, 12 Feb 2025 16:42:44 +0100
Subject: [PATCH 2/2] Fixed added test method

---
 src/test/resources/all/issues/silicon/0338.vpr | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/test/resources/all/issues/silicon/0338.vpr b/src/test/resources/all/issues/silicon/0338.vpr
index b8f140d65..7a17c8c09 100644
--- a/src/test/resources/all/issues/silicon/0338.vpr
+++ b/src/test/resources/all/issues/silicon/0338.vpr
@@ -48,20 +48,20 @@ method bar(x: Ref)
 }
 
 
-field x: Int
-field y: Int
+field fx: Int
+field fy: Int
 
 method unsound(a: Ref)
-requires acc(a.x) && acc(a.y)
+requires acc(a.fx) && acc(a.fy)
 ensures false
 {
-    package acc(a.x) --* (acc(a.x) && acc(a.y))
+    package acc(a.fx) --* (acc(a.fx) && acc(a.fy))
 
-    package acc(a.x) --* (acc(a.x) && acc(a.y)) {
-        assert acc(a.x, 2/1)
+    package acc(a.fx) --* (acc(a.fx) && acc(a.fy)) {
+        assert acc(a.fx, 2/1)
         assert false // necessary to trigger unsoundness
     }
 
     //:: ExpectedOutput(assert.failed:insufficient.permission)
-    assert acc(a.x) // shouldn't hold as we should have zero permissions
+    assert acc(a.fx) // shouldn't hold as we should have zero permissions
 }
\ No newline at end of file