Optimize signed bitvectors in Z3

I am trying to optimize an expression that consists of bitvectors in Z3 (the code runs in e.g. https://rise4fun.com/Z3/tutorial/optimization):

(declare-const x (_ BitVec 32))
(assert (bvslt x #x00000008))
(maximize x)
(check-sat)
(get-objectives)

The result I get is:

sat
(objectives
  (x 4294967295)
)

which is the maximum int 0xffffffff for 32 bits, which would be signed -1. However, I want to get the signed maximum, i.e. 7. Is there any way to do that in Z3 (apart from making multiple calls to Z3 with different constraints (i.e b&b) as in CVC4 minimize/maximize model optimization)? Does anyone know any other solver (preferably using smtlibv2 input) to do that?

All bit-vectors in SMT are unsigned, but there are special comparison operators like bvslt that have signed semantics. You can add another constraint to enforce that x is positive:

(assert (bvslt #x00000000 x))

It then produces the expected result (7).

Another way to do this is by shifting the numbers up by 2^n-1 (or flipping their first bit), which could then go into the objective function:

(declare-const x (_ BitVec 32))
(assert (bvslt x #x00000008))
(maximize (bvadd x #x80000000))
(check-sat)
(get-objectives)
(get-value (x))

says

sat
(objectives
 ((bvadd x #x80000000) 2147483655)
)
((x #x00000007))