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 feasible solutions.

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

Please note that I am using the C or C # API. I do not use Z3 using smt2lib. Therefore, if you can give me an example of a C or C # API function 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 (> (+ xy) 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 .