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!

[hagozaebii]

#7221