Initial set of files.

1 files changed, 20 insertions, 0 deletions

diff --git a/Test/test0/Orderings.bpl b/Test/test0/Orderings.bpl
new file mode 100644
index 00000000..0ba6c69c
--- /dev/null
+++ b/Test/test0/Orderings.bpl
@@ -0,0 +1,20 @@
+

+type C;

+

+const c:int extends a;

+const d:int extends a complete;

+const e:int extends unique a, b;

+const f:int extends complete;

+

+const a:int;

+const b:int;

+

+const g:int extends x;        // error: undeclared parent

+

+const c0:C;

+const c1:C extends c0, c0;    // error: parent mentioned twice

+const c2:C extends c2;        // error: constant as its own parent

+

+const h:int extends y;        // error: variable cannot be parent

+

+var y:int;
\ No newline at end of file