Using SMT solvers to generate random solutions to given predicate
Let $\varphi(x)$ be the SMT instance, so the task is to find $x$ such that $\varphi(x)$ is true.

One approach is to fix a hash function $h$ that maps a value of $x$ to an element of some small set $S$.  Then, you randomly select a value $s \in S$, and ask your SMT solver to find a satisfying assignment for the formula $\varphi(x) \land h(x)=s$.

If you want to generate $k$ random satisfying assignments to $\varphi(x)$, you might choose $S$ to have size a bit bigger than $k$; that will probably suffice.

You probably want to make the hash function $h$ as simple as possible.  There is a tradeoff between a simpler hash function (easier for the SMT solver to find satisfying assignments to $\varphi(x) \land h(x)=s$) and a better hash function that mixes the bits better (leads to more random solutions $x$).  In practice, often surprisingly simple hash functions suffice.  For instance, sometimes your hash function can be chosen via the following simple procedure: pick a random subset of the variables in $x$, project to just those variables, and then hash those variables in some simple way.  The hash function itself can be a relatively simple function, e.g., a random linear function: for example, select a random boolean matrix and multiply it with the bit vector obtained from $x$, so that $h(x)=Mx$ for some boolean matrix $M$). 

There may be other ways to do it, but this is one way that allows you to use an existing SMT solver, unmodified, as a black box.