исключение квантора по битовым векторам дает слишком сложные результаты

Я использую функцию ELIM_QUANTIFIERS Z3, чтобы исключить кванторы из формул над битовыми векторами. Я столкнулся со следующей ситуацией, когда Z3 дает правильный, но слишком сложный результат, и мне было интересно, существует ли способ переписать мою проблему или, возможно, вариант конфигурации, который приведет к простому результату, которого я ожидал.

Во-первых, вот пример, который работает так, как ожидалось. В нем говорится, что для битового вектора длины 4 существует битовый вектор, равный ему.

(set-option ELIM_QUANTIFIERS true)
(declare-fun a () BitVec[4])
(simplify (exists ((x BitVec[4])) 
          (= a x)))

Z3 генерирует следующий вывод для этого примера.

success
success
true

Однако, если я добавлю отрицание:

(set-option ELIM_QUANTIFIERS true)
(declare-fun a () BitVec[4])
(simplify (exists ((x BitVec[4])) 
          (not (= a x))))

затем Z3 производит следующий вывод, в котором перечислены все возможные значения вектора вместо того, чтобы просто вернуть «истина».

success
success
(let (($x54 (= (_ bv0 4) a)))
(let (($x55 (not $x54)))
(let (($x61 (= (_ bv2 4) a)))
(let (($x62 (not $x61)))
(let (($x68 (= (_ bv6 4) a)))
(let (($x69 (not $x68)))
(let (($x75 (= (_ bv4 4) a)))
(let (($x76 (not $x75)))
(let (($x82 (= (_ bv12 4) a)))
(let (($x83 (not $x82)))
(let (($x89 (= (_ bv8 4) a)))
(let (($x90 (not $x89)))
(let (($x95 (= (_ bv1 4) a)))
(let (($x96 (not $x95)))
(let (($x102 (= (_ bv5 4) a)))
(let (($x103 (not $x102)))
(let (($x109 (= (_ bv13 4) a)))
(let (($x110 (not $x109)))
(let (($x116 (= (_ bv9 4) a)))
(let (($x117 (not $x116)))
(let (($x123 (= (_ bv3 4) a)))
(let (($x124 (not $x123)))
(let (($x130 (= (_ bv7 4) a)))
(let (($x131 (not $x130)))
(let (($x137 (= (_ bv14 4) a)))
(let (($x138 (not $x137)))
(let (($x144 (= (_ bv10 4) a)))
(let (($x145 (not $x144)))
(let (($x151 (= (_ bv11 4) a)))
(let (($x152 (not $x151)))
(let (($x158 (= (_ bv15 4) a)))
(let (($x159 (not $x158)))
(or $x159 $x152 $x145 $x138 $x131 $x124 $x117 $x110 $x103 $x96 $x90 $x83 $x76 $x69 $x62 $x55)))))))))))))))))))))))))))))))))

Для более длинных битовых векторов, например, размером 32 или более, Z3 не дает результата за разумное время, поскольку он предположительно перечисляет все возможные значения 32-битной переменной.

Обратите внимание, что в этом конкретном случае я мог бы просто использовать check-sat, чтобы проверить правильность формулы; однако в общем случае меня интересует получение бескванторного выражения, эквивалентного исходной формуле, а не просто проверка его достоверности.

Я использую Z3 v3.2 для Linux.