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 6/22/2026
Evidence 11 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
7 connectionsUCLID5 invokes the Z3 SMT solver to check satisfiability of verification conditions.
Dependency analysis uses the Z3 SMT solver for satisfiability checking.
EPEX uses the Z3 SMT solver for efficient reasoning.
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.
The paper uses Z3 SMT solver for dependency satisfiability checking.
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