[SMT-COMP] Question about benchmarks with unknown status

[Alberto Griggio]

Hello list,

we're writing because we have a question about the candidate set of
benchmarks for the upcoming SMT-COMP. According to the rules, only
benchmarks with known status (sat/unsat) are eligible for the
competition, and this definitely makes sense. However, a big portion of
the new benchmarks recently added to the SMT-LIB are marked as unknown
(for example, those in QF_LIA/nec-smt/large, or in
QF_IDL/schedulingIDL). Therefore, we wanted to know whether there are
any plans to try to determine their status, or if they will just be not
taken into account for the competition. In our opinion, it would be
important to have as many benchmarks as possible in the competition
pool, so it should be tried to assign a status to the unknown
instances. Of course, we are willing to help in this if needed.

Best,

Alberto, Anders, Alessandro and Roberto