summaryrefslogtreecommitdiff
path: root/Test/smoke/smoke0.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/smoke/smoke0.bpl')
-rw-r--r--Test/smoke/smoke0.bpl110
1 files changed, 55 insertions, 55 deletions
diff --git a/Test/smoke/smoke0.bpl b/Test/smoke/smoke0.bpl
index 87531c8d..6c4c8167 100644
--- a/Test/smoke/smoke0.bpl
+++ b/Test/smoke/smoke0.bpl
@@ -1,55 +1,55 @@
-// RUN: %boogie -smoke "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure a(x:int)
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- } else {
- y := 2;
- }
-}
-
-
-procedure b(x:int)
- requires x>0;
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- } else {
- y := 2;
- }
-}
-
-
-
-procedure c(x:int)
- requires x>0;
-{
- var y : int;
-
- if(x<0) {
- y := 1;
- assert false;
- } else {
- y := 2;
- }
-}
-
-procedure d(x:int)
- requires x>0;
-{
- var y : int;
-
- if(x<0) {
- assert false;
- y := 1;
- } else {
- y := 2;
- }
-}
-
-
+// RUN: %boogie -smoke "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure a(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+
+procedure b(x:int)
+ requires x>0;
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+
+
+procedure c(x:int)
+ requires x>0;
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ assert false;
+ } else {
+ y := 2;
+ }
+}
+
+procedure d(x:int)
+ requires x>0;
+{
+ var y : int;
+
+ if(x<0) {
+ assert false;
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+