pub fn lower_bool_bounded(e: &BoundedExpr) -> Result<ProofExpr, BlastRefusal>Expand description
lower_bool with the refusal NAMED. The circuit is built in the shared DAG and PRICED before
anything is materialised, so an obligation past the budget costs the DAG — never the tree, and
never the allocator.