rewrite
inline fun <T : KBvSort> KContext.rewriteBvSubNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean, rewriteBvSignedLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvSignedLessExpr, rewriteBvUnsignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvUnsignedLessOrEqualExpr, createBvAddNoUnderflowExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvAddNoUnderflowExpr, rewriteBvNegationExpr: KContext.(KExpr<T>) -> KExpr<T> = KContext::simplifyBvNegationExpr, rewriteImplies: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::simplifyImplies): KExpr<KBoolSort>