search

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
403 stars 75 forks source link

add --seed option to smtbmc and btor engines #97

Closed nakengelhardt closed 4 years ago

nakengelhardt commented 4 years ago

Allows setting a seed for the solver in the [engines] section:

[engines]
smtbmc --seed 42 yices
btor --seed 42 btormc

For btor the seed is not in the file format so requires engine-specific handling, but the code for parsing it if it's before the engine is already there, whereas args after the engine aren't processed. I like having it more uniform, but I can change it if you really want...