如何从Microsoft Z3获得随机结果？

Question

在Microsoft Z3中，当我们试图解决一个公式时，当存在两个或更多可满足的解决方案时，Z3总是以相同的顺序返回结果。

是否可以从Z3中获得随机结果，以便对于相同的输入，它将在不同的执行过程中生成不同的输出序列。

请注意，我使用C或C＃API。我没有使用smt2lib使用Z3。所以如果你能给我一个可以添加随机化的C或C＃API函数的例子，它会更有用。

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) 

摘自here。