From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Test/AbsHoudini/test9.bpl | 184 +++++++++++++++++++++++-----------------------
 1 file changed, 92 insertions(+), 92 deletions(-)

(limited to 'Test/AbsHoudini/test9.bpl')

diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl
index 7d624167..9e7778eb 100644
--- a/Test/AbsHoudini/test9.bpl
+++ b/Test/AbsHoudini/test9.bpl
@@ -1,92 +1,92 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var v1: int;
-var v2: int;
-var v3: int;
-function{:existential true} b1(): bool;
-function{:existential true} b2(): bool;
-function{:existential true} b3(): bool;
-function{:existential true} b4(): bool;
-function{:existential true} b5(): bool;
-function{:existential true} b6(): bool;
-function{:existential true} b7(): bool;
-function{:existential true} b8(): bool;
-function{:existential true} b9(): bool;
-function{:existential true} b10(): bool;
-function{:existential true} b11(): bool;
-function{:existential true} b12(): bool;
-function{:existential true} b13(): bool;
-function{:existential true} b14(): bool;
-function{:existential true} b15(): bool;
-function{:existential true} b16(): bool;
-
-procedure push() 
-requires {:candidate} b1() || v1 == 0;
-requires {:candidate} b2() || v1 == 1;
-ensures  {:candidate} b3() || v1 == 0;
-ensures {:candidate}  b4() || v1 == 1;
-modifies v1,v2;
-{
-   v2 := v1;
-   v1 := 1;
-}
-
-procedure pop()
-modifies v1,v2;
-requires {:candidate} b5() || v1 == 0;
-requires {:candidate} b6() || v1 == 1;
-ensures  {:candidate} b7() || v1 == 0;
-ensures {:candidate}  b8() || v1 == 1;
-{
-   v1 := v2;
-   havoc v2;
-}
-
-procedure foo() 
-modifies v1,v2;
-requires {:candidate} b9() || v1 == 0;
-requires {:candidate} b10() || v1 == 1;
-ensures  {:candidate} b11() || v1 == 0;
-ensures {:candidate}  b12() || v1 == 1;
-{
-   call push();
-   call pop();
-}
-
-procedure bar()
-modifies v1,v2;
-requires {:candidate} b13() || v1 == 0;
-requires {:candidate} b14() || v1 == 1;
-ensures  {:candidate} b15() || v1 == 0;
-ensures {:candidate}  b16() || v1 == 1;
-{
-   call push();
-   call pop();
-}
-
-procedure main() 
-modifies v1,v2;
-{
-   v1 := 1;
-   call foo();
-   havoc v1;
-   call bar();
-}
-
-// Expected:
-//b1 = true
-//b2 = true
-//b3 = true
-//b4 = false
-//b5 = true
-//b6 = false
-//b7 = true
-//b8 = true
-//b9 = true
-//b10 = false
-//b11 = true
-//b12 = false
-//b13 = true
-//b14 = true
-//b15 = true
-//b16 = true
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var v1: int;
+var v2: int;
+var v3: int;
+function{:existential true} b1(): bool;
+function{:existential true} b2(): bool;
+function{:existential true} b3(): bool;
+function{:existential true} b4(): bool;
+function{:existential true} b5(): bool;
+function{:existential true} b6(): bool;
+function{:existential true} b7(): bool;
+function{:existential true} b8(): bool;
+function{:existential true} b9(): bool;
+function{:existential true} b10(): bool;
+function{:existential true} b11(): bool;
+function{:existential true} b12(): bool;
+function{:existential true} b13(): bool;
+function{:existential true} b14(): bool;
+function{:existential true} b15(): bool;
+function{:existential true} b16(): bool;
+
+procedure push() 
+requires {:candidate} b1() || v1 == 0;
+requires {:candidate} b2() || v1 == 1;
+ensures  {:candidate} b3() || v1 == 0;
+ensures {:candidate}  b4() || v1 == 1;
+modifies v1,v2;
+{
+   v2 := v1;
+   v1 := 1;
+}
+
+procedure pop()
+modifies v1,v2;
+requires {:candidate} b5() || v1 == 0;
+requires {:candidate} b6() || v1 == 1;
+ensures  {:candidate} b7() || v1 == 0;
+ensures {:candidate}  b8() || v1 == 1;
+{
+   v1 := v2;
+   havoc v2;
+}
+
+procedure foo() 
+modifies v1,v2;
+requires {:candidate} b9() || v1 == 0;
+requires {:candidate} b10() || v1 == 1;
+ensures  {:candidate} b11() || v1 == 0;
+ensures {:candidate}  b12() || v1 == 1;
+{
+   call push();
+   call pop();
+}
+
+procedure bar()
+modifies v1,v2;
+requires {:candidate} b13() || v1 == 0;
+requires {:candidate} b14() || v1 == 1;
+ensures  {:candidate} b15() || v1 == 0;
+ensures {:candidate}  b16() || v1 == 1;
+{
+   call push();
+   call pop();
+}
+
+procedure main() 
+modifies v1,v2;
+{
+   v1 := 1;
+   call foo();
+   havoc v1;
+   call bar();
+}
+
+// Expected:
+//b1 = true
+//b2 = true
+//b3 = true
+//b4 = false
+//b5 = true
+//b6 = false
+//b7 = true
+//b8 = true
+//b9 = true
+//b10 = false
+//b11 = true
+//b12 = false
+//b13 = true
+//b14 = true
+//b15 = true
+//b16 = true
-- 
cgit v1.2.3