A question about the relevancy_lvl parameter

[davidtr1037]

I am using queries with quantifiers (forall) where the body is a formula over arrays and bit-vectors,
and the bound variables are bit-vectors.

Under this scenario:
What is the recommended value for the relevancy_lvl parameter?
Are all the values for this parameter safe? Are there some values which might lead to incorrect results / unsoundness?

[NikolajBjorner]

almost everything uses either relevancy=0 or relevancy=2. When you have arrays and quantifiers, relevancy=2 tends to work better because it throttles quantifier instantiation.
Regarding soundness, it is not expected to affect correctness. There are some other parameter configurations that are less tested and exercised even though they have been pounded well by fuzzing tools by now. I am not sure it is too useful to explore too many configuration settings. You could observe whether z3 runtime fluctuates with different values of random seeds. It is very possible it will given these kinds of formulas. Then the most useful mode is to run z3 with iterative deepening or multiple instances.

[davidtr1037]

Thanks for the reply!

I observed that in ABV (with forall quantifiers), and also in QFABV, relevancy_lvl=0 works much better (compared to relevancy_lvl=2).
I attached below two examples that demonstrate that (with different configurations of this parameter).
Is it just a coincidence or there is a reasonable explanation for that?
queries.tar.gz