Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas

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