CODEWITHSUNDEEP
z3
Shambo
Shambo

Reputation: 946

Use of random-seeds in Z3

What is the use of the option random-seed in z3? Can it be used to generate random models? In this post Z3: Offering random solutions in solving, it is mentioned that LIA cant have random models. So why do we need random-seeds?

Upvotes: 3

Views: 1654

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

You can use random seeds to control the propositional variable selection heuristic in the SMT core. Random seeds can among other things be used to check if the performance of the SAT search component is stable under pertubations in the order of how the formula is written.

Upvotes: 2

Related Questions