z3 test case generator does not converge for data dependent fields of large types

[Smfakhoury]

Test case generator does not converge with data dependent fields larger than UINT16, e.g.:

typedef struct _Foo
{
UINT32 DataLen;
UINT8 DependentField[:byte-size DataLen];
} Foo;