Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas

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