Check that a - b does not underflow.
(a: BitVecRef, b: BitVecRef, signed: bool = False)
| 2019 | |
| 2020 | |
| 2021 | def BVSubNoUnderflow(a: BitVecRef, b: BitVecRef, signed: bool = False) -> BoolRef: |
| 2022 | """Check that a - b does not underflow.""" |
| 2023 | sort = a._sort |
| 2024 | if not isinstance(sort, BitVecSortRef): |
| 2025 | raise TypeError("BVSubNoUnderflow requires BitVecRef") |
| 2026 | w = sort._width |
| 2027 | if signed: |
| 2028 | ea = SignExt(1, a) |
| 2029 | eb = SignExt(1, b) |
| 2030 | s = ea - eb |
| 2031 | lower = BitVecVal(-(1 << (w - 1)), w + 1) |
| 2032 | return s >= lower |
| 2033 | else: |
| 2034 | return ULE(b, a) |
| 2035 | |
| 2036 | |
| 2037 | def BVMulNoOverflow(a: BitVecRef, b: BitVecRef, signed: bool = False) -> BoolRef: |