Z3 SMT solver
ToolZ3 is identified in the available evidence as an integrated SMT solver used by HOL-TestGen during test data selection, where it is combined with other constraint-solving techniques and random test generation to instantiate test cases for partitions of an input/output relation.
First seen 5/25/2026
Last seen 8/16/2026
Evidence 14 chunks
Wiki v1
WIKI
Overview
Z3 is referenced as an integrated SMT solver in the context of HOL-TestGen-based test generation. In the cited microprocessor test-program-generation case study, Z3 appears in the test data selection phase, where it is used together with a combination of constraint solvers and random test generation to construct an instance for each generated partition. [C1]
Role in HOL-TestGen test generation
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
10 connectionsDependency analysis uses the Z3 SMT solver for satisfiability checking.
UCLID5 invokes the Z3 SMT solver to check satisfiability of verification conditions.
EPEX uses the Z3 SMT solver for efficient reasoning.
The paper uses Z3 SMT solver for dependency satisfiability checking.
Examiner uses the Z3 SMT solver to solve encoding symbol constraints for test case generation.
FuSS uses the Z3 SMT solver for constraint solving during symbolic execution.
Z3 SMT-solver was used by the same research group for contract mutation, in contrast to MINION used for program-level distinguishing test cases.
Z3 SMT solver is referenced as a constraint solving tool used in the framework
Z3 is an SMT solver for constraint solving
HOL-TestGen uses Z3 as an integrated SMT solver for test data selection.
LINKED ENTITIES
1 linksCITATIONS
2 sources2 citations — click to collapse
[1] Z3 is an integrated SMT solver used during HOL-TestGen test data selection together with constraint solvers and random test generation to construct an instance for each partition. Test Program Generation for a Microprocessor: A Case Study
[2] The HOL-TestGen context described in the evidence represents sequence test specifications using state-exception monads and models programs under test as input/output stepping functions over state. Test Program Generation for a Microprocessor: A Case Study