Test for Silicon issue 410

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

@@ -45,4 +45,23 @@ method bar(x: Ref)
     }
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert false
+}
+
+
+field fx: Int
+field fy: Int
+
+method unsound(a: Ref)
+requires acc(a.fx) && acc(a.fy)
+ensures false
+{
+    package acc(a.fx) --* (acc(a.fx) && acc(a.fy))
+
+    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.fx) // shouldn't hold as we should have zero permissions
 }

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)
+}