Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas

<strong>Fuzzing SMT solvers with Diversified Sub-formulas</strong> Table of Contents Background Install Usage Bugs <strong>Background</strong> <strong>Octopus </strong>is the tool for detecting soundness bugs in SMT solvers. <br> We have submitted 10 valid bug reports for Z3 so far. 7 bugs are confirmed/fixed by developers among these reports. <strong>Install</strong> Octopus itself has few dependencies. It uses Python3 and Python-virtualenv. You can install Python-virtualenv using <code>pip install virtualenv</code> Then install Octopus. <code>virtualenv --python=/usr/bin/python3.6 virenv</code> <code>source virenv/bin/activate</code> <code>cd octopus</code> <code>python3 setup.py install</code> <strong>Usage</strong> 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: <code>git clone https://github.com/Z3Prover/z3.git</code> <code>python scripts/mk_make.py </code> <code>cd build; make</code> Then Octopus can be used to validate it, for example: <code>octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA</code> To run Octopus in multiple cores: <code>octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA --cores=20</code> <strong>Bugs</strong> 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]<br> https://github.com/Z3Prover/z3/issues/5443 [reported]<br> https://github.com/Z3Prover/z3/issues/5447 [fixed]<br> https://github.com/Z3Prover/z3/issues/5456 [fixed]<br> https://github.com/Z3Prover/z3/issues/5457 [fixed] <br> https://github.com/Z3Prover/z3/issues/5460 [fixed]<br> https://github.com/Z3Prover/z3/issues/5468 [fixed] <br> https://github.com/Z3Prover/z3/issues/5488 [fixed]<br> https://github.com/Z3Prover/z3/issues/5502 [duplicate]<br> https://github.com/Z3Prover/z3/issues/5508 [reported]<br> https://github.com/Z3Prover/z3/issues/5423 [invalid]