[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks
cwinter at microsoft.com
Fri Apr 28 09:54:36 EDT 2017
Yes, I downloaded them (old and new) but haven't committed them to the repository yet. I'll run the latest Z3 over them as well, just to make sure everything's in order.
Just a minor point: Rafael Z?hl's name doesn't render right (when I open the file in emacs). Should I change it to Zaehl?
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
From: Delcypher [mailto:delcypher at gmail.com]
Sent: 28 April 2017 13:55
To: Christoph Wintersteiger <cwinter at microsoft.com>
Cc: Clark Barrett <barrett at cs.stanford.edu>; smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks
On 23 April 2017 at 20:29, Delcypher <delcypher at gmail.com> wrote:
> On 21 April 2017 at 16:06, Christoph Wintersteiger
> <cwinter at microsoft.com> wrote:
>> Hi Dan,
>> Space is free, submit them all! If it turns out there are too many of them, we can let others (e.g. the competition organizers) do the sub-sampling themselves and by their own criteria.
>> In other parts of the library it turned out that we had a bunch of duplicates with different file names (e.g. QF_BV/sage2 if I remember correctly). If there's an easy way for you to filter those, that would be nice.
> Finally! I have the first version of the benchmarks for consideration.
> I'm sorry that this took so long. I had a lot of false starts.
> Good call on asking me to remove duplicates (I used the fdupes tool
> for this). This found a bug in my tool because it is supposed to cache
> query results so for a single run of my tool there should have been no
> duplicates but it turns out were some!
> They are available at
> These have been annotated with
> * The logic
> * Satisfiability if known. This was determined by running Z3 and
> Mathsat5 on the benchmarks before doing any annotation. I suspect the
> `QF_FPABV` logic annotation might confuse the solvers but I've not
> tried. I allowed at most 30 minutes per query
> * A note regarding a corresponding equisatisfiable query if it exists
> A few statistics:
> Number of benchmarks by logic:
> QF_FPABV: 18033 benchmarks
> QF_FPBV: 17156 benchmarks
> Number of benchmarks by satisfiability:
> 28099 sat benchmarks
> 7070 unsat benchmarks
> 20 unknown benchmarks
> Please take a look and let me know if you find any problems. If you or
> others wish to remove benchmarks please discuss this with me first.
> Doing so without care will breaks the comments in the benchmarks
> noting about corresponding equisatisfiable benchmarks in the other
I don't know if you've had a chance to look yet but I noticed I didn't attribute all the authors of the benchmarks that I should have.
I've produced a revised version which fixes this which is available at the link below.
I'm keen to get feedback on this so please take a look. Again if you'd like me to trim down the number of benchmarks I'm happy to do this but I need to the okay from Christoph because he will become the owner of these benchmarks.
More information about the SMT-COMP