This is the research artifact of the paper entitled `Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs’. SMT solvers check the satisfiability of logic formulas over first-order theories, which have been utilized in a rich number of critical applications. The implemented tool HistFuzz is a practical fuzzer for SMT solvers, which includes two main components: collecting bug-triggering inputs from mainstream SMT solvers’ issue trackers and utilizing them to perform testing. Compared to the state-of-the-art SMT solver testing tools, HistFuzz exploits historical bug-triggering formulas, which are often neglected by the existing techniques, to generate effective test instances.

The artifact evaluation experiments of HistFuzz include two main aspects: detecting real bugs in SMT solvers and comparing the achieved code coverage with the state-of-the-art fuzzers. We apply to obtain the Available'' andReusable'' badges for the artifacts. The reason is that we place the artifact, which is carefully documented, on a publicly accessible archival repository and also provide a Docker container image to facilitate the reproduction of the results. In addition, we assume users of the artifact are able to use Linux Ubuntu Operating System.