rewrite
inline fun <T : KBvSort> KContext.rewriteBvAddNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean, rewriteBvSignedLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvSignedLessExpr, rewriteBvAddExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::simplifyBvAddExpr, rewriteBvZeroExtensionExpr: KContext.(Int, KExpr<T>) -> KExpr<KBvSort> = KContext::simplifyBvZeroExtensionExpr, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<T>) -> KExpr<KBvSort> = KContext::simplifyBvExtractExpr, rewriteBvEq: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBoolSort> = { l, r -> simplifyEq(l, r) }, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { l, r -> simplifyAnd(l, r) }, rewriteImplies: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::simplifyImplies): KExpr<KBoolSort>