quantifier elimination over bit vectors produces overly complicated results

I am using the ELIM_QUANTIFIERS feature of Z3 to eliminate quantifiers from formulas over bit vectors. I ran into the following situation where Z3 produces a correct, yet overly complicated result, and I was wondering whether there exists a way to re-write my problem or perhaps a configuration option that would lead to the simple result I expect.

First, here is an example that works as expected. It states that for a bit vector of length 4 there exists a bit vector that is equal to it.

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

Z3 generates the following output for this example.

success
 success
 true
 

However, if I add a negation:

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

then Z3 produces the following output, which lists all possible values of the vector instead of just returning "true".

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)))))))))))))))))))))))))))))))))
 

For longer bit vectors, e.g., of size 32 or more, Z3 does not produce a result in a reasonable time, as it is presumably enumerating all possible values of the 32-bit variable.

Note that in this particular case I could just use check-sat to check the validity of the formula; however in the general case I am interested in obtaining a quantifier-free expression equivalent to the original formula, rather than just checking its validity.

I am using Z3 v3.2 for Linux.

---