[SMT-LIB] QF_BV and division by zero

[Clark Barrett]

Yes.  I will circulate a new draft of QF_BV early next week.

-Clark

On Tue, Apr 11, 2017 at 11:05 PM, Trevor Hansen <trev_abroad at yahoo.com>
wrote:

> Hi Clark,
>
> I think it's reasonable to go with the majority's preference for the
> division & remainder-by-zero semantics.
>
> Is there still time to get it finalised in time for this year's SMTCOMP?
>
> Thanks,
>
> Trev.
>
>
>
> On Tuesday, 4 April 2017, 21:28, Armin Biere <armin.biere at gmail.com>
> wrote:
>
>
> 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 <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
> <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
> <http://www.cs.nyu.edu/mailman/listinfo/smt-lib>
>
>
>
>
>