mk
open fun <T : KBvSort> mkBvAddNoOverflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>, isSigned: Boolean): KBvAddNoOverflowExpr<T>
Create BitVec add-no-overflow check expression. Determines that BitVec arithmetic addition does not overflow. An overflow occurs when the addition result value is greater than max supported value.
See also
for the underflow check.