rewrite
fun <T : KBvSort> KContext.rewriteBvMulNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvExtractExpr, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvConcatExpr, rewriteBvMulExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvMulExpr, rewriteBvXorExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvXorExpr, rewriteBvEq: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBoolSort> = { l, r -> mkEq(l, r) }, rewriteBvNotExpr: KContext.(KExpr<T>) -> KExpr<T> = KContext::mkBvNotExpr, rewriteOr: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>, Boolean, Boolean) -> KExpr<KBoolSort> = KContext::mkOr, rewriteFlatOr: KContext.(List<KExpr<KBoolSort>>) -> KExpr<KBoolSort> = { mkOr(it) }, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { l, r -> mkAnd(l, r) }, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::mkNot): KExpr<KBoolSort>