edict_generate_tests
Generate structured test cases automatically from Z3-verified contracts, extracting boundary values and counterexamples to create regression tests without manual effort.
Instructions
Auto-generate structured test cases from Z3-verified contracts. For proven contracts, extracts boundary input values and expected outputs from Z3 models. For failing contracts, extracts counterexample inputs as regression tests. Returns an array of GeneratedTest objects — each with function name, input values, expected output, and source (boundary/counterexample). Use this to get free tests from formal specifications without writing them manually.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| ast | Yes | The Edict program AST (module) — same format as edict_check |