Check for overflow on bitvector operations

[fabriceleal]

This is probably more of an open ended question, not particular to z3 (since bitvector theory is described in smt-lib), but do I need to roll my own bitvector arithmetic to track the carry bit, to check for overflows ?

[NikolajBjorner]

The API supports creating predicates for over-and under-flow conditions.
The SMTLIB2 is extended with the few operations that cannot be easily encoded.
They are:
"bvumul_noovfl"
"bvsmul_noovfl"
"bvumul_noudfl"
they take two arguments.
The semantics is described in the header file for z3_api.h (also in auto-generated documentation).

To specifically address carry bits: for addition you can just 0-extend bit-vector arguments by one. Then check that the most significant bit in the output is 0. SMTLIB2 syntax lets you do all of this and you can also declare functions to perform this using SMTLIB2 if that works better for you.
If you need guidance on implementing the under/overflow conditions using existing primitives, take a look at
https://github.com/Z3Prover/z3/blob/master/src/api/api_bv.cpp
Admittedly, the code is not adorned by gratuitous comments, but it uses existing API functions to implement extensions.

[fabriceleal]

Interesting, will check these. Thanks!

[nunoplopes]

For inspiration, search for overflow here: https://github.com/AliveToolkit/alive2/blob/master/smt/expr.cpp