======================================================================

    9th International Satisfiability Modulo Theories Competition
                            (SMT-COMP'14)

                             July 18, 2014
                            Vienna, Austria

                           CALL FOR COMMENTS - by 5 Feb 2014
                          CALL FOR BENCHMARKS
                     PRELIMINARY CALL FOR SOLVERS

======================================================================

SMT-COMP is the annual competition among Satisfiability Modulo Theories
(SMT) solvers. The goals of SMT-COMP are to spur solver advances, collect
benchmarks, and encourage adoption of the SMT-LIB standard, through
friendly competition.

SMT-COMP'14 will be held as part of the 'Olympic Games'
at the 'Summer of Logic', in Vienna, Austria (July 9-24).
The SMT competition will end in time to be described and the
results announced at the SMT workshop (July 17-18).
The Olympic Games consists of 12 different competitions in various
aspects of logic.

SMTCOMP'14 is organized under the direction of the SMT Steering
committee. The organizing team for SMTCOMP'14 is
    David Cok - GrammaTech, Inc., USA
    David Deharbe - Federal University of Rio Grande do Norte, Brazil
    Tjark Weber - Uppsala University, Sweden

This is a call for three things:

CALL FOR COMMENTS:
The organizing team is preparing the schedule and rules for 2014.
Any comments you may have to improve the competition over past years
or to redirect its focus are welcome and will be considered by the
team. Please submit such comments by 5 February 2014.

CALL FOR BENCHMARKS:
The competition is enhanced by new sets of benchmarks to add to those
already in use (and used in past competitions). A random selection
of benchmarks in various categories is used for the competition
(according to rules that are currently being revised).

If you have benchmarks that you think would be useful to SMT-LIB
and SMT-COMP (and may be made public), please let us know as soon
as possible, even if the material is not quite ready. The deadline
for benchmarks to be used in the 2014 competition will be announced
when the schedule and rules are finalized.

CALL FOR SOLVERS:
A submission deadline for solvers will be announced along with the
rules. However, it is useful to the team to know which and how many
solvers may be entering. Thus we request that you let us know
if you think you may be submitting one or more solvers to the competition,
particularly if you think there may be unusual circumstances.

COMMUNICATION:
The competition web-site will be at www.smtcomp.org/2014,
once it is up and running.

Public email regarding the competition may be sent to smt-comp@cs.nyu.edu.
Announcements will be sent on both smt-comp@cs.nyu.edu and smt-lib@cs.nyu.edu.

Email to the organizers only may be sent to smtcomp-discussion@lists.sourceforge.net

Sincerely,

The organizing team.