SMT solvers are automated tools that can determine the satisfiability of logical formulas in various theories, including arithmetic, bit-vectors, arrays, and more. smtfuzz is a random generator for SMT-LIB2 formulas. It is designed to help users generate test cases for SMT solvers and explore various SMT-LIB2 features.
To install a stable version of smtfuzz:
pip3 install smtfuzz
Install from source
pip install -e .
After installing the package, you can type
smtfuzz
And you will see an SMT-LIB2 formula on the screen.
For more advanced options, please use the -h flag to display the help menu. Feel free to experiment with different combinations of options to generate a wide variety of SMT-LIB2 formulas for testing purposes.
Please submit an issue to report any bugs, issues, questions, or feature requests. We are pleased to receive your feedback.