Check that signed a + b does not underflow.
(a: BitVecRef, b: BitVecRef)
| 1993 | |
| 1994 | |
| 1995 | def BVAddNoUnderflow(a: BitVecRef, b: BitVecRef) -> BoolRef: |
| 1996 | """Check that signed a + b does not underflow.""" |
| 1997 | sort = a._sort |
| 1998 | if not isinstance(sort, BitVecSortRef): |
| 1999 | raise TypeError("BVAddNoUnderflow requires BitVecRef") |
| 2000 | w = sort._width |
| 2001 | ea = SignExt(1, a) |
| 2002 | eb = SignExt(1, b) |
| 2003 | s = ea + eb |
| 2004 | lower = BitVecVal(-(1 << (w - 1)), w + 1) |
| 2005 | return s >= lower |
| 2006 | |
| 2007 | |
| 2008 | def BVSubNoOverflow(a: BitVecRef, b: BitVecRef) -> BoolRef: |