Added by Sergey Smolov over 7 years ago. Updated over 7 years ago.
100%
Description
bv2int converts bit vector argument to integer
int2bv takes integer length parameter and an integer argument and converts it to bit vector of the specified length
Here is a fragment of the header for the newest Z3 release 4.3.5:
- Z3_OP_INT2BV Coerce integer to bit-vector. NB. This function
is not supported by the decision procedures. Only the most
rudimentary simplification rules are applied to this function.
- Z3_OP_BV2INT Coerce bit-vector to integer. NB. This function
is not supported by the decision procedures. Only the most
rudimentary simplification rules are applied to this function.
It seems that CVC4 supports operations that are called bv2nat\int2bv