Efficient Analysis of Probabilistic Programs with an Unbounded Counter