rewrite
inline fun <T : KBvSort> KContext.rewriteBvSubNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvSignedLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvSignedLessExpr, rewriteBvAddNoOverflowExpr: (KExpr<T>, KExpr<T>, Boolean) -> KExpr<KBoolSort> = { l, r, isSigned -> simplifyBvAddNoOverflowExpr(l, r, isSigned) }, rewriteBvEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = { l, r -> simplifyEq(l, r) }, rewriteBvNegationExpr: KContext.(KExpr<T>) -> KExpr<T> = KContext::simplifyBvNegationExpr, rewriteIte: (KExpr<KBoolSort>, KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { c, t, f -> simplifyIte(c, t, f) }): KExpr<KBoolSort>