[SMT-LIB] overflow checking for bit-vectors

[Johannes Waldmann]

> The general idea is to have overflow-checking predicates, which can sometimes 
> be implemented more efficiently than the obvious way of doing it.

+1

I would use these.

In fact I do already,
since Boolector has them in its API.

Actually my use case is non-overflowing arithmetics,
so I always apply the checking predicate after the operation,
and that could be implemented still more efficiently?

- Johannes.