PV1 Murxlafuzzer for SMT solvers

Application domain/field

Type of tool

Fuzzer for SMT solvers

Expected input


Expected output

API trace file if an issue is encountered. This trace file can be replayed (and minimized) to trigger the issue.


Murxla is a model-based API fuzzer for SMT solvers, i.e. it tries to find bugs in SMT solvers via fuzzing. It generates valid sequences of solver API calls. It provides support to record, minimize and replay such traces. Murxla currently supports the following SMT solvers: Bitwuzla, Boolector, cvc5, Yices Murxla supports two modes: continuous and one-shot. Continuous can be used to continuously fuzz an SMT solver until (1) it is interrupted or (2) the specified maximum number of test runs were performed. This is typically used to find solver errors. In one-shot mode, Murxla performs a single test run. This can be done using either a specific seed or an API trace. This is typically used to inspect a specific test run in detail, i.e. debugging purposes. Murxla also provides options to replay and minimize traces.


Related papers

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (CAV 2022)

Last publication date

6 August 2022

Related tools

Other fuzzers for the SMT-LIB language: FuzzSMT, Storm, TypeFuzz

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.