rewrite
inline fun <T : KBvSort> KContext.rewriteBvDivNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = { l, r -> simplifyEq(l, r) }, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { l, r -> simplifyAnd(l, r) }, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::simplifyNot): KExpr<KBoolSort>