Currently vera test skips functions with ADT parameters (e.g. @Color, @Option<Int>) because the Z3 input generation pipeline only supports primitive types. String and Float64 are being added in #169, but ADTs require constructor synthesis — generating a valid Color means picking one of Red, Green, Blue and synthesising the right WASM value.
Scope: Extend the test runner to generate inputs for simple ADTs (enums with no fields, and ADTs whose constructor fields are all in _Z3_SUPPORTED). Complex cases (ADTs with recursive fields, generic ADTs) may remain out of scope.
Depends on: #169 (String/Float64 support, which establishes the heterogeneous-input infrastructure)
SKIPPED (cannot generate Color inputs) ← current
TESTED (5/5 passed) ← goal
Currently
vera testskips functions with ADT parameters (e.g.@Color,@Option<Int>) because the Z3 input generation pipeline only supports primitive types. String and Float64 are being added in #169, but ADTs require constructor synthesis — generating a validColormeans picking one ofRed,Green,Blueand synthesising the right WASM value.Scope: Extend the test runner to generate inputs for simple ADTs (enums with no fields, and ADTs whose constructor fields are all in
_Z3_SUPPORTED). Complex cases (ADTs with recursive fields, generic ADTs) may remain out of scope.Depends on: #169 (String/Float64 support, which establishes the heterogeneous-input infrastructure)