Ошибка атрибута, 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'

Любое предложение о том, как решить эту проблему, приветствуется. заранее спасибо