[SMT-LIB] QF_BV and division by zero

[Trevor Hansen]

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

______________________________ __________
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