[SMT-COMP] [SMT-LIB] QF_BV and division by zero

Clark Barrett barrett at cs.stanford.edu
Thu May 4 22:36:17 EDT 2017

Hi all,

Changes have been made to the theory of bitvectors.  Specifically, bvudiv
now returns a vector of all 1's if the second operand is 0 and bvurem
returns its first operand if the second operand is 0 (note that this also
affects the operators defined in terms of these two).  This is detailed in
the online descriptions of the theory FixedSizeBitVectors and the logic
QF_BV, both available on the smtlib.org website.  Before the benchmark
release on June 1, all benchmarks will be checked and their statuses
updated if affected by these changes.


More information about the SMT-COMP mailing list