Search code examples
pythonarraysz3smtformal-verification

An array of a certain size in z3

I'm using the z3py library for a program verification project, and would like to encode accesses to arrays in z3. Is there a simple way to make the Array z3type have a certain size, say, 112 entries for instance? I'm thinking of something like: A = Array('A', IntSort(), size)

Thanks,

Solution

  • If you want an array with 112 integer elements, you should declare it as

    A = IntVector('A', 112)