Fix lit test suite when running Boogie under a path that contains

spaces.

40 files changed, 240 insertions, 240 deletions

diff --git a/Test/test21/BooleanQuantification.bpl b/Test/test21/BooleanQuantification.bpl
index 527ab174..1493269b 100644
--- a/Test/test21/BooleanQuantification.bpl
+++ b/Test/test21/BooleanQuantification.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 

diff --git a/Test/test21/BooleanQuantification2.bpl b/Test/test21/BooleanQuantification2.bpl
index 73234024..22dfd217 100644
--- a/Test/test21/BooleanQuantification2.bpl
+++ b/Test/test21/BooleanQuantification2.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 axiom (forall x:bool :: x || !x);

diff --git a/Test/test21/Boxing.bpl b/Test/test21/Boxing.bpl
index 00e3013e..0112b6cf 100644
--- a/Test/test21/Boxing.bpl
+++ b/Test/test21/Boxing.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 type Box;

 

diff --git a/Test/test21/Casts.bpl b/Test/test21/Casts.bpl
index 1320cff2..739185ea 100644
--- a/Test/test21/Casts.bpl
+++ b/Test/test21/Casts.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 procedure P() returns () {

diff --git a/Test/test21/Coercions2.bpl b/Test/test21/Coercions2.bpl
index 849376f5..e9a78574 100644
--- a/Test/test21/Coercions2.bpl
+++ b/Test/test21/Coercions2.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 type Box, C;

diff --git a/Test/test21/Colors.bpl b/Test/test21/Colors.bpl
index 7e63c9ff..f0e12672 100644
--- a/Test/test21/Colors.bpl
+++ b/Test/test21/Colors.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 type Color;

diff --git a/Test/test21/DisjointDomains.bpl b/Test/test21/DisjointDomains.bpl
index 303d0e4f..30d8a6f7 100644
--- a/Test/test21/DisjointDomains.bpl
+++ b/Test/test21/DisjointDomains.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 type C _;

 

 function f<a>(C a) returns (int);

diff --git a/Test/test21/DisjointDomains2.bpl b/Test/test21/DisjointDomains2.bpl
index 8677d9dc..ae25a20e 100644
--- a/Test/test21/DisjointDomains2.bpl
+++ b/Test/test21/DisjointDomains2.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 type C _;

 

 function f<a>(C a) returns (int);

diff --git a/Test/test21/EmptyList.bpl b/Test/test21/EmptyList.bpl
index 28362b73..450cd064 100644
--- a/Test/test21/EmptyList.bpl
+++ b/Test/test21/EmptyList.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 type List _;

diff --git a/Test/test21/EmptySetBug.bpl b/Test/test21/EmptySetBug.bpl
index 06a42652..e3feb16c 100644
--- a/Test/test21/EmptySetBug.bpl
+++ b/Test/test21/EmptySetBug.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 type ref;

 

 const null: ref;

diff --git a/Test/test21/Flattening.bpl b/Test/test21/Flattening.bpl
index 4ef7e5c8..ddebd9ab 100644
--- a/Test/test21/Flattening.bpl
+++ b/Test/test21/Flattening.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 function g(int) returns (int);

diff --git a/Test/test21/FunAxioms.bpl b/Test/test21/FunAxioms.bpl
index c51024ad..5964b4e8 100644
--- a/Test/test21/FunAxioms.bpl
+++ b/Test/test21/FunAxioms.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 type Pair a b;

diff --git a/Test/test21/FunAxioms2.bpl b/Test/test21/FunAxioms2.bpl
index 3b9bccf2..6e087baf 100644
--- a/Test/test21/FunAxioms2.bpl
+++ b/Test/test21/FunAxioms2.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 type T;

 

diff --git a/Test/test21/HeapAbstraction.bpl b/Test/test21/HeapAbstraction.bpl
index 6f88189c..0fb2f007 100644
--- a/Test/test21/HeapAbstraction.bpl
+++ b/Test/test21/HeapAbstraction.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 type Field a, Heap = <a>[ref, Field a]a;

diff --git a/Test/test21/HeapAxiom.bpl b/Test/test21/HeapAxiom.bpl
index adb3f632..691c97f9 100644
--- a/Test/test21/HeapAxiom.bpl
+++ b/Test/test21/HeapAxiom.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 type Field a, Heap = <a>[ref, Field a]a;

diff --git a/Test/test21/InterestingExamples0.bpl b/Test/test21/InterestingExamples0.bpl
index d3021553..08ed61d4 100644
--- a/Test/test21/InterestingExamples0.bpl
+++ b/Test/test21/InterestingExamples0.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 procedure P() returns () {

 var a : <t>[t]int;

diff --git a/Test/test21/InterestingExamples1.bpl b/Test/test21/InterestingExamples1.bpl
index a530c625..247e2c5b 100644
--- a/Test/test21/InterestingExamples1.bpl
+++ b/Test/test21/InterestingExamples1.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 type Set = <a> [a] bool;

 type Field a;

diff --git a/Test/test21/InterestingExamples2.bpl b/Test/test21/InterestingExamples2.bpl
index fd17b122..6fc8d259 100644
--- a/Test/test21/InterestingExamples2.bpl
+++ b/Test/test21/InterestingExamples2.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 procedure P() returns () {

diff --git a/Test/test21/InterestingExamples3.bpl b/Test/test21/InterestingExamples3.bpl
index 3acca9a1..24e89b2b 100644
--- a/Test/test21/InterestingExamples3.bpl
+++ b/Test/test21/InterestingExamples3.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 procedure P() returns () {

 

diff --git a/Test/test21/InterestingExamples4.bpl b/Test/test21/InterestingExamples4.bpl
index db2e9682..941c9020 100644
--- a/Test/test21/InterestingExamples4.bpl
+++ b/Test/test21/InterestingExamples4.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 // a property that should hold according to the Boogie semantics

 // (but no automatic theorem prover will be able to prove it)

 

diff --git a/Test/test21/InterestingExamples5.bpl b/Test/test21/InterestingExamples5.bpl
index be388839..3f4e4f34 100644
--- a/Test/test21/InterestingExamples5.bpl
+++ b/Test/test21/InterestingExamples5.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 type C a;

diff --git a/Test/test21/Keywords.bpl b/Test/test21/Keywords.bpl
index 9af526e4..3be91fa8 100644
--- a/Test/test21/Keywords.bpl
+++ b/Test/test21/Keywords.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 function NOT(x:int) returns(int);

diff --git a/Test/test21/LargeLiterals0.bpl b/Test/test21/LargeLiterals0.bpl
index 203e9bc5..57877f9d 100644
--- a/Test/test21/LargeLiterals0.bpl
+++ b/Test/test21/LargeLiterals0.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 var x : int;

diff --git a/Test/test21/LetSorting.bpl b/Test/test21/LetSorting.bpl
index 38e77396..c58c6242 100644
--- a/Test/test21/LetSorting.bpl
+++ b/Test/test21/LetSorting.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 procedure Array0() returns (z: int)

diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl
index 66e7a142..4c8302a4 100644
--- a/Test/test21/MapAxiomsConsistency.bpl
+++ b/Test/test21/MapAxiomsConsistency.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 // Dafny program verifier version 0.92, Copyright (c) 2003-2008, Microsoft.

 // Command Line Options: /trace /typeEncoding:arguments /print:test.bpl test.dfy

 

diff --git a/Test/test21/MapOutputTypeParams.bpl b/Test/test21/MapOutputTypeParams.bpl
index 4e83e6f1..c9304d34 100644
--- a/Test/test21/MapOutputTypeParams.bpl
+++ b/Test/test21/MapOutputTypeParams.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 

diff --git a/Test/test21/Maps0.bpl b/Test/test21/Maps0.bpl
index ba3a0f98..125730ef 100644
--- a/Test/test21/Maps0.bpl
+++ b/Test/test21/Maps0.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 const a : [int] bool;

diff --git a/Test/test21/Maps1.bpl b/Test/test21/Maps1.bpl
index 417521eb..024cd50f 100644
--- a/Test/test21/Maps1.bpl
+++ b/Test/test21/Maps1.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 // different map type classes with the same arity

diff --git a/Test/test21/Maps2.bpl b/Test/test21/Maps2.bpl
index ea020afd..0b7980c7 100644
--- a/Test/test21/Maps2.bpl
+++ b/Test/test21/Maps2.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 // XFAIL: *

 

 type T;

diff --git a/Test/test21/NameClash.bpl b/Test/test21/NameClash.bpl
index 9b6fefa8..d31a6e01 100644
--- a/Test/test21/NameClash.bpl
+++ b/Test/test21/NameClash.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 function f(int) returns (int);

diff --git a/Test/test21/Orderings.bpl b/Test/test21/Orderings.bpl
index 6a048224..39361461 100644
--- a/Test/test21/Orderings.bpl
+++ b/Test/test21/Orderings.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 const a, b:int;

diff --git a/Test/test21/Orderings2.bpl b/Test/test21/Orderings2.bpl
index fe01184c..01d3be15 100644
--- a/Test/test21/Orderings2.bpl
+++ b/Test/test21/Orderings2.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 const b:int;

diff --git a/Test/test21/Orderings3.bpl b/Test/test21/Orderings3.bpl
index a842be12..3036d8e6 100644
--- a/Test/test21/Orderings3.bpl
+++ b/Test/test21/Orderings3.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 // Example from the Boogie 2 language report

 

 

diff --git a/Test/test21/Orderings4.bpl b/Test/test21/Orderings4.bpl
index 62f7b7fa..00da92dc 100644
--- a/Test/test21/Orderings4.bpl
+++ b/Test/test21/Orderings4.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 type Wicket;

diff --git a/Test/test21/ParallelAssignment.bpl b/Test/test21/ParallelAssignment.bpl
index 6bd414e9..6f7c7639 100644
--- a/Test/test21/ParallelAssignment.bpl
+++ b/Test/test21/ParallelAssignment.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 // Examples from the Boogie2 language report

 

 type C, D;

diff --git a/Test/test21/PolyList.bpl b/Test/test21/PolyList.bpl
index c68c637e..08fcd637 100644
--- a/Test/test21/PolyList.bpl
+++ b/Test/test21/PolyList.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 

diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl
index 42b1f889..eb140f77 100644
--- a/Test/test21/Real.bpl
+++ b/Test/test21/Real.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 axiom (forall r: real :: r == 0.0 || r / r == 1.0);

 

 procedure P(a: real, b: real) returns () {

diff --git a/Test/test21/Triggers0.bpl b/Test/test21/Triggers0.bpl
index f58b168f..c3ff14d5 100644
--- a/Test/test21/Triggers0.bpl
+++ b/Test/test21/Triggers0.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 const ar : [int]bool;

diff --git a/Test/test21/Triggers1.bpl b/Test/test21/Triggers1.bpl
index 63a780f5..a4199040 100644
--- a/Test/test21/Triggers1.bpl
+++ b/Test/test21/Triggers1.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 

 

 

diff --git a/Test/test21/test3_AddMethod_conv.bpl b/Test/test21/test3_AddMethod_conv.bpl
index d0abb5c3..89c34c45 100644
--- a/Test/test21/test3_AddMethod_conv.bpl
+++ b/Test/test21/test3_AddMethod_conv.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t

-// RUN: %diff %s.n.expect %t

-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t

-// RUN: %diff %s.p.expect %t

-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t

-// RUN: %diff %s.a.expect %t

+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"

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

+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"

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

 // XFAIL: *

 // Spec# program verifier version 0.90, Copyright (c) 2003-2008, Microsoft.

 // Command Line Options: /print:debug.txt AddMethod.dll