[SMT-COMP] StarExec questions

François Bobot francois.bobot at cea.fr
Tue Jun 13 07:44:28 EDT 2017


Hi,

Le 12/06/2017 à 16:57, Giles Reger a écrit :
> You are correct that the table summarises the results as given by the post processor. However, I
> don’t always find the numbers in this table that helpful and tend to rely more on the downloaded
> CSV file (see next). For some post processors “wrong” does not always mean an error.

Yes it is very confusing that the main postprocessors (SMT-COMP *) answers wrong when a prover 
solves a benchmark marked as unknown. Does some people uses other post-processors?

Thanks,

-- 
François


More information about the SMT-COMP mailing list