z3py: почему время проверки меняется так сильно после переименования переменной?

Question

Я заметил, что время проверки моих логических формул, написанных на z3py, сильно изменилось (от ~ 60 с до ~ 30 с, около 50%) после того, как я удалил «-» в именах переменных, которые я определил.

Е.Г.,

vec = IntVector('vec-1',10) 

в

vec = IntVector('vec1',10) 

Ожидается, это что-то? Если да, то почему?

Answer 1

Возможно, одна из этих форм имеет столкновение имен. В этом случае Z3 ссылается на одну и ту же константу дважды вместо того, чтобы бросать ошибку. Таким образом, вы решаете другую формулу.