bvuaddo bvnego etc.

[bclement-ocp]

No description provided.

[hra687261]

Is the idea to properly support them, or to add them by using existing operators as described by their semantics in https://smt-lib.org/theories-FixedSizeBitVectors.shtml?
It seems that adding bv2int is needed, but it can be defined using an ite on the sign bit and bv2nat

[bclement-ocp]

The goal is to properly support them through the DL (once it's merged) or arithmetic solver. I think we want to avoid ite – or at least we want theory propagation to learn when these become true from intervals.