[SMT-COMP] QF_BV: Division by zero
Clark Barrett
barrett at cs.nyu.edu
Wed Jul 8 17:55:52 EDT 2009
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.
More information about the SMT-COMP
mailing list