SMTLib compliance for `random-seed`

[LeventErkok]

Hi Nikolaj,

I noticed that you've removed the random-seed parameter, opting for sat.random-seed and smt.random-seed. Unfortunately, this causes a minor issue with the SMTLib standard. Page 57 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf states solvers can optionally support a :random-seed setting. Of course, this is an optional requirement, so you can choose not to implement it; but it's rather unfortunate as z3's behavior changed. For this simple benchmark:

(set-option :random-seed 123)

we now get:

(error "line 1 column 26: unknown parameter 'random_seed', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list")

Per strict reading of the standard, I suppose you should instead print unsupported to be fully compliant.

This is a minor issue, but wanted to draw your attention to it. My personal preference would be that you keep supporting :random-seed per the SMTLib standard (and default it to the smt.random-seed internally, I suppose?), but wanted to hear your opinion on it.

Cheers..

[LeventErkok]

The same comment also applies to the comand:

(get-option :random-seed)

which is also no longer supported by z3.

[NikolajBjorner]

reverted then, 18b8089a1ee1b060ffb0cb728acd56f24333c70b

[LeventErkok]

Thanks!