Я новичок в Z3 и проверял онлайн-учебник по Python.
Затем я подумал, что могу проверить поведение переполнения в BitVecs.
Я написал этот код:
x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
и я ожидал [y = 7, x = 7] (т.е. когда значения равны, но преемники не равны, потому что x + 1 будет 0, а y + 1 будет 8)
Но Z3 отвечает [y = 0, x = 0].
Что я делаю неправильно?
Я не думаю, что вы делаете что-то неправильно, похоже, что BV2Int глючит:
x = BitVec('x', 3)
prove(x <= 3)
prove(BV2Int(x) <= 3)
Z3py доказывает первое, но приводит контрпример x=0 для второго. Это звучит неправильно. (Единственным объяснением может быть какая-то странная штука с Python, но я не понимаю, как это сделать.)
Также обратите внимание, что модель, которую вы получите, будет зависеть от того, рассматривает ли + битовый вектор как число со знаком в привязках Python, что, я считаю, имеет место. Однако BV2Int может этого не делать, рассматривая его как беззнаковое значение. Это еще больше усложнило бы дело.
В любом случае, похоже, что BV2Int не совсем кошерно; Я бы держался подальше от этого, пока не будет официального ответа от людей Z3.
Для других, кто обеспокоен этим, в какой-то момент это, похоже, было решено. Я только что повторно запустил этот пример с последней версией z3 (через несколько лет после первоначального сообщения), и он действительно возвращает 7,7.
