[SMT-COMP] QF_BV: Division by zero

[Johannes Waldmann]

Speaking of partial functions - I'd very much want QF_BV to have
non-overflowing arithmetic operations (plus, times).
(that is, overflow leading to unsatisfiability.)

Since this is currently not available,
I have to use extra constraints to check for overflow.
This complicates the formula, and probably makes it harder
for the solvers. Instead it should be easier?

- Johannes.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : /pipermail/smt-comp/attachments/20090708/86888491/signature.bin