search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Add divide-by-zero bitvec tests #48

Closed aytey closed 5 years ago

aytey commented 5 years ago

As noted in #47, Boolector has no (explicit) tests for validating division when the divisor is zero.

This PR duplicates the test_udiv_bitvec test to create test_udiv_bitvec_zero where the second operand is force to be 0.

aniemetz commented 5 years ago

Fixed a bit differently in https://github.com/Boolector/boolector/commit/f689fbbfe820392d35e26be368f9d87d2dbdb037 (see #47).