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/bitvectors/bv9.bpl | 50 ++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'Test/bitvectors/bv9.bpl')

diff --git a/Test/bitvectors/bv9.bpl b/Test/bitvectors/bv9.bpl
index 19a147ad..11c5156b 100644
--- a/Test/bitvectors/bv9.bpl
+++ b/Test/bitvectors/bv9.bpl
@@ -1,25 +1,25 @@
-// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure foo();
-
-implementation foo()
-{
-    assert (forall Q#a$1^15.32#tc1: bv64, Q#b$1^15.32#tc1: bv64, Q#c$1^15.32#tc1: bv64 :: true && true && true ==> ($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) == Q#c$1^15.32#tc1 || $bv_bvadd64($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), 1bv64) == Q#c$1^15.32#tc1) && (if Q#c$1^15.32#tc1 == $bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) then $bv_bvugt64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1)) else $bv_bvuge64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1))) ==> $bv_bvlshr64($bv_bvxor64($bv_bvor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), $bv_bvand64($bv_bvxor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), Q#c$1^15.32#tc1)), 0bv32 ++ 63bv32) == 1bv64);
-}
-
-function {:bvbuiltin "bvlshr"} $bv_bvlshr64(p1: bv64, p2: bv64) : bv64;
-
-function {:bvbuiltin "bvand"} $bv_bvand64(p1: bv64, p2: bv64) : bv64;
-
-function {:bvbuiltin "bvor"} $bv_bvor64(p1: bv64, p2: bv64) : bv64;
-
-function {:bvbuiltin "bvxor"} $bv_bvxor64(p1: bv64, p2: bv64) : bv64;
-
-function {:bvbuiltin "bvuge"} $bv_bvuge64(p1: bv64, p2: bv64) : bool;
-
-function {:bvbuiltin "bvugt"} $bv_bvugt64(p1: bv64, p2: bv64) : bool;
-
-function {:bvbuiltin "bvsub"} $bv_bvsub64(p1: bv64, p2: bv64) : bv64;
-
-function {:bvbuiltin "bvadd"} $bv_bvadd64(p1: bv64, p2: bv64) : bv64;
-
+// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo();
+
+implementation foo()
+{
+    assert (forall Q#a$1^15.32#tc1: bv64, Q#b$1^15.32#tc1: bv64, Q#c$1^15.32#tc1: bv64 :: true && true && true ==> ($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) == Q#c$1^15.32#tc1 || $bv_bvadd64($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), 1bv64) == Q#c$1^15.32#tc1) && (if Q#c$1^15.32#tc1 == $bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) then $bv_bvugt64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1)) else $bv_bvuge64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1))) ==> $bv_bvlshr64($bv_bvxor64($bv_bvor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), $bv_bvand64($bv_bvxor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), Q#c$1^15.32#tc1)), 0bv32 ++ 63bv32) == 1bv64);
+}
+
+function {:bvbuiltin "bvlshr"} $bv_bvlshr64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvand"} $bv_bvand64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvor"} $bv_bvor64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvxor"} $bv_bvxor64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvuge"} $bv_bvuge64(p1: bv64, p2: bv64) : bool;
+
+function {:bvbuiltin "bvugt"} $bv_bvugt64(p1: bv64, p2: bv64) : bool;
+
+function {:bvbuiltin "bvsub"} $bv_bvsub64(p1: bv64, p2: bv64) : bv64;
+
+function {:bvbuiltin "bvadd"} $bv_bvadd64(p1: bv64, p2: bv64) : bv64;
+
-- 
cgit v1.2.3