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/multi.bpl | 134 +++++++++++++++++++++++-----------------------
 1 file changed, 67 insertions(+), 67 deletions(-)

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

diff --git a/Test/AbsHoudini/multi.bpl b/Test/AbsHoudini/multi.bpl
index a33817ac..e53bb075 100644
--- a/Test/AbsHoudini/multi.bpl
+++ b/Test/AbsHoudini/multi.bpl
@@ -1,67 +1,67 @@
-function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;
-function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;
-function {:existential true} {:absdomain "PowDomain"} b3(x1: int) : bool;
-function {:existential true} {:absdomain "PowDomain"} b4(x1: bv32) : bool;
-function {:existential true} {:absdomain "EqualitiesDomain"} b5(x: int, y: int, z: int, w:int) : bool;
-
-function {:builtin "bvslt"} BV_SLT(x: bv32, y: bv32) : bool;
-
-var x: int;
-var flag: bool;
-
-// Test implication domain
-procedure foo ()
-  modifies x, flag;
-{
-   flag := true;
-   x := 0;
-   assert b1(flag, x == 0);
-   flag := false;
-   assert b2(flag, x == 0);
-}
-
-// Test for PowDomain(int)
-procedure bar1 ()
-  modifies x, flag;
-{
-   x := 2;
-   if(*) { x := 16; }
-   assert b3(x);
-}
-
-// Test for PowDomain(bv32)
-procedure bar2 ()
-  modifies x, flag;
-{
-  var s: bv32;
-
-  s := 2bv32;
-  if(*) { s := 16bv32; }
-  assert b4(s);
-}
-
-// Test for EqualitiesDomain
-procedure baz ()
-  modifies x, flag;
-{
-  var y: int;
-  var z: int;
-  var w: int;
-
-  assume x == y;
-  assume x == z;
-
-  if(*) {
-    x := x + 1;
-    y := y + 1;
-  } else {
-    x := x + 2;
-    y := y + 2;
-  }
-
-  assume x == w;
-
-  assert b5(x,y,z,w);
-}
-
-
+function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;
+function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;
+function {:existential true} {:absdomain "PowDomain"} b3(x1: int) : bool;
+function {:existential true} {:absdomain "PowDomain"} b4(x1: bv32) : bool;
+function {:existential true} {:absdomain "EqualitiesDomain"} b5(x: int, y: int, z: int, w:int) : bool;
+
+function {:builtin "bvslt"} BV_SLT(x: bv32, y: bv32) : bool;
+
+var x: int;
+var flag: bool;
+
+// Test implication domain
+procedure foo ()
+  modifies x, flag;
+{
+   flag := true;
+   x := 0;
+   assert b1(flag, x == 0);
+   flag := false;
+   assert b2(flag, x == 0);
+}
+
+// Test for PowDomain(int)
+procedure bar1 ()
+  modifies x, flag;
+{
+   x := 2;
+   if(*) { x := 16; }
+   assert b3(x);
+}
+
+// Test for PowDomain(bv32)
+procedure bar2 ()
+  modifies x, flag;
+{
+  var s: bv32;
+
+  s := 2bv32;
+  if(*) { s := 16bv32; }
+  assert b4(s);
+}
+
+// Test for EqualitiesDomain
+procedure baz ()
+  modifies x, flag;
+{
+  var y: int;
+  var z: int;
+  var w: int;
+
+  assume x == y;
+  assume x == z;
+
+  if(*) {
+    x := x + 1;
+    y := y + 1;
+  } else {
+    x := x + 2;
+    y := y + 2;
+  }
+
+  assume x == w;
+
+  assert b5(x,y,z,w);
+}
+
+
-- 
cgit v1.2.3