Z3 has APIs for the signed and unsigned interpretations.
For example, in the C API, Z3_mk_bvslt
creates the signed less than, and Z3_mk_bvult
the unsigned one. In Z3Py, we overloaded <
, <=
, ... using the signed ones. For creating, the unsigned a < b
, we have to use ULT(a,b)
. Here is the list of unsigned operators: ULE
(<=
), ULT
(<
), UGE
(>=
), UGT
(>
), UDiv
(unsigned division), URem
(unsigned remainder). You can find more information here:
http://research.microsoft.com/en-us/um/redmond/projects/z3/namespacez3py.html