[SMT-COMP] QF_BV: Division by zero

[Clark Barrett]

If you'd like to propose additional operators for QF_BV, I suggest you post
your request to smt-lib at cs.nyu.edu with details about the semantics you would
like to see in the new operators.

-Clark

> 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.