SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2017

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Unsat Core Track (Summary)

Competition results as of Tue Jul 18 22:06:21 GMT

Logic Solvers Benchmarks Order (sequential performance)
Order (parallel performance)
QF_AUFBV 3 25 mathsat-5.4.1n; z3-4.5.0n; CVC4
mathsat-5.4.1n; z3-4.5.0n; CVC4
AUFNIRA 2 1050 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
AUFLIA 2 3 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
UFIDL 2 57 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
UF 2 3316 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
QF_UFNRA 2 11 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_UFNIA 2 7 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_NIRA 2 2 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_BVFP 1 3174 z3-4.5.0n
z3-4.5.0n
UFLRA 2 10 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_IDL 3 816 z3-4.5.0n; CVC4; SMTInterpol
z3-4.5.0n; CVC4; SMTInterpol
QF_RDL 3 113 z3-4.5.0n; CVC4; SMTInterpol
z3-4.5.0n; CVC4; SMTInterpol
QF_UFBV 3 31 mathsat-5.4.1n; z3-4.5.0n; CVC4
mathsat-5.4.1n; z3-4.5.0n; CVC4
QF_BV 3 23732 mathsat-5.4.1n; z3-4.5.0n; CVC4
mathsat-5.4.1n; z3-4.5.0n; CVC4
QF_LRA 4 671 SMTInterpol; z3-4.5.0n; mathsat-5.4.1n; CVC4
SMTInterpol; z3-4.5.0n; mathsat-5.4.1n; CVC4
QF_LIA 4 2844 SMTInterpol; z3-4.5.0n; mathsat-5.4.1n; CVC4
z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4
UFLIA 2 7714 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
NIA 2 4 CVC4; z3-4.5.0n
z3-4.5.0n; CVC4
QF_ANIA 2 8 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
QF_ABV 3 4673 z3-4.5.0n; CVC4; mathsat-5.4.1n
z3-4.5.0n; CVC4; mathsat-5.4.1n
QF_UF 4 4101 CVC4; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n
CVC4; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n
QF_AX 4 279 z3-4.5.0n; SMTInterpol; CVC4; mathsat-5.4.1n
z3-4.5.0n; SMTInterpol; CVC4; mathsat-5.4.1n
QF_AUFNIA 2 12 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_NRA 2 5296 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
QF_UFIDL 3 322 z3-4.5.0n; SMTInterpol; CVC4
z3-4.5.0n; SMTInterpol; CVC4
AUFLIRA 2 19771 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
BV 2 94 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
LIA 2 233 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
QF_UFLRA 4 511 mathsat-5.4.1n; z3-4.5.0n; SMTInterpol; CVC4
mathsat-5.4.1n; z3-4.5.0n; SMTInterpol; CVC4
QF_NIA 2 3130 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_LIRA 3 5 z3-4.5.0n; CVC4; SMTInterpol
z3-4.5.0n; CVC4; SMTInterpol
UFBV 2 97 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
UFNIA 2 2432 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
QF_ALIA 4 80 z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4
z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4
ALIA 2 41 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_UFLIA 4 183 z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4
z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4
QF_FP 1 20028 z3-4.5.0n
z3-4.5.0n
NRA 2 3801 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_AUFLIA 4 516 CVC4; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n
CVC4; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n
LRA 2 1106 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n

n. Non-competing.