summaryrefslogtreecommitdiff
path: root/Test/linear/bug.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/linear/bug.bpl')
-rw-r--r--Test/linear/bug.bpl32
1 files changed, 16 insertions, 16 deletions
diff --git a/Test/linear/bug.bpl b/Test/linear/bug.bpl
index 9177e2ca..4757b5b9 100644
--- a/Test/linear/bug.bpl
+++ b/Test/linear/bug.bpl
@@ -1,16 +1,16 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
-function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }
-
-var {:linear ""} g:int;
-
-procedure A()
-{
-}
-
-procedure B()
-{
- call A();
- assert false;
-}
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }
+
+var {:linear ""} g:int;
+
+procedure A()
+{
+}
+
+procedure B()
+{
+ call A();
+ assert false;
+}