3 files changed, 30 insertions, 0 deletions
diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer
index 1bcc3a2b..aa060ee4 100644
--- a/Test/bitvectors/Answer
+++ b/Test/bitvectors/Answer
@@ -49,3 +49,7 @@ Boogie program verifier finished with 0 verified, 1 error
 -------------------- bv8.bpl --------------------
 
 Boogie program verifier finished with 2 verified, 0 errors
+-------------------- bv9.bpl /bv:z /z3bv --------------------
+Boogie program verifier version 2, Copyright (c) 2003-2010, Microsoft.
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/bitvectors/bv9.bpl b/Test/bitvectors/bv9.bpl
new file mode 100644
index 00000000..9637c87f
--- /dev/null
+++ b/Test/bitvectors/bv9.bpl
@@ -0,0 +1,23 @@
+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;
+
diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat
index cbafa065..2ec881fd 100644
--- a/Test/bitvectors/runtest.bat
+++ b/Test/bitvectors/runtest.bat
@@ -15,3 +15,6 @@ for %%f in (bv5.bpl bv6.bpl bv8.bpl) do (
   echo -------------------- %%f --------------------
   %BGEXE% %* %%f
 )
+
+echo -------------------- bv9.bpl /bv:z /z3bv --------------------
+%BGEXE% /bv:z /z3bv bv9.bpl
+\ No newline at end of file