[SMT-COMP] 回复:SMT-COMP Digest, Vol 78, Issue 2

简简单单 122261138 at qq.com
Thu Jun 29 11:06:19 EDT 2017


发件人:"smt-comp-request"<smt-comp-request at cs.nyu.edu>
发送时间:2017年3月18日 星期六 上午0:2
收件人:"smt-comp"<smt-comp at cs.nyu.edu>
主题:SMT-COMP Digest, Vol 78, Issue 2
Send SMT-COMP mailing list submissions to
smt-comp at cs.nyu.edu
To subscribe or unsubscribe via the World Wide Web, visit
or, via email, send a message with subject or body 'help' to
smt-comp-request at cs.nyu.edu
You can reach the person managing the list at
smt-comp-owner at cs.nyu.edu
When replying, please edit your Subject line so it is more specific
than "Re: Contents of SMT-COMP digest..."
Today's Topics:
1. Contribution of QF_FPBV and QF_FPABV benchmarks (Delcypher)
Message: 1
Date: Fri, 17 Mar 2017 13:39:00 +0000
From: Delcypher <delcypher at gmail.com>
To: "smt-comp at cs.nyu.edu" <smt-comp at cs.nyu.edu>
Subject: [SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks
<CANNJ_zjAGB0uY3Dh8-t+JHxUzDWLCrY2fW9R7r2Q_ohPSDJXpA at mail.gmail.com>
Content-Type: text/plain; charset=UTF-8
I just saw the call for benchmarks.
I'd like to state I intend to contribute a set of benchmarks
* Some QF_FPBV benchmarks
* A new category that I suggested some time ago that mixes the
theories of quantifier free floating point and arrays of bitvectors. I
suggest the name QF_FPABV
I should have preliminary version of these benchmarks available in the
next few days.
A few questions:
* Do I need to curate these benchmarks in some way. If so what
criteria should I use? E.g. Should I pick the longest running? I have
quite a few benchmarks (~ 8000) so having that many might not be
* Some benchmarks may use Z3's non-standard fp.to_ieee_bv function. Is
that a problem?
* The QF_FPBV and QF_FPABV benchmarks will be very similar because
they come from the same source (the QF_FPBV benchmarks are QF_FPABV
benchmarks where we have been able to remove arrays using knowledge of
our problem domain). Is this a problem?
* Many benchmarks do not have a known answer. Is that a problem?
* Are there any requirements about what needs to be in the pre-amble
of the smt2 file? (.e.g Does the logic need to be stated?).
SMT-COMP mailing list
SMT-COMP at cs.nyu.edu
End of SMT-COMP Digest, Vol 78, Issue 2

More information about the SMT-COMP mailing list