[SMT-LIB] QF_BV and division by zero

[Christoph Wintersteiger]

Fantastic, another +1 from me :)

Christoph


Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Alberto Griggio
Sent: 15 October 2015 09:04
To: Clark Barrett <barrett at cs.nyu.edu>; smt-lib <smt-lib at cs.nyu.edu>
Subject: Re: [SMT-LIB] QF_BV and division by zero

Hi Clark,

> Hi all,
>
> We've had many discussions about the semantics of division by zero in 
> the bit-vector theory.  After the most recent discussion at the SMT 
> workshop, it became clear that the arguments for fixing an 
> interpretation seem to outweigh the arguments for the current 
> semantics.  So, we are proposing to change the semantics of bit-vector 
> division so that division by zero produces a vector of all 1's.  The rationale is:

[...]

> A new version of bit-vectors with this proposed change will be 
> available for comment soon.  In the meantime, feedback is welcome.

A big +1 from me (as you might know :-)

Alberto
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.cs.nyu.edu%2fmailman%2flistinfo%2fsmt-lib&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c36b5e03c433840614fb008d2d53781d7%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=9Y2vkFcSILJcErEoXsIQuW9c2br%2bzK%2bwru3CxsGCpyY%3d