[SMT-COMP] SMT-COMP 2016: Incorrect Answers (Unknown Track)

Tjark Weber tjark.weber at it.uu.se
Wed Jul 6 14:16:24 EDT 2016


In the "unknown benchmarks" track, we currently have no authoritative
way to tell correct from incorrect answers.

However, there were 603 conflicts (i.e., at least one solver answered
sat and another solver answered unsat) on 79 benchmarks. The following
list shows how often each solver was involved in a conflict:

     25 ABC_default
     25 ABC_glucose
     25 Boolector
     25 Boolector preprop
     55 CVC4-master-2016-05-27-cfef263-main
     22 MapleSTP
     23 MapleSTP-mt
     25 mathsat-5.3.11-linux-x86_64-Main
     25 Minkeyrink  2016
     12 ProB
     27 Q3B
     50 raSAT 0.3
      7 raSAT 0.4 exp - final
     35 SMT-RAT
     25 stp-cms-exp-2016
     25 stp-cms-mt-2016
     25 stp-cms-st-2016
     24 stp-minisat-st-2016
      1 vampire_smt_4.1_parallel
     55 Yices-2.4.2
     67 z3-4.4.1

Again, this does *not* necessarily mean that the solver gave an
incorrect answer, but merely that it disagreed with some other
solver(s).

A more detailed list that includes benchmark information is attached.

Best,
Tjark
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Non-Incremental_Unknown.conflicts.csv
Type: text/csv
Size: 107416 bytes
Desc: not available
URL: </pipermail/smt-comp/attachments/20160706/489cd551/attachment-0001.csv>


More information about the SMT-COMP mailing list