Check that signed a - b does not overflow.
(a: BitVecRef, b: BitVecRef)
| 2006 | |
| 2007 | |
| 2008 | def BVSubNoOverflow(a: BitVecRef, b: BitVecRef) -> BoolRef: |
| 2009 | """Check that signed a - b does not overflow.""" |
| 2010 | sort = a._sort |
| 2011 | if not isinstance(sort, BitVecSortRef): |
| 2012 | raise TypeError("BVSubNoOverflow requires BitVecRef") |
| 2013 | w = sort._width |
| 2014 | ea = SignExt(1, a) |
| 2015 | eb = SignExt(1, b) |
| 2016 | s = ea - eb |
| 2017 | upper = BitVecVal((1 << (w - 1)) - 1, w + 1) |
| 2018 | return s <= upper |
| 2019 | |
| 2020 | |
| 2021 | def BVSubNoUnderflow(a: BitVecRef, b: BitVecRef, signed: bool = False) -> BoolRef: |