kdrag.termination.opaque_abs_size

kdrag.termination.opaque_abs_size(e: ExprRef) → ExprRef

A kludge to get around the fact that Z3’s size function can return negative values, which breaks some of my proofs.