title: Sample uniformly from set of satisfying assignments in Z3
body: <p>Is there a way to use the Z3 theorem prover to sample uniformly from the set of satisfying assignments? If not, what is the closest system to Z3 that has this capability?</p>