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