Reasoning about non-deterministically terminating loops
In [dB80] Hitchcock and Park's analysis of the termination properties
of recursion is proven to correspond to a semantic analysis based on
the so-called Egli-Milner interpretation of relations [Egl75, Plo76],
which expresses erratic nondeterminism. This notion captures
that a nondeterministic union of relations is correct if it generates
at least one computation leading to a desired result (even in the
presence of a nonterminating computation). This appears to correspond
to what you are trying to do.

Next characterize the meaning of a statement $S$ as a function $f_S$
mapping each initial state $\sigma$ to some nonempty set of states,
possibly containing $\bot$, such that $f_S$ is strict in the sense
that $f_S(\bot) = \{\bot\}$. The nondeterministic choice between
statements $S_1$ and $S_2$ is described by the function mapping each
initial state $\sigma$ to the union of the individual results $f_{S_1}
(\sigma) \cup f_{S_2} (\sigma)$. Thus, whenever $S_1$ or $S_2$ has the
nondeterministic possibility of producing an undesirable result, then
so does their nondeterministic choice. As the resulting sets of final
states one obtains in this analysis the so-called Egli-Milner
powerset of states:

${\cal P}_{\text{E--M}}(S) = \{ ~s\subseteq S_\bot ~|~ s$ is finite and nonempty, or contains $\bot\}$

Why are infinite subsets of $S$ not considered possible sets of final
states in this model? Under the assumption that all basic building
blocks of relational terms produce only finite, nonempty sets of
possible final states, an infinite set of possible final states can
only be generated when an infinite computation is possible. This can
be seen as follows. Structure the set of all possible computations
starting in a given state $\sigma_0$ as a tree with root $\sigma_0$
and states as nodes. The set of leaves is then exactly the set of
possible final states reachable from $\sigma_0$, except for $\bot$,
which might be missing among the leaves but is represented in the set
of final states by the fact that there is an infinite path in the
tree. By the assumption above, and since only finite nondeterministic
choice is available, this tree is finitely branching. Thus, there is
only a finite number of leaves at any given finite depth. Consequently
an infinite number of possible final states can only be generated in
the presence of an infinite computation (an application of König's
lemma [Kön32]).

$({\cal P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$ is a poset for
$\sqsubseteq_{\text{E--M}}$ defined by: for $s,t\in{\cal
  P}_{\text{E--M}}(S)$,

$
  s\sqsubseteq_{\text{E--M}} t\quad = \quad
  (\bot\in s \land s\setminus\{\bot\}\subseteq t)
  \lor (\bot\notin s \land s=t)~.
$

Here, $\bot$ can be seen as a placeholder through which
$\sqsubseteq_{\text{E--M}}$-greater sets can be generated by inserting
more states in lieu of $\bot$. Therefore, $\{\bot\}$ is the least
element of $({\cal P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$.
Furthermore, the poset $({\cal
  P}_{\text{E--M}}(S),\sqsubseteq_{\text{E--M}})$ possesses lub's for
$\omega$-chains. Similarly, the strict functions from $S\cup\{\bot\}$
to ${\cal P}_{\text{E--M}}(S)$ are partially ordered by the pointwise
extension of $\sqsubseteq_{\text{E--M}}$. Moreover, the least such
function is $\lambda\sigma.\{\bot\}$ and lub's of $\omega$-chains of
such functions exist, too.

[dB80] JW de Bakker. Mathematical Theory of Program Correctness.
Prentice Hall, 1980.

[Egl75] H Egli. A mathematical model for nondeterministic
computations. Technical report, ETH Zürich, 1975.

[Kön32] D König. Theorie der endlichen und unendlichen Graphen.
Technical report, Leipzig, 1932.

[Plo76] GD Plotkin. A powerdomain construction. SIAM Journal on
  Computation, 5(3):452-487, 1976.

Disclaimer: this is taken almost verbatim from a book I once co-authored:

WP de Roever and K Engelhardt. Data Refinement: Model-Oriented
  Proof Methods and their Comparison. Cambridge University Press, 1998.