[SMTCOMP] request for comment

[Hossein Sheini]

Dear Aaron,

First I would like to thank all of you for the very successful competition you
held in 2005. I participated in SMT-COMP'05 with my solver, Ario.

I just have a few comments/suggestions for the SMT-COMP'06, as follows:

1. I think it is very helpful to have your method for selecting benchmarks from
the benchmark pool as described in your "Benchmark Selection" section. However,
I do have a question on how the organizers are going to determine the difficulty
of each benchmark considering that different solvers perform differently on
those benchmarks. My suggestion is to use the average data as collected in
SMT-COMP'05 to regulate that decision.

2. There were instances in SMT-COMP'05 that were added at the last minute, not
included in the released final version of benchmarks suites, i.e.
check/int_incompleteness2.smt. I just wanted to suggest that if the same could
happen this time, it is better to be mentioned in the documents that all
solvers are required to be able to read the SMT header format (like note,
comment, etc sections) correctly.

3. In SMT-COMP'05, there were a few solvers that performed buggy in many
instances. My suggestion is to set up a rule that if a solver passed a
threshold in the number of bugs, it should be eliminated from the competition
because I dont know how its performance on those instances that it had no bugs
can be trusted. (example of such solver is the performance of HTP in QF_LRA
category considering its buggy performance in other categories)

4. I am very much excited about the short presentation as suggested for
SMT-COMP'06. I think it is a very good idea and gives everyone an opportunity
to get to know the spec of other solvers after seeing their performance.

I do appreciate your effort and would like to say that it played an important
role for me to get to know the weaknesses and advantages of my solver better
and to focus my work accordingly.

I also would like to express my interest to get more involved in the SMT
community and help by any means in any of these activities.

with best wishes,

Hossein Sheini
EECS PhD Candidate
University of Michigan at Ann Arbor
www.eecs.umich.edu/~hsheini


Quoting Aaron Stump <stump at cse.wustl.edu>:

> Dear SMT-COMP interest group,
>
> A month ago or so we sent out our current working draft of the SMT-COMP
> rules for 2006 for your comment.  We have received very little feedback
> as of yet, and we would really appreciate your input.  So if you haven't
> already done so, please take a moment to look at the draft and let us
> know any changes you think should be made.  We will prepare the final
> version of the rules soon, so please give us your comments no later than
> February 1.  The draft rules are attached below.
>
> Best wishes,
> Aaron Stump
> (writing also for Clark Barrett and Leonardo de Moura)
>
>