[Question]: z3 py in overflow checking for bit-vectors

[hagozaebii]

Hello, recently, I want to use overflow checking functions in z3py.

I can understand bvsaddo and bvuaddo are corresponding to BVAddNoOverflow(signed=True), BVAddNoOverflow(signed=False) each. However, I cannot find functions corresponding to bvssubo and bvusubo. Even though there is a function BVSubNoOverflow however, it does not have singed argument. And, there is a function BVSubNoUnderflow with signed argument. So, I am very confused of what to use for overflow checking in z3 py.

If you are okay, can I know what functions correspond to overflow checking functions?(bvsaddo, bvuaddo, bvssubo, bvusubo, bvsmulo, bvumulo, bvsdivo, bvsnego)

Thanks for your time!

[NikolajBjorner]

Those functions, bvsaddo, bvuaddo, bvssubo, bvusubo, bvsmulo, bvumulo, bvsdivo, bvsnego, were defined in smtlib2 much later than overflow support was added to z3. We haven't created python variants of these or exposed them to build terms. You can add a pull request to add them. The relevant files are in src/api/api_bv.cpp and src/api/z3_api.h and the corresponding python files.