[SMT-LIB] QF_BV and division by zero

Mon May 1 20:56:51 EDT 2017

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: 
http://www.cs.nyu.edu/pipermail/smt-lib/2008/000255.html

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://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