Function nonzero_bound 

fn nonzero_bound<'a>(
    expr: &'a SymExpr,
    value: &'a SymExpr,
) -> Option<(&'a SymExpr, U256)>