Synonym axiom stymies ((_ int2bv n) (bv2int b)) identity

[atomb]

The following SMT-Lib input declares a function nat_from_bv16 and provides an axiom asserting its equivalence to bv2int.

(declare-fun nat_from_bv16 ((_ BitVec 16)) Int)
(assert
  (forall ((b (_ BitVec 16)))
    (! (= (nat_from_bv16 b) (bv2int b))
       :pattern ((nat_from_bv16 b))
    )
  )
)
(declare-fun short () (_ BitVec 16))
(assert (not (= short ((_ int2bv 16) (nat_from_bv16 short)))))
(check-sat)

Neither Z3 4.8.17 or 4.8.14 can prove this (in the time I was willing to wait), nor can 4.8.5 (an old version, but the only one that currently works well with Danfy, where this problem originated).

However, Z3 can easily prove (assert (not (= short ((_ int2bv 16) (bv2int short))))), without the synonym function.

Ultimately, I'm quite happy to accept that there are many integer/bitvector relationships Z3 won't be able to prove, but this seems like one it shouldn't have much trouble with.