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
The evidence describes a three-phase workflow for test generation:
- A symbolic phase that produces a CNF-like normal form and partitions the input/output relation.
- A test data selection phase that uses constraint solvers, random test generation, and the integrated SMT solver Z3 to instantiate each partition.
- A test execution phase that converts instantiated test cases, also called test oracles, into test driver code for execution against the system under test. [C1]
Within this workflow, Z3 contributes specifically to the construction of concrete instances during test data selection after the input/output relation has been partitioned. [C1]
Technical context
The same source situates the use of Z3 within sequence-oriented test generation for systems whose behavior is modeled as state transitions. In the HOL-TestGen setting described, sequence test specifications are represented using state-exception monads, allowing programs under test to be treated as input/output stepping functions that may either fail for a state and input or produce an output and successor state. [C2]
Related tools
- HOL-TestGen uses Z3 as an integrated SMT solver during its test data selection workflow. [C1]