Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas

Fuzzing SMT solvers with Diversified Sub-formulas Table of Contents Background Install Usage Bugs Background Octopus is the tool for detecting soundness bugs in SMT solvers. We have submitted 10 valid bug reports for Z3 so far. 7 bugs are confirmed/fixed by developers among these reports. Install Octopus itself has few dependencies. It uses Python3 and Python-virtualenv. You can install Python-virtualenv using pip install virtualenv Then install Octopus. virtualenv --python=/usr/bin/python3.6 virenv source virenv/bin/activate cd octopus python3 setup.py install Usage You can download SMT instances in SMT COMP 2021 as benchmarks. 2021-05-26 - StarExec Then install and build the SMT solver you want to test. For example: git clone https://github.com/Z3Prover/z3.git python scripts/mk_make.py cd build; make Then Octopus can be used to validate it, for example: octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA To run Octopus in multiple cores: octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA --cores=20 Bugs Octopus has detected many new refutational soundness bugs in Z3. Here is a list of issues we reported. https://github.com/Z3Prover/z3/issues/5373 [confirmed] https://github.com/Z3Prover/z3/issues/5443 [reported] https://github.com/Z3Prover/z3/issues/5447 [fixed] https://github.com/Z3Prover/z3/issues/5456 [fixed] https://github.com/Z3Prover/z3/issues/5457 [fixed] https://github.com/Z3Prover/z3/issues/5460 [fixed] https://github.com/Z3Prover/z3/issues/5468 [fixed] https://github.com/Z3Prover/z3/issues/5488 [fixed] https://github.com/Z3Prover/z3/issues/5502 [duplicate] https://github.com/Z3Prover/z3/issues/5508 [reported] https://github.com/Z3Prover/z3/issues/5423 [invalid]