Adding test for Carbon issue #420 (#845)

viperproject · Feb 11, 2025 · dbb955d · dbb955d
1 parent e41ab2b
commit dbb955d
Showing 1 changed file with 21 additions and 0 deletions.
diff --git a/src/test/resources/all/issues/carbon/0420.vpr b/src/test/resources/all/issues/carbon/0420.vpr
@@ -0,0 +1,21 @@
+// Any copyright is dedicated to the Public Domain.^M
+// http://creativecommons.org/publicdomain/zero/1.0/^M
+
+domain MyInt {
+  function succ(n: MyInt): MyInt
+  function pred(n: MyInt): MyInt
+
+  axiom ps{
+    forall n:MyInt ::
+      { pred(succ(n)) }
+        pred(succ(n)) == n
+  }
+}
+
+method test(n: MyInt, m: MyInt)
+requires succ(n) == succ(m)
+ensures n == m {
+  if (pred(succ(n)) != n) {
+
+  }
+}