Changed ranking function for Seq, so that it's compatible with data types.

1 files changed, 31 insertions, 0 deletions

diff --git a/Test/dafny0/RankNeg.dfy b/Test/dafny0/RankNeg.dfy
new file mode 100644
index 00000000..39e7630d
--- /dev/null
+++ b/Test/dafny0/RankNeg.dfy
@@ -0,0 +1,31 @@
+// Negative tests

+

+// Not well-founded mutual recursions.

+

+function seq_loop_i(xs: seq<int>): int

+{

+  if (xs == [1, 2]) then seq_loop_s([[1,2]])

+  else 0

+}

+function seq_loop_s(xs: seq<seq<int>>): int

+{

+  if (xs == [[1, 2]]) then seq_loop_i([1,2])

+  else 0

+}

+

+datatype wrap = X | WS(ds: seq<wrap>);

+function wrap_loop_1(xs: seq<wrap>): int

+{

+  if (xs == [WS([X,X])]) then wrap_loop_2(WS([X,X]))

+  else 0

+}

+function wrap_loop_2(xs: wrap): int

+{

+  if (xs == WS([X,X])) then wrap_loop_3([X,X])

+  else 0

+}

+function wrap_loop_3(xs: seq<wrap>): int

+{

+  if (xs == [X,X]) then wrap_loop_1([WS([X,X])])

+  else 0

+}