[SMT-COMP] SMT-COMP 2019: Call for Comments, Benchmarks, Solvers

[François Bobot]

Le 23/01/2019 à 16:17, Mohamed Iguernlala a écrit :
> This will not require extra resources, but just some
> scripts. Assuming a category 'C' of this track, once all the
> solvers have been ran on the benchmarks in 'C', one could
> classify the solvers using three criteria to identify:
> 
> (1) the best solver answering 'unsat'
> (2) the best solver answering 'sat'
> (3) the best solver overall

I think it is a good idea, because the prover are also used for different means that are interested
more in satisfiability or unsatisfiability cases.

And also without any more resource needed more chance that everybody goes back home with a nice
certificate!

Best,

-- 
François