SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2018

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Unsat Core Track (Summary)

Competition results as of Thu Jul 12 23:54:00 GMT

Logic Solvers Benchmarks Order (sequential performance)
Order (parallel performance)
ALIA 2 41 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
AUFBVDTLIA 1 25 CVC4
CVC4
AUFLIA 2 3 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
AUFLIRA 2 19771 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
AUFNIRA 2 1053 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
BV 2 4937 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
LIA 2 233 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
LRA 2 1539 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
NIA 2 4 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
NRA 2 3801 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
QF_ABV 4 4677 Yices 2.6.0; z3-4.7.1n; MathSAT-5.5.2n; CVC4
Yices 2.6.0; z3-4.7.1n; MathSAT-5.5.2n; CVC4
QF_ABVFP 1 3934 CVC4
CVC4
QF_ALIA 5 80 z3-4.7.1n; Yices 2.6.0; MathSAT-5.5.2n; SMTInterpol; CVC4
z3-4.7.1n; Yices 2.6.0; MathSAT-5.5.2n; SMTInterpol; CVC4
QF_ANIA 2 8 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
QF_AUFBV 4 25 MathSAT-5.5.2n; Yices 2.6.0; CVC4; z3-4.7.1n
MathSAT-5.5.2n; Yices 2.6.0; CVC4; z3-4.7.1n
QF_AUFLIA 5 516 CVC4; z3-4.7.1n; Yices 2.6.0; MathSAT-5.5.2n; SMTInterpol
CVC4; z3-4.7.1n; Yices 2.6.0; MathSAT-5.5.2n; SMTInterpol
QF_AUFNIA 2 12 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
QF_AX 5 279 Yices 2.6.0; z3-4.7.1n; CVC4; MathSAT-5.5.2n; SMTInterpol
Yices 2.6.0; z3-4.7.1n; CVC4; MathSAT-5.5.2n; SMTInterpol
QF_BV 4 25700 Yices 2.6.0; MathSAT-5.5.2n; CVC4; z3-4.7.1n
Yices 2.6.0; MathSAT-5.5.2n; CVC4; z3-4.7.1n
QF_BVFP 2 3174 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
QF_DT 2 4422 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
QF_FP 2 20026 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
QF_IDL 5 816 z3-4.7.1n; CVC4; Yices 2.6.0; SMTInterpol; MathSAT-5.5.2n
z3-4.7.1n; CVC4; Yices 2.6.0; SMTInterpol; MathSAT-5.5.2n
QF_LIA 5 3019 SMTInterpol; Yices 2.6.0; MathSAT-5.5.2n; z3-4.7.1n; CVC4
SMTInterpol; Yices 2.6.0; MathSAT-5.5.2n; z3-4.7.1n; CVC4
QF_LIRA 4 5 z3-4.7.1n; CVC4; Yices 2.6.0; SMTInterpol
z3-4.7.1n; CVC4; Yices 2.6.0; SMTInterpol
QF_LRA 5 683 SMTInterpol; Yices 2.6.0; z3-4.7.1n; MathSAT-5.5.2n; CVC4
SMTInterpol; Yices 2.6.0; z3-4.7.1n; MathSAT-5.5.2n; CVC4
QF_NIA 2 4842 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
QF_NIRA 2 2 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
QF_NRA 2 5357 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
QF_RDL 5 113 z3-4.7.1n; CVC4; Yices 2.6.0; MathSAT-5.5.2n; SMTInterpol
z3-4.7.1n; CVC4; Yices 2.6.0; MathSAT-5.5.2n; SMTInterpol
QF_UF 5 4330 CVC4; z3-4.7.1n; SMTInterpol; Yices 2.6.0; MathSAT-5.5.2n
CVC4; z3-4.7.1n; SMTInterpol; Yices 2.6.0; MathSAT-5.5.2n
QF_UFBV 4 575 z3-4.7.1n; Yices 2.6.0; MathSAT-5.5.2n; CVC4
z3-4.7.1n; Yices 2.6.0; MathSAT-5.5.2n; CVC4
QF_UFIDL 5 322 Yices 2.6.0; z3-4.7.1n; SMTInterpol; MathSAT-5.5.2n; CVC4
Yices 2.6.0; z3-4.7.1n; SMTInterpol; MathSAT-5.5.2n; CVC4
QF_UFLIA 5 183 z3-4.7.1n; SMTInterpol; Yices 2.6.0; MathSAT-5.5.2n; CVC4
z3-4.7.1n; SMTInterpol; Yices 2.6.0; MathSAT-5.5.2n; CVC4
QF_UFLRA 5 511 MathSAT-5.5.2n; z3-4.7.1n; Yices 2.6.0; SMTInterpol; CVC4
MathSAT-5.5.2n; z3-4.7.1n; Yices 2.6.0; SMTInterpol; CVC4
QF_UFNIA 2 7 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
QF_UFNRA 2 11 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
UF 2 3442 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
UFBV 2 97 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
UFDT 1 1863 CVC4
CVC4
UFIDL 2 57 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
UFLIA 2 7743 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
UFLRA 2 10 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
UFNIA 2 2457 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n

n. Non-competing.