[SMT-COMP] QF_BV: Division by zero
Johannes Waldmann
waldmann at imn.htwk-leipzig.de
Wed Jul 8 04:54:46 EDT 2009
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
More information about the SMT-COMP
mailing list