rewrite
inline fun <T : KBvSort> KContext.rewriteBvAddNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvSignedLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvSignedLessExpr, rewriteBvAddExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T> = KContext::simplifyBvAddExpr, 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>