From 2c71dc1ae81eb6710e3f4feaf3d393afe1da4b60 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Sat, 1 Feb 2025 18:05:40 +0100
Subject: [PATCH] Test for Silicon issue 892

---
 .../resources/all/issues/silicon/0892.vpr     | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 src/test/resources/all/issues/silicon/0892.vpr

diff --git a/src/test/resources/all/issues/silicon/0892.vpr b/src/test/resources/all/issues/silicon/0892.vpr
new file mode 100644
index 000000000..2e957cb7b
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0892.vpr
@@ -0,0 +1,23 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+predicate P(r: Ref) {
+  Q(r) &&
+  unfolding Q(r) in true
+}
+
+predicate Q(r: Ref) {true}
+
+predicate R(r: Ref) {
+  P(r) && unfolding P(r) in true
+}
+
+method test01(r: Ref) returns ()
+  requires P(r)
+{
+  fold acc(R(r), wildcard)
+
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
\ No newline at end of file