Added test

viperproject · Jan 15, 2025 · 44dc671 · 44dc671
1 parent b02dc7c
commit 44dc671
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/src/test/resources/all/issues/silver/0833.vpr b/src/test/resources/all/issues/silver/0833.vpr
@@ -0,0 +1,9 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function gggg(a: Int): Int
+  decreases
+
+@opaque()
+function hhhh(a: Int): Int
+  decreases