[SMT-LIB] QF_BV and division by zero

[Armin Biere]

With (bvurem x 0) = x we also get that bvurem is surjective.
Otherwise ~0 can not be produced (we came across this during
our work on local search with propagation).  So it seems more
natural from this side too.

Armin

On Tue, Apr 4, 2017 at 10:31 AM, Vijay Ganesh <vijay.ganesh at uwaterloo.ca>
wrote:

> I agree. From my perspective, Bruno nailed the argument nicely.
>
> Cheers,
> Vijay Ganesh.
> https://ece.uwaterloo.ca/~vganesh
>
> ________________________________________
> From: smt-lib-bounces at cs.nyu.edu [smt-lib-bounces at cs.nyu.edu] on behalf
> of Aina Niemetz [aina.niemetz at jku.at]
> Sent: Tuesday, April 04, 2017 3:58 AM
> To: Alberto Griggio; Bruno Dutertre; Clark Barrett; Martin Nyx Brain
> Cc: Trevor Hansen; smt-lib at cs.nyu.edu
> Subject: Re: [SMT-LIB] QF_BV and division by zero
>
> I also agree with Bruno.
>
> Aina
>
>
> On 04/04/2017 08:39 AM, Alberto Griggio wrote:
> >> From an implementation point of view, the simplest approach is one that
> >> avoids special treatments for division by zero and makes things
> >> uniform.
> >
> > [snip]
> >
> > I agree with Bruno.
> >
> > Alberto
> > _______________________________________________
> > SMT-LIB mailing list
> > SMT-LIB at cs.nyu.edu
> > http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> >
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>