[SMT-COMP] SMT-COMP 2015: exit Command Optional

[Tjark Weber]

Dear SMT-COMP participants,

We noticed that many SMT-LIB benchmarks do not contain a final (exit)
command. This affects approximately 58760 benchmarks in the following
main track divisions: LIA, NIA, QF_BV, QF_FP, QF_LIA, QF_LIRA, QF_LRA,
QF_NIA, QF_NIRA, UFBV, UFLIA, and UFNIA.

Moreover, due to the large number of benchmarks affected, it is
unfortunately not feasible to re-release SMT-LIB with final (exit)
commands added, at least not in time for the competition.

Therefore, main track solvers must not assume that benchmarks end with
(exit). Solvers should terminate upon either reading an (exit) command
or reaching the end of the benchmark file. (Note that failure to
terminate may lead to a timeout, which according to Section 7.1 of the
competition rules would result in a benchmark score of 0 even if a
correct result had been generated.)

I would expect that most solvers already implement this behavior. If
your solver currently requires a final (exit) command to terminate,
please consider providing a new solver version until June 14.

Best,
Tjark