[SMT-LIB] overflow checking for bit-vectors

Johannes Waldmann johannes.waldmann at htwk-leipzig.de
Fri Sep 11 05:17:31 EDT 2015


> 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.



More information about the SMT-LIB mailing list