We present a novel automated approach to derive guaranteed bounds on the normalised posterior distribution (NPD) of a probabilistic program with conditioning via polynomial solving. Our approach can handle programs with unbounded while loops and continuous distributions with infinite supports. Concretely, we classify programs in this work into two classes: (i) \emph{score-at end} programs when conditioning occurs only at the end of programs, and (ii) \emph{score recursive} programs when conditioning occurs inside loops. To infer the bounds on NPDs, we establish a fixed-point theorem for \emph{score-at-end} programs and propose a multiplicative variant of Optional Stopping Theorem (OST) for \emph{score-recursive} programs.