Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas

## Installation:<br> ```<br> virtualenv --python=/usr/bin/python3 virenv<br> source virenv/bin/activate<br> cd octopus<br> python3 setup.py install<br> ``` ## Usage: ```<br> octopus --benchmark=[PATH TO SEED DIRECTORY] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=[SOLVER THEORY]<br> ``` For example: ```<br> octopus --benchmark=/home/SMT2021 --solverbin=../z3/build/z3 --solver=z3 --theory=LIA<br> ``` To run `n` parallel instances of octopus on `n` cores, use the `--cores` flag. For example: ```<br> octopus --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA --cores=10<br> ``` <br> ## Refutational soundness bugs detected so far:<br> octopus has detected many new "refutational soundness" bugs in Z3. <br> Here is a list of issues we reported. https://github.com/Z3Prover/z3/issues/5373 `[z3]` `[QF_NRA]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5443 `[z3]` `[QF_BVFP]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5447 `[z3]` `[QF_ABV]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5456 `[z3]` `[QF_IDL]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5457 `[z3]` `[QF_BV]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5460 `[z3]` `[QF_BV]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5468 `[z3]` `[AUFLIRA]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5488 `[z3]` `[QF_BV]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5502 `[z3]` `[QF_NIA]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5508 `[z3]` `[QF_NIA]` &lt;br&gt;<br> https://github.com/Z3Prover/z3/issues/5423 `[z3]` `[QF_BVFP]` `Won't fixed` &lt;br&gt;<br>