[SMT-COMP] SMT-COMP 2016: Unsat-core Track Test Jobs

[Matthias Heizmann]

Dear SMT-COMP participants,

I run two test jobs for the Unsat-core Track.

Out of curiosity, I first run an "inofficial" Unsat-core Track test 
on a very small subset of benchmarks in which I also included 
all 27 solvers that participate in the Main Track.
https://www.starexec.org/starexec/secure/details/job.jsp?anonId=104f9dee-e863-4a77-8372-c338c98ef2cc
(For simplicity each solver was used in each division.)

The test showed that not only SMTInterpol which was registered for the 
Unsat-core Track but also four other solvers produce unsat-cores.
These four solvers are MathSAT, toysmt, veriT, and Z3.

My plan is to add these four solvers as non-competitive participants to the 
Unsat-core Track. Each solver will participate in the division in which
it participated in the Main Track.

Using these five solvers (SMTInterpol + four non-competitive Unsat-core 
Track participants) I run another test on a larger subset of benchmarks 
with 5 min timeout.
https://www.starexec.org/starexec/secure/details/job.jsp?anonId=104f9dee-e863-4a77-8372-c338c98ef2cc

If you are interested, please have a look at the results and let me know
if there are any problems.


The best way to have a look at the results is to download the 
"job information". This is a CSV file that lists information for each
solver-benchmark job pair.

Most of the columns in the CSV file should be self-explaining the others
have the following meaning.

- reduction
The reduction is the number that defines the score of the solver in case
the result is not erroneous. The reduction is the difference between the 
number of assert commands in the benchmark file and the size of the 
unsat-core.

- parsable-unsat-core
This value is 'true' iff our post-processor was able to recognize an 
unsat-core in the solver's output.
Sometimes this value is 'false'. In all cases that I checked the reason was 
that the solver returned just 'unsat' but did not output an unsat-core.

- validation-check-sat-response
In order to validate if the unsat-core returned by the solver is correct the 
post-processor produces a "validation script".
The validation script is similar to the solver's input but all assert command
that are not in the unsat-core are removed. The post-processor uses the
non-competitive Main Track participant Z3 to determine the status
of the validation script.

- result-is-erroneous
The result is considered error free (value 0) if the solver's check-sat 
response was not 'sat' and the determined status of the validation script
was not 'sat'.

Best,
Matthias
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part.
URL: </pipermail/smt-comp/attachments/20160608/3ed4f41d/attachment.asc>