Merge pull request #737 from viperproject/meilers_fix_silicon_744

Adding test for Silicon issue #744
viperproject · Aug 21, 2023 · 56b74d1 · 56b74d1
2 parents 0f16c1f + c7d57c2
commit 56b74d1
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/src/test/resources/all/issues/silicon/0744.vpr b/src/test/resources/all/issues/silicon/0744.vpr
@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+function fac(i: Int): Int
+  ensures ge(result, 1)
+{
+  i <= 1 ? 1 : i * fac(i - 1)
+}
+
+function ge(i1: Int, i2: Int): Bool
+{
+  i1 >= i2
+}