1 files changed, 52 insertions, 52 deletions
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl
index cb2fe89a..4acc862d 100644
--- a/Test/AbsHoudini/test10.bpl
+++ b/Test/AbsHoudini/test10.bpl
@@ -1,52 +1,52 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var sdv_7: int;
-var sdv_21: int;
-function {:existential true} b1(): bool;
-function{:existential true}  b2(): bool;
-function{:existential true}  b3(): bool;
-function{:existential true}  b4(): bool;
-
-procedure push(a:int)
-modifies sdv_7, sdv_21;
-{
-   sdv_21 := sdv_7;
-   sdv_7 := a;
-}
-
-procedure pop()
-modifies sdv_7, sdv_21;
-{
-   sdv_7 := sdv_21;
-   havoc sdv_21;
-}
-
-procedure foo()
-modifies sdv_7, sdv_21;
-requires {:candidate} b1() || (sdv_7 == 0);
-ensures{:candidate}  b2() || (sdv_7 == old(sdv_7));
-{
-   call push(2);
-   call pop();
-   call bar();
-}
-
-procedure bar()
-requires{:candidate} b3() || (sdv_7 == 0);
-ensures{:candidate}  b4() || (sdv_7 == old(sdv_7));
-modifies sdv_7, sdv_21;
-{
-   call push(1);
-   call pop();
-}
-
-procedure main()
-modifies sdv_7, sdv_21;
-{
-   sdv_7 := 0;
-   call foo();
-}
-
-// Expected: All false
-
-
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var sdv_7: int;
+var sdv_21: int;
+function {:existential true} b1(): bool;
+function{:existential true}  b2(): bool;
+function{:existential true}  b3(): bool;
+function{:existential true}  b4(): bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+   sdv_21 := sdv_7;
+   sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+   sdv_7 := sdv_21;
+   havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1() || (sdv_7 == 0);
+ensures{:candidate}  b2() || (sdv_7 == old(sdv_7));
+{
+   call push(2);
+   call pop();
+   call bar();
+}
+
+procedure bar()
+requires{:candidate} b3() || (sdv_7 == 0);
+ensures{:candidate}  b4() || (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+   call push(1);
+   call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+   sdv_7 := 0;
+   call foo();
+}
+
+// Expected: All false
+
+