Dear SMT users and developers,
There has been renewed requests to introduce within SMT-LIB some overflow predicates for bit vectors, i.e., predicates indicating if the result of an operation on bit vectors is not corresponding to the expected integer, because of the fixed bit width. Impacted operations are: neg, add, sub, mul, div.
According to the initial request, we plan to introduce the following predicates:
with the same arguments as the corresponding operations, returning true if there is an overflow, and false if not. We do not plan to distinguish whether the result is over or below the expected value. We plan this evolution both for the 2.6 and the 3.0 versions of SMT-LIB.
We solicit comments on this by the end of January 2023. If there are no objections by then, we will proceed in adding those functions in the relevant logics and theories.
Thanks for your feedback!
Happy holidays to All,
Cesare, Clark, Pascal
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/6fb3655e-13cb-9518-0e7e-3e067ffef9d2%40uliege.be.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/AF1CDAA4-40C1-4D8B-8734-3E536D928DB6%40uiowa.edu.