[SMT-LIB] QF_BV and division by zero

[Vijay Ganesh]

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
>