Грешка в атрибута, z3 няма атрибут Ints

Правя символно изпълнение в Python, използвайки модула z3. В някаква част от кода exec се използва за извикване на извикваща функция z3. Кодовият фрагмент е както следва:

def can_be_satisfied(n):
 path = get_path(n)
 my_names, path =to_single_assignment(path)
 s1 = "%s = z3.Ints('%s')" % (', '.join(my_names), ' '.join(my_names))
 exec(s1, globals(), locals())
 s = z3.Solver()
 s2 = 's.add(%s)' % (', '.join([tosrc(i) for i in path]))
 print(s2)
 exec(s2, globals(), locals())
 if s.check() == z3.sat:
    print("sat:", s.model())
    return True
 else:
    return False

Както видях в документацията на z3 модул за Python (http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm), съдържа атрибута "Ints". Въпреки това, след изпълнението на програмата, следната грешка се генерира от фрагмента:

File "code/symbolic_concolic_egt/symbolic/symbolic.py", line 69, in can_be_satisfied
    exec(s1, globals(), locals())
File "<string>", line 1, in <module>     
AttributeError: module 'z3' has no attribute 'Ints'

Всяко предложение как да се реши този проблем е добре дошло. Благодаря ви предварително