[SMT-COMP] Question about benchmarks with unknown status

[Alberto Griggio]

Hello Morgan,
thanks for the explanation.

> If you can demonstrate the (un)satisfiability of any of the
> unknown-status benchmarks, please let us know.  We have, in fact,
> determined the status of many of the benchmarks added to SMT-LIB
> recently, though not all of them.
>
> We plan to have updated benchmarks, with current status and difficulty
> information, published by June 1.  They will also be available for
> execution on SMT-Exec.
>
> Currently, in QF_LIA/nec-smt/large, we know 888 to be SAT, 1117 to be
> UNSAT, and 376 remain unknown.  In QF_IDL/schedulingIDL, we have 247
> SAT, 31 UNSAT, and 2 remain unknown.  We may be able to determine a
> few more in the next few days.

I see. What is exactly the procedure to use for determining the status?
Are you simply running one (or more) solver(s) with a very high timeout?
Or is something more needed? (e.g. a model or an unsat core)

Thanks again,
Alberto