Понимание индексации связанных переменных в Z3

Я пытаюсь понять, как связанные переменные индексируются в z3. Вот фрагмент в z3pyи соответствующий вывод.(http://rise4fun.com/Z3Py/plVw1)

x, y = Ints('x y')
f1 = ForAll(x, And(x == 0, Exists(y, x == y)))
f2 = ForAll(x, Exists(y, And(x == 0, x == y)))
print f1.body()
print f2.body()

Выход:

ν0 = 0 ∧ (∃y : ν1 = y)
y : ν1 = 0 ∧ ν1 = y

В f1почему одна и та же связанная переменная xимеет разные индексы.(0и1). Если я изменю f1и выведу Exists, то xбудет иметь тот же индекс(0).

Причина, по которой я хочу понять механизм индексации:

У меня есть формула FOL, представленная в DSL в scala, которую я хочу отправить на z3. Теперь ScalaZ3имеет API mkBoundдля создания связанных переменных, которые принимают indexи sortв качестве аргументов. Я не уверен, какое значение я должен передать аргументу index. Итак, я хотел бы знать следующее:

Если у меня есть две формулы phi1и phi2с максимальными индексами связанных переменных n1и n2, каким будет индекс xвForAll(x, And(phi1, phi2))

Кроме того, есть ли способ показать все переменные в индексированной форме? f1.body()просто показывает мне xв индексированной форме, а не y. (Я думаю, причина в том, что yвсе еще связан вf1.body())