[Smtcomp-discussion] benchmarks involving divide by zero

[David C. <dc...@gr...>]

There was some discussion among some participants and adjustment of 
benchmark results for some QF_BV benchmarks that had divide-by-zero. 
This email is to make sure that all participants for whom this is 
relevant are OK with the outcome. If not, please respond promptly with 
your concerns.

- David

------------------------------ part of the email thread

I've updated new versions with corrected status attributes for the 
QF_BV/spear/w_get benchmarks (corrected according to the current SMT-LIB 
standard).  As mentioned in the discussion thread, the other benchmarks 
in question appear to be labeled correctly - it is just that some 
solvers do not give the right answer.
-Clark


On Mon, Jun 9, 2014 at 3:27 PM, Morgan Deters <md...@cs... 
<mailto:md...@cs...>> wrote:

    On Mon, Jun 9, 2014 at 2:39 PM, Morgan Deters <md...@cs...
    <mailto:md...@cs...>> wrote:

        A follow-up.

        A recent build of Z3 (checked out from their git repository) now
        agrees with the SMT-EVAL versions of Boolector and CVC4 on the
        asp/TravellingSalesperson cases (answering sat).  Modern CVC4
        also gives sat (and verifies its model internally).

        On the spear/wgets, there is still disagreement.  Modern CVC4
        continues to say sat; I'm investigating.


    Liana Hadarean was able to investigate this matter further.  We
    believe that the spear/wget differing results are due to bitvector
    division.  Z3 can be made to leave division-by-zero uninterpreted
    with the parameter HI_DIV0=true, and when it does so, it agrees with
    CVC4's result.  When CVC4 is made to interpret division-by-zero as a
    constant, it agrees with Z3.

    This means that some of the spear/wgets appear to have an incorrect
    status.

    Liana also confirmed my determination of the
    asp/TravellingSalesperson ones, showing that (the outdated) Z3 was
    giving incorrect results.

    Morgan
    -- 
    Morgan Deters
    Senior Research Scientist
    Courant Institute of Mathematical Sciences
    251 Mercer St., New York, NY 10012
    md...@cs... <mailto:md...@cs...> -
    http://cs.nyu.edu/~mdeters/ <http://cs.nyu.edu/%7Emdeters/>