Enable as many "og" lit tests. Several fail because they weren't

being executed previously!

    Boogie :: og/DeviceCacheSimplified.bpl
    Boogie :: og/DeviceCacheWithBuffer.bpl
    Boogie :: og/async.bpl
    Boogie :: og/houd1.bpl
    Boogie :: og/lock-introduced.bpl
    Boogie :: og/termination.bpl
    Boogie :: og/treiber-stack.bpl

48 files changed, 150 insertions, 21 deletions

diff --git a/Test/og/Answer b/Test/og/Answer
index b82acad4..4b1bceae 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,25 +1,25 @@
 

 -------------------- foo.bpl --------------------

-foo.bpl(28,3): Error: Non-interference check failed

+foo.bpl(30,3): Error: Non-interference check failed

 Execution trace:

-    foo.bpl(5,3): anon0

-    foo.bpl(5,3): anon0$1

-    foo.bpl(12,3): inline$Incr_1$0$this_A

+    foo.bpl(7,3): anon0

+    foo.bpl(7,3): anon0$1

+    foo.bpl(14,3): inline$Incr_1$0$this_A

     (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

 Boogie program verifier finished with 9 verified, 1 error

 

 -------------------- bar.bpl --------------------

-bar.bpl(26,3): Error: Non-interference check failed

+bar.bpl(28,3): Error: Non-interference check failed

 Execution trace:

-    bar.bpl(5,3): anon0

-    bar.bpl(5,3): anon0$1

-    bar.bpl(12,3): inline$Incr_1$0$this_A

+    bar.bpl(7,3): anon0

+    bar.bpl(7,3): anon0$1

+    bar.bpl(14,3): inline$Incr_1$0$this_A

     (0,0): inline$Impl_YieldChecker_PC_1$1$L0

-bar.bpl(26,3): Error: Non-interference check failed

+bar.bpl(28,3): Error: Non-interference check failed

 Execution trace:

-    bar.bpl(36,3): anon0

-    bar.bpl(36,3): anon0$1

+    bar.bpl(38,3): anon0

+    bar.bpl(38,3): anon0$1

     (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

 Boogie program verifier finished with 8 verified, 2 errors

@@ -29,11 +29,11 @@ Boogie program verifier finished with 8 verified, 2 errors
 Boogie program verifier finished with 3 verified, 0 errors

 

 -------------------- parallel1.bpl --------------------

-parallel1.bpl(28,3): Error: Non-interference check failed

+parallel1.bpl(30,3): Error: Non-interference check failed

 Execution trace:

-    parallel1.bpl(5,3): anon0

-    parallel1.bpl(5,3): anon0$1

-    parallel1.bpl(12,3): inline$Incr_1$0$this_A

+    parallel1.bpl(7,3): anon0

+    parallel1.bpl(7,3): anon0$1

+    parallel1.bpl(14,3): inline$Incr_1$0$this_A

     (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

 Boogie program verifier finished with 7 verified, 1 error

@@ -55,10 +55,10 @@ Boogie program verifier finished with 6 verified, 0 errors
 Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- parallel4.bpl --------------------

-parallel4.bpl(24,3): Error BP5001: This assertion might not hold.

+parallel4.bpl(26,3): Error BP5001: This assertion might not hold.

 Execution trace:

     (0,0): og_init

-    parallel4.bpl(22,5): anon0$1

+    parallel4.bpl(24,5): anon0$1

 

 Boogie program verifier finished with 5 verified, 1 error

 

@@ -71,13 +71,13 @@ Boogie program verifier finished with 8 verified, 0 errors
 Boogie program verifier finished with 6 verified, 0 errors

 

 -------------------- t1.bpl --------------------

-t1.bpl(58,5): Error: Non-interference check failed

+t1.bpl(60,5): Error: Non-interference check failed

 Execution trace:

     (0,0): og_init

-    t1.bpl(78,13): anon0

-    t1.bpl(78,13): anon0$1

+    t1.bpl(80,13): anon0

+    t1.bpl(80,13): anon0$1

     (0,0): inline$SetG_1$0$Entry

-    t1.bpl(78,13): anon0$2

+    t1.bpl(80,13): anon0$2

     (0,0): inline$Impl_YieldChecker_A_1$1$L2

 

 Boogie program verifier finished with 5 verified, 1 error

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 23f36ae5..59723dc8 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

diff --git a/Test/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect
new file mode 100644
index 00000000..11d204a8
--- /dev/null
+++ b/Test/og/DeviceCache.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 35 verified, 0 errors
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index 28e8b662..3365e565 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type X;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl
index f1da0ecf..a5252b87 100644
--- a/Test/og/DeviceCacheWithBuffer.bpl
+++ b/Test/og/DeviceCacheWithBuffer.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 2fddf217..4c664ec4 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type X;

 const nil: X;

 var {:phase 1} l: X;

diff --git a/Test/og/FlanaganQadeer.bpl.expect b/Test/og/FlanaganQadeer.bpl.expect
new file mode 100644
index 00000000..9823d44a
--- /dev/null
+++ b/Test/og/FlanaganQadeer.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index 90ccfebe..37bba956 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

diff --git a/Test/og/akash.bpl.expect b/Test/og/akash.bpl.expect
new file mode 100644
index 00000000..9823d44a
--- /dev/null
+++ b/Test/og/akash.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/og/async.bpl b/Test/og/async.bpl
index 4ca43d30..88307ba1 100644
--- a/Test/og/async.bpl
+++ b/Test/og/async.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} x: int;

 var {:phase 1} y: int;

 

diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 22751d29..26a4eb46 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} g:int;

 

 procedure {:yields} {:phase 1} PB()

diff --git a/Test/og/bar.bpl.expect b/Test/og/bar.bpl.expect
new file mode 100644
index 00000000..d59bd019
--- /dev/null
+++ b/Test/og/bar.bpl.expect
@@ -0,0 +1,13 @@
+bar.bpl(28,3): Error: Non-interference check failed
+Execution trace:
+    bar.bpl(7,3): anon0
+    bar.bpl(7,3): anon0$1
+    bar.bpl(14,3): inline$Incr_1$0$this_A
+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0
+bar.bpl(28,3): Error: Non-interference check failed
+Execution trace:
+    bar.bpl(38,3): anon0
+    bar.bpl(38,3): anon0$1
+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0
+
+Boogie program verifier finished with 8 verified, 2 errors
diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index 378bb8b5..9d82e229 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type X;

 const nil: X;

 

diff --git a/Test/og/civl-paper.bpl.expect b/Test/og/civl-paper.bpl.expect
new file mode 100644
index 00000000..812c54cc
--- /dev/null
+++ b/Test/og/civl-paper.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 28 verified, 0 errors
diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index 400f5a4e..ba05d666 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} g:int;

 

 procedure {:yields} {:phase 1} PB()

diff --git a/Test/og/foo.bpl.expect b/Test/og/foo.bpl.expect
new file mode 100644
index 00000000..b386f3f6
--- /dev/null
+++ b/Test/og/foo.bpl.expect
@@ -0,0 +1,8 @@
+foo.bpl(30,3): Error: Non-interference check failed
+Execution trace:
+    foo.bpl(7,3): anon0
+    foo.bpl(7,3): anon0$1
+    foo.bpl(14,3): inline$Incr_1$0$this_A
+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0
+
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Test/og/houd1.bpl b/Test/og/houd1.bpl
index aff53a48..03d52e54 100644
--- a/Test/og/houd1.bpl
+++ b/Test/og/houd1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 const {:existential true} b0: bool;

 const {:existential true} b1: bool;

 const {:existential true} b2: bool;

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 9effc04d..f6a4de75 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type X;

 function {:builtin "MapConst"} MapConstInt(int) : [X]int;

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

diff --git a/Test/og/linear-set.bpl.expect b/Test/og/linear-set.bpl.expect
new file mode 100644
index 00000000..00ddb38b
--- /dev/null
+++ b/Test/og/linear-set.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 36a8f9c7..dff4936c 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type X;

 function {:builtin "MapConst"} MapConstInt(int) : [X]int;

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

diff --git a/Test/og/linear-set2.bpl.expect b/Test/og/linear-set2.bpl.expect
new file mode 100644
index 00000000..00ddb38b
--- /dev/null
+++ b/Test/og/linear-set2.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl
index 928b3d00..f0825c14 100644
--- a/Test/og/lock-introduced.bpl
+++ b/Test/og/lock-introduced.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

 {

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 8357d36d..044cde1e 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 2} b: bool;

 

 procedure {:yields} {:phase 2} main()

diff --git a/Test/og/lock.bpl.expect b/Test/og/lock.bpl.expect
new file mode 100644
index 00000000..76a9a2bf
--- /dev/null
+++ b/Test/og/lock.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 9f5e0be8..2d1c53df 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 2} b: int;

 

 procedure {:yields} {:phase 2} main()

diff --git a/Test/og/lock2.bpl.expect b/Test/og/lock2.bpl.expect
new file mode 100644
index 00000000..76a9a2bf
--- /dev/null
+++ b/Test/og/lock2.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 459cb470..f0a2fd5b 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type X;

 

 const unique null : int;

diff --git a/Test/og/multiset.bpl.expect b/Test/og/multiset.bpl.expect
new file mode 100644
index 00000000..63682bb4
--- /dev/null
+++ b/Test/og/multiset.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 85 verified, 0 errors
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 6854e29c..a691c087 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;

 

 var {:phase 1} g:int;

diff --git a/Test/og/new1.bpl.expect b/Test/og/new1.bpl.expect
new file mode 100644
index 00000000..00ddb38b
--- /dev/null
+++ b/Test/og/new1.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 1da2f116..190a024a 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} x:int;

 

 procedure {:yields} {:phase 0,1} Set(v: int);

diff --git a/Test/og/one.bpl.expect b/Test/og/one.bpl.expect
new file mode 100644
index 00000000..a9949f2e
--- /dev/null
+++ b/Test/og/one.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index 427dc72d..90846b6c 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} g:int;

 

 procedure {:yields} {:phase 1} PB()

diff --git a/Test/og/parallel1.bpl.expect b/Test/og/parallel1.bpl.expect
new file mode 100644
index 00000000..5fc0cbf6
--- /dev/null
+++ b/Test/og/parallel1.bpl.expect
@@ -0,0 +1,8 @@
+parallel1.bpl(30,3): Error: Non-interference check failed
+Execution trace:
+    parallel1.bpl(7,3): anon0
+    parallel1.bpl(7,3): anon0$1
+    parallel1.bpl(14,3): inline$Incr_1$0$this_A
+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0
+
+Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 1bce7c8a..52c2e913 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} a:[int]int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

diff --git a/Test/og/parallel2.bpl.expect b/Test/og/parallel2.bpl.expect
new file mode 100644
index 00000000..76a9a2bf
--- /dev/null
+++ b/Test/og/parallel2.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 2a2feb2d..4bffcf94 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} a:int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect
new file mode 100644
index 00000000..7c696364
--- /dev/null
+++ b/Test/og/parallel4.bpl.expect
@@ -0,0 +1,6 @@
+parallel4.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    (0,0): og_init
+    parallel4.bpl(24,5): anon0$1
+
+Boogie program verifier finished with 5 verified, 1 error
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index a73af06e..5f0b30bf 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} a:[int]int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

diff --git a/Test/og/parallel5.bpl.expect b/Test/og/parallel5.bpl.expect
new file mode 100644
index 00000000..76a9a2bf
--- /dev/null
+++ b/Test/og/parallel5.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 6d07ca75..3f5adedd 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var {:phase 1} x: int;

 function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;

 

diff --git a/Test/og/perm.bpl.expect b/Test/og/perm.bpl.expect
new file mode 100644
index 00000000..00ddb38b
--- /dev/null
+++ b/Test/og/perm.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index c7e30dd9..c4964c0e 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect
new file mode 100644
index 00000000..9f9e44b1
--- /dev/null
+++ b/Test/og/t1.bpl.expect
@@ -0,0 +1,10 @@
+t1.bpl(60,5): Error: Non-interference check failed
+Execution trace:
+    (0,0): og_init
+    t1.bpl(80,13): anon0
+    t1.bpl(80,13): anon0$1
+    (0,0): inline$SetG_1$0$Entry
+    t1.bpl(80,13): anon0$2
+    (0,0): inline$Impl_YieldChecker_A_1$1$L2
+
+Boogie program verifier finished with 5 verified, 1 error
diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl
index 80109bf4..a7969e7c 100644
--- a/Test/og/termination.bpl
+++ b/Test/og/termination.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 procedure {:yields} X();

 ensures {:atomic 0} |{ A: return true; }|;

 

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index fb347935..3ee7485b 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 function RightOpen(n: int) : [int]bool;

 function RightClosed(n: int) : [int]bool;

 axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);

diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect
new file mode 100644
index 00000000..812c54cc
--- /dev/null
+++ b/Test/og/ticket.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 28 verified, 0 errors
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 6e87d8f3..e082c4ca 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 type Node;

 type lmap;

 function {:linear "Node"} dom(lmap): [Node]bool;