def mk_at_least_one(ctx, nets):
    """
    Computes "at least one net is true"

    Args:
        ctx: the context to use
        nets: the nets to use
    """
    at_least_one = ctx.mk_false()
    num_nets = len(nets)
    for i in range(num_nets):
        at_least_one = ctx.mk_or(at_least_one, nets[i])
    return at_least_one