Summary

The vera test MVP (v0.0.47, #79) generates inputs for Int, Nat, and Bool parameters via Z3. This issue tracks extending input generation to Float64, String, Array, and ADT parameters.

Float64

Z3 Real is not IEEE 754 -- it represents exact rationals, not floating-point values. Options:

• Use Z3 Real as an approximation and round to the nearest Float64
• Use random generation within precondition-satisfying ranges
• Hybrid: Z3 for constraint solving, random perturbation for IEEE edge cases (NaN, Inf, subnormals)

String, Array, ADT

No Z3 encoding exists for these types. Possible approaches:

• Random structural generation (random strings of bounded length, random arrays of bounded size)
• Grammar-based generation for ADTs (enumerate constructors, recurse on fields)
• Hypothesis strategies for complex types (see #170)

Dependencies

String and Array input generation depends on codegen maturity for those types:

• #134 string built-in operations
• #132 arrays of compound types in codegen
• #154 recursive generic ADT codegen

Follow-up from

• #79 vera test contract-driven testing (v0.0.47)