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/bv9.bpl | |
| 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/bv9.bpl')
| -rw-r--r-- | Test/bitvectors/bv9.bpl | 23 |
1 files changed, 23 insertions, 0 deletions
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;
+
|