Z3 randomness of generated model values

Question

I am trying to influence the randomness of results for model values ​​generated by Z3. As far as I understand, the options for this are very limited: in the case of linear arithmetic, the simplex solver does not allow random results that still satisfy the given constraints. However, there is the smt.arith.random_initial_value option ("use random initial values ​​in a procedure based on the simplex method for linear arithmetic (default: false)"), which does not seem to work:

from z3 import * set_option('smt.arith.random_initial_value',True) x = Int('x') y = Int('y') s = Solver() s.add( x+y > 0) s.check() s.model() 

As a result, it seems that it always turns out [y = 0, x = 1]. Even completion of the model for variables not used in these constraints creates deterministic results all the time.

Any ideas or tips on how this option works?

Answer 1

Thanks for catching this! In fact, there was a mistake due to which the random seed was not transmitted to arithmetic theory. Now this is fixed in an unstable branch (fix here ).

In this example:

 (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) 

Now three different models are produced:

 sat model (define-fun y () Int 4294966763) (define-fun x () Int 4294966337) ) sat (model (define-fun y () Int 216) (define-fun x () Int 4294966341) ) sat (model (define-fun y () Int 196) (define-fun x () Int 4294966344) ) 

It seems that there may be another place where this option is not passed correctly (for example, when using set-logic instead of directly invoking qflra tactics) we are still studying this.