Using SMT solvers to generate random solutions to given predicate

Question

I am interested in generating random solutions to predicates. I only need SMT for integers with the following predicates/functions <, >, <=, >=, ==, !=, +, *

The algorithm I want should produce a random assignment of variables to values (a substitution) such that applying the substitution to the given predicate yields a true statement. In the UNSAT case I just need to know that it is UNSAT.

It is probably important to clarify what I mean by random. I think a sufficient definition is that there might be an extra parameter that acts as a seed. If I give a different seed the algorithm should give me a very different solution rather than the same solution. Frankly I'm not sure how to cash this out but it much the same way that a typical random number generator generates an integer between X and Y (well with a modulus and an addition anyhow) I'd like to generate to a wider class of predicates.

I would like to use existing SMT solvers ideally in either Haskell or the JVM stack (more ideally Haskell however). I have thought of basically just randomizing the DPLL algorithm and translating the SMT problems into SAT my self but that sounds like a terrible idea when really good existing SMT solvers exist.