How to get random results from Microsoft Z3?

Question

In Microsoft Z3, when we try to solve a formula, Z3 always returns the results in the same sequence, when there are two or more satisfiable solutions.

Is it possible to get random results from Z3 so that for the same input, it will generate different output sequence in different execution.

Please note that, I am using C or C# API. I am not using Z3 using smt2lib. So if you can give me a C or C# API function example that can add randomization, it will be more useful.

Answer 1

(set-option :smt.arith.random_initial_value true)
(declare-const x Int)
(declare-const y Int)
(assert (> (+ x y) 0))
(check-sat-using (using-params qflra :random_seed 1))
(get-model)
(check-sat-using (using-params qflra :random_seed 2))
(get-model)
(check-sat-using (using-params qflra :random_seed 3))
(get-model)

Taken from here.