Add srem and sdiv operations on bitvectors
It looks like there exists, in both CVC4 and Z3, operations on 2's complement signed integer for division (BVSDIV) and modulo on bitvectors. For modulo BVSMOD follows the semantic of the modulo in programming language.
I would appreciate if these two operations could be added in the theory of bitvector in addition to the urem
and udiv
operation that are already existing.