nicdard
commented
2 years ago Coverage information:
- compare on a subset of the seeds the original yinyang fusion functions with our generated functions
- change parameters to the generator
Bug bounty:
- use different solvers
We should define a strategy to conduct the benchmarking with different number of operators in the functions and so on and document it for the final report.
I would also like to explore other smt solvers, from those that are listed on the SMT-LIB website and are still under active development. Those solver should be compatible with SMT-LIB format. This would increase our chances to actually find some real bugs as I think most of the researchers focus on Z3 and CVC4/5. openSMT2 seems to be a good candidate for example