summaryrefslogtreecommitdiff
path: root/Test/test0/Orderings.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test0/Orderings.bpl')
-rw-r--r--Test/test0/Orderings.bpl42
1 files changed, 21 insertions, 21 deletions
diff --git a/Test/test0/Orderings.bpl b/Test/test0/Orderings.bpl
index 0d55ed27..1cf900b6 100644
--- a/Test/test0/Orderings.bpl
+++ b/Test/test0/Orderings.bpl
@@ -1,22 +1,22 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-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
-
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+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