Looping over a dynamically sized array

May 23, 2014 at 7:51 AM
I asked this question on StackOverflow, but I haven't received a good answer yet: http://stackoverflow.com/questions/23728786/how-to-loop-over-array-in-z3py

Essentially I have this code that hard codes the lengths of the username and password arrays, but I want Z3 to figure out what those sizes should be:
from z3 import *

s = Solver()
sum = 0
name = Array('name', BitVecSort(32), BitVecSort(32))
i = Int('i')

for i in xrange(0, 1):
    s.add(name[i] >= 65)
    s.add(name[i] < 127)
    if name[i] > 90:
        sum += name[i] - 32
    else:
        sum += name[i]
r1 = sum ^ 0x5678

passwd = Array('passwd', BitVecSort(32), BitVecSort(32))
r2 = 0
for i in xrange(0, 5):
    s.add(passwd[i] < 127)
    s.add(passwd[i] >= 48)
    c = passwd[i] - 48
    r2 *= 10
    r2 += c
r2 ^= 0x1234

s.add(r1 == r2)

print s.check()
print s.model()