diff options
| author |  stobies <unknown> | 2010-08-06 08:23:27 +0000 |
|---|---|---|
| committer | stobies <unknown> | 2010-08-06 08:23:27 +0000 |
| commit | 149d9a5ec06529e7f4c4c6e3cb688d2c73a2c1f0 (patch) | |
| tree | 58dd84047d9d685caa78f14e5338a593371fbc9c /Test/bitvectors | |
| parent | 92414e15910661de7203bbaf8a20942baac50403 (diff) | |
Boogie: added /z3bv option that overrides the current setting of Z3 options for better performance on VCs that are heavy on bitvector arithmetic
Diffstat (limited to 'Test/bitvectors')
| -rw-r--r-- | Test/bitvectors/Answer | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv9.bpl | 23 | ||||
| -rw-r--r-- | Test/bitvectors/runtest.bat | 3 |
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 |