Guide: BitVec arithmetic wraps modularly.
(self)
| 647 | """From z3py guide: machine arithmetic (bit-vectors).""" |
| 648 | |
| 649 | def test_bv_arithmetic(self): |
| 650 | """Guide: BitVec arithmetic wraps modularly.""" |
| 651 | x = BitVec("x", 16) |
| 652 | y = BitVec("y", 16) |
| 653 | expr = x + y |
| 654 | assert isinstance(expr, BitVecRef) |
| 655 | assert expr.size() == 16 |
| 656 | |
| 657 | def test_bv_signed_vs_unsigned_comparison(self): |
| 658 | """Guide: signed < is different from ULT.""" |