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