[SMT-LIB] Signed comparisons in bit vector theory

[Regis Blanc]

Hello all,

I am trying to use the theory of bit vectors to encode some
properties of java Integers. However, as far as I can tell, the only
comparison operator available in the standard is bvult, which
does an unsigned comparison. I was wondering if there was a standard
way to do signed comparison (negative numbers in two-complement) or
if I had to do my own encoding based on the unsigned comparison and
extracting leading bits?

Thanks,
Regis