[SMT-LIB] QF_BV and division by zero

Tue May 2 07:52:47 EDT 2017

Hi Trevor,

I can confirm that, the status of these four benchmarks changes when enabling the other semantics. I think we should just annotated them as "unknown" until somebody has a closer look at them. 

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | https://www.microsoft.com/en-us/research/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 Trevor Hansen
Sent: 02 May 2017 01:57
To: Clark Barrett <barrett at cs.stanford.edu>
Cc: smt-lib at cs.nyu.edu
Subject: Re: [SMT-LIB] QF_BV and division by zero

Hi Clark, 

I've implemented the proposed semantics in our solver, STP,  and tested against SMTLIB QF_BV. 

I believe that the status of four benchmarks needs to be changed to unsatisfiable, they are:QF_BV/spear/wget_v1.10.2/src_wget_vc18196.smt2
QF_BV/spear/wget_v1.10.2/src_wget_vc18197.smt2
QF_BV/spear/wget_v1.10.2/src_wget_vc18755.smt2
QF_BV/spear/wget_v1.10.2/src_wget_vc18756.smt2

Z3, the version of which I'm using that I believe implements the proposed semantics, gives the same results.
These benchmarks have been discussed previously: 
https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.cs.nyu.edu%2Fpipermail%2Fsmt-lib%2F2008%2F000255.html&data=02%7C01%7Ccwinter%40microsoft.com%7C4cbc0fd1f7e4429c241a08d490f718dc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636292838345298787&sdata=2OXiK0puNSpoPzgcYf%2F0fRcC%2FwiXmplc7n1JQP0dhjI%3D&reserved=0

STP times-out/memory-outs on 42 benchmarks that have a known status and contain mod/div/rem. So I don't know if their result depends on the semantics of division/remainder-by-zero, they are listed below. These benchmarks may be structured to prevent division/remainder-by-zero. But unless someone else checks them, it seems best to me to set their status to unknown?

I've not checked the other affected divisions, e.g. BV, QF_AUFBV, QF_UFBV. Can someone else do this?

Division-by-zero in BV has been a pain for nearly a decade now, I'm looking forward to finally getting it resolved,

Trev.
-----

./QF_BV/bmc-bv-svcomp14/797336/s3_srvr_1_alt_true.BV.c.cil.c.17.smt2
./QF_BV/bmc-bv-svcomp14/797281/s3_srvr_1_alt_true.BV.c.cil.c.21.smt2
./QF_BV/challenge/892054/integerOverflow.smt2
./QF_BV/float/2016958/gaussian.c.125.smt2
./QF_BV/float/2016962/gaussian.c.175.smt2
./QF_BV/float/2016959/gaussian.c.75.smt2
./QF_BV/float/797539/sin2.c.10.smt2
./QF_BV/float/797442/sin2.c.15.smt2
./QF_BV/float/2016963/sin2.c.20.smt2
./QF_BV/log-slicing/815113/bvudiv_25.smt2
./QF_BV/log-slicing/815160/bvsdiv_19.smt2
./QF_BV/log-slicing/815168/bvsdiv_20.smt2
./QF_BV/log-slicing/815218/bvsdiv_21.smt2
./QF_BV/log-slicing/815248/bvsdiv_22.smt2
./QF_BV/log-slicing/815217/bvsdiv_23.smt2
./QF_BV/log-slicing/815185/bvsdiv_24.smt2
./QF_BV/log-slicing/815172/bvsdiv_25.smt2
./QF_BV/log-slicing/815226/bvsmod_17.smt2
./QF_BV/log-slicing/815112/bvsmod_18.smt2
./QF_BV/log-slicing/815239/bvsmod_19.smt2
./QF_BV/log-slicing/815158/bvsmod_20.smt2
./QF_BV/log-slicing/815190/bvsrem_17.smt2
./QF_BV/log-slicing/815235/bvsrem_18.smt2
./QF_BV/log-slicing/815138/bvsrem_19.smt2
./QF_BV/log-slicing/815111/bvsrem_20.smt2
./QF_BV/log-slicing/815146/bvudiv_18.smt2
./QF_BV/log-slicing/815207/bvudiv_19.smt2
./QF_BV/log-slicing/815133/bvudiv_20.smt2
./QF_BV/log-slicing/815150/bvudiv_21.smt2
./QF_BV/log-slicing/815192/bvudiv_22.smt2
./QF_BV/log-slicing/815234/bvudiv_23.smt2
./QF_BV/log-slicing/815246/bvudiv_24.smt2
./QF_BV/log-slicing/815144/bvurem_16.smt2
./QF_BV/log-slicing/815230/bvurem_17.smt2
./QF_BV/log-slicing/815116/bvurem_18.smt2
./QF_BV/log-slicing/815245/bvurem_19.smt2
./QF_BV/log-slicing/815215/bvurem_20.smt2
./QF_BV/log-slicing/815119/bvurem_21.smt2
./QF_BV/log-slicing/815137/bvurem_22.smt2
./QF_BV/galois/368975/iffyInterleavedModMult-128.smt2
./QF_BV/galois/368976/iffyInterleavedModMult-32.smt2
./QF_BV/galois/368978/iffyInterleavedModMult-8.smt2

  Show original message     On Sunday, 16 April 2017, 1:46, Clark Barrett <barrett at cs.stanford.edu> wrote:

 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://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fece.uwaterloo.ca%2F~&data=02%7C01%7Ccwinter%40microsoft.com%7C4cbc0fd1f7e4429c241a08d490f718dc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636292838345308796&sdata=CYibn3bWFbmUB%2BtxbnS5MVKgfRfY7gMgVPvIxno37R8%3D&reserved=0 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
> https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.cs.nyu.edu%2Fmailman%2F&data=02%7C01%7Ccwinter%40microsoft.com%7C4cbc0fd1f7e4429c241a08d490f718dc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636292838345308796&sdata=l5xQcTsyaEK82bO%2Bx3%2BJRlsT8a2bQ%2Fn5O5SulEOna8U%3D&reserved=0 listinfo/smt-lib
>

______________________________ _________________
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%2F&data=02%7C01%7Ccwinter%40microsoft.com%7C4cbc0fd1f7e4429c241a08d490f718dc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636292838345308796&sdata=l5xQcTsyaEK82bO%2Bx3%2BJRlsT8a2bQ%2Fn5O5SulEOna8U%3D&reserved=0 listinfo/smt-lib

_______________________________________________
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=02%7C01%7Ccwinter%40microsoft.com%7C4cbc0fd1f7e4429c241a08d490f718dc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636292838345308796&sdata=SMvotN%2Fx73q79zX5Mang0jC4%2FU4IGCMq4ruDH4Idm1k%3D&reserved=0