smtfuzz: a random generator for SMT-LIB2 formulas

smtfuzz generates random SMT-LIB 2 formulas for stress-testing SMT solvers. It can be used as:

• a standalone formula generator that prints an SMT-LIB benchmark to standard output;
• an advanced runner for seed-based fuzzing and generation-based solver testing; and
• a library of mutation components for SMT-LIB formulas and solver options.

SMT solvers determine the satisfiability of logical formulas over theories such as arithmetic, bit-vectors, arrays, strings, floating point, sets, bags, and uninterpreted functions. Random generation and mutation help exercise solver front ends, simplifiers, theory solvers, and model/answer consistency checks.

Installation

From PyPI

pip3 install smtfuzz

From source

git clone https://github.com/ZJU-Automated-Reasoning-Group/smtfuzz.git
cd smtfuzz
python -m pip install -e .

The package requires Python 3.6 or newer. Runtime dependencies are declared in setup.py and include z3-solver, meson, and tqdm.

Quick start

Generate one random SMT-LIB2 formula and write it to stdout:

smtfuzz

Generate a bit-vector benchmark with a fixed random seed:

smtfuzz --logic QF_BV --strategy noinc --seed 1

Save a generated formula to a file:

smtfuzz --logic QF_LIA --strategy cnf > case.smt2

Run an installed solver on the generated benchmark:

z3 case.smt2

Use smtfuzz --help to see all options supported by the standalone generator.

Command-line tools

smtfuzz

The smtfuzz console script invokes the legacy random SMT-LIB generator in smtfuzz/smtfuzz.py.

Common options:

Option	Purpose
--logic LOGIC	SMT-LIB logic to generate, such as QF_BV, QF_LIA, or random.
--strategy STRATEGY	Generation strategy: noinc, bool, cnf, ncnf, CNFexp, strictcnf, or random.
--seed SEED	Random seed for reproducible generation.
--cntsize N	Maximum number of assertions per generated query.
--smtopt 1	Enable optimization-query generation.
--maxsmt 1	Enable MaxSMT generation.
--qbf 1	Enable QBF-style generation.
--qe 1	Enable quantifier-elimination queries.
--unsat_core 1	Enable named assertions and unsat-core queries.
--proof 1	Enable proof-production queries.

smtfuzz-runner

The smtfuzz-runner console script provides higher-level fuzzing modes:

• seed: mutate and run existing .smt2 seed files;
• gen: generate formulas and run a target solver.

Examples:

# Seed-based fuzzing with a local corpus
smtfuzz-runner seed --seed /path/to/seeds --solver z3 --output /tmp/smtfuzz-results

# Differential seed fuzzing with multiple solvers
smtfuzz-runner seed --seed /path/to/seeds --diff yes --solvers "z3;cvc5" --output /tmp/smtfuzz-diff

# Generation-based fuzzing against one solver
smtfuzz-runner gen --solver cvc5 --logicmode bv --count 100 --output /tmp/smtfuzz-gen

# Increase parallelism
smtfuzz-runner gen --solver z3 --workers 4 --count 500

Use smtfuzz-runner --help, smtfuzz-runner seed --help, or smtfuzz-runner gen --help for the full argument lists.

Repository layout

smtfuzz/
  smtfuzz.py          Legacy standalone random SMT-LIB generator
  cli.py              Entry point for the `smtfuzz` command
  runner_cli.py       Entry point for the `smtfuzz-runner` command
  runner/             Seed-based and generation-based fuzzing runners
  bet/                Bounded-exhaustive testing and mutation utilities
  sae/                Skeletal approximation enumeration utilities
  inter/              Inter-theory seed generation and mutation engine
  options/            Solver-option mutators
  tests/              Regression tests

Additional documentation is available in:

• smtfuzz/runner/README.md for runner architecture and examples;
• smtfuzz/inter/README.md for inter-theory mutation details.

Development

Install the project in editable mode before making changes:

python -m pip install -e .

Run the current test suite with:

python -m pytest smtfuzz/tests

When adding generation features, prefer documenting a small reproducible command that uses --seed so solver failures can be replayed.

Feedback and bug reports

Please open a GitHub issue for bugs, questions, or feature requests. If you report a solver crash or wrong answer, include:

1. the generated SMT-LIB file or seed file;
2. the smtfuzz or smtfuzz-runner command used to produce it;
3. solver name, version, and command-line options; and
4. operating system and Python version.

A list of detected solver bugs is maintained at https://smtfuzz.github.io/.

Publications

@inproceedings{zheng2025bsd,
  title={SAS 2025: Bounded-Exhaustive Subspace Diversification for SMT Solver Testing},
  author={Zheng, Junda and Yao, Peisen},
  booktitle={Proceedings of the 32nd Static Analysis Symposium},
  year={2025}
}

@inproceedings{fse21skeletal,
  title={Skeletal Approximation Enumeration for SMT Solver Testing},
  author={Yao, Peisen and Huang, Heqing and Tang, Wensheng and Shi, Qingkai and Wu, Rongxin and Zhang, Charles},
  booktitle={Proceedings of the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering},
  series={ESEC/FSE 2021},
  year={2021},
  publisher={ACM}
}

@inproceedings{issta21opt,
  title={Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration},
  author={Yao, Peisen and Huang, Heqing and Tang, Wensheng and Shi, Qingkai and Wu, Rongxin and Zhang, Charles},
  booktitle={Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis},
  series={ISSTA 2021},
  year={2021},
  publisher={ACM}
}