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

Main Track (Summary)

Competition results as of Fri Jul 21 10:18:02 GMT

Logic Solvers Benchmarks # pairs Complete % Complete Order (sequential performance)
Order (parallel performance)
ALIA 4 42 168 100 z3-4.5.0n; CVC4; vampire 4.2; veriT
z3-4.5.0n; CVC4; vampire 4.2; veriT
AUFBVDTLIA 1 1709 1709 100 CVC4
CVC4
AUFDTLIA 2 728 1456 100 CVC4; vampire 4.2
CVC4; vampire 4.2
AUFLIA 4 4 16 100 CVC4; veriT; z3-4.5.0n; vampire 4.2
CVC4; vampire 4.2; veriT; z3-4.5.0n
AUFLIRA 4 20011 80044 100 z3-4.5.0n; vampire 4.2; CVC4; veriT
z3-4.5.0n; vampire 4.2; CVC4; veriT
AUFNIRA 3 1480 4440 100 vampire 4.2; CVC4; z3-4.5.0n
vampire 4.2; CVC4; z3-4.5.0n
BV 4 5150 20600 100 z3-4.5.0n; Q3B; Boolector; CVC4
z3-4.5.0n; Q3B; Boolector; CVC4
LIA 4 388 1552 100 z3-4.5.0n; CVC4; vampire 4.2; veriT
z3-4.5.0n; CVC4; vampire 4.2; veriT
LRA 5 2419 12095 100 z3-4.5.0n; CVC4; veriT+Redlog; Redlog; vampire 4.2
z3-4.5.0n; CVC4; veriT+Redlog; Redlog; vampire 4.2
NIA 3 14 42 100 z3-4.5.0n; CVC4; vampire 4.2
z3-4.5.0n; CVC4; vampire 4.2
NRA 5 3811 19055 100 Redlog; veriT+Redlog; z3-4.5.0n; vampire 4.2; CVC4
Redlog; veriT+Redlog; z3-4.5.0n; vampire 4.2; CVC4
QF_ABV 5 15061 75305 100 Boolector; Yices2; CVC4; z3-4.5.0n; mathsat-5.4.1n
Boolector; Yices2; CVC4; z3-4.5.0n; mathsat-5.4.1n
QF_ALIA 6 139 834 100 Yices2; mathsat-5.4.1n; SMTInterpol; CVC4; z3-4.5.0n; veriT
Yices2; mathsat-5.4.1n; SMTInterpol; CVC4; z3-4.5.0n; veriT
QF_ANIA 2 8 16 100 CVC4; z3-4.5.0n
CVC4; z3-4.5.0n
QF_AUFBV 5 31 155 100 mathsat-5.4.1n; Yices2; CVC4; Boolector; z3-4.5.0n
mathsat-5.4.1n; Yices2; CVC4; Boolector; z3-4.5.0n
QF_AUFLIA 6 1009 6054 100 Yices2; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4; veriT
Yices2; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4; veriT
QF_AUFNIA 2 17 34 100 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
QF_AX 5 551 2755 100 Yices2; mathsat-5.4.1n; z3-4.5.0n; CVC4; SMTInterpol
Yices2; mathsat-5.4.1n; z3-4.5.0n; CVC4; SMTInterpol
QF_BV 10 40043 400430 100 Boolector+CaDiCaL; Boolector; MinkeyRink; stp_st; stp_mt; z3-4.5.0n; CVC4; Yices2; Q3B; mathsat-5.4.1n
MinkeyRink; Boolector+CaDiCaL; Boolector; stp_mt; stp_st; CVC4; z3-4.5.0n; Yices2; Q3B; mathsat-5.4.1n
QF_BVFP 2 17215 34430 100 z3-4.5.0n; COLIBRI
z3-4.5.0n; COLIBRI
QF_DT 1 8000 8000 100 CVC4
CVC4
QF_FP 3 40302 120906 100 z3-4.5.0n; COLIBRI; xsat
z3-4.5.0n; COLIBRI; xsat
QF_IDL 5 2193 10965 100 Yices2; z3-4.5.0n; CVC4; veriT; SMTInterpol
Yices2; z3-4.5.0n; CVC4; veriT; SMTInterpol
QF_LIA 7 6141 42987 100 mathsat-5.4.1n; CVC4; Yices2; SMTInterpol; z3-4.5.0n; SMTRAT; veriT
mathsat-5.4.1n; CVC4; Yices2; SMTInterpol; z3-4.5.0n; SMTRAT; veriT
QF_LIRA 5 7 35 100 z3-4.5.0n; Yices2; CVC4; SMTRAT; SMTInterpol
z3-4.5.0n; Yices2; CVC4; SMTRAT; SMTInterpol
QF_LRA 8 1649 13192 100 CVC4; Yices2; SMTInterpol; veriT; mathsat-5.4.1n; z3-4.5.0n; SMTRAT; opensmt2
CVC4; Yices2; SMTInterpol; veriT; mathsat-5.4.1n; z3-4.5.0n; SMTRAT; opensmt2
QF_NIA 5 23876 119380 100 CVC4; Yices2; z3-4.5.0n; SMTRAT; AProVE
CVC4; Yices2; z3-4.5.0n; SMTRAT; AProVE
QF_NIRA 4 3 12 100 SMTRAT; z3-4.5.0n; CVC4; Yices2
SMTRAT; z3-4.5.0n; CVC4; Yices2
QF_NRA 5 11354 56770 100 Yices2; z3-4.5.0n; veriT+raSAT+Redlog; SMTRAT; CVC4
Yices2; z3-4.5.0n; veriT+raSAT+Redlog; SMTRAT; CVC4
QF_RDL 5 255 1275 100 Yices2; CVC4; veriT; z3-4.5.0n; SMTInterpol
Yices2; CVC4; veriT; z3-4.5.0n; SMTInterpol
QF_UF 7 6650 46550 100 Yices2; veriT; CVC4; opensmt2; z3-4.5.0n; mathsat-5.4.1n; SMTInterpol
Yices2; veriT; CVC4; opensmt2; z3-4.5.0n; mathsat-5.4.1n; SMTInterpol
QF_UFBV 5 31 155 100 Boolector; Yices2; CVC4; mathsat-5.4.1n; z3-4.5.0n
Boolector; Yices2; CVC4; mathsat-5.4.1n; z3-4.5.0n
QF_UFIDL 5 428 2140 100 Yices2; z3-4.5.0n; SMTInterpol; veriT; CVC4
Yices2; z3-4.5.0n; SMTInterpol; veriT; CVC4
QF_UFLIA 6 583 3498 100 Yices2; z3-4.5.0n; CVC4; SMTInterpol; mathsat-5.4.1n; veriT
Yices2; z3-4.5.0n; CVC4; SMTInterpol; mathsat-5.4.1n; veriT
QF_UFLRA 6 1284 7704 100 Yices2; z3-4.5.0n; mathsat-5.4.1n; veriT; CVC4; SMTInterpol
Yices2; z3-4.5.0n; mathsat-5.4.1n; veriT; CVC4; SMTInterpol
QF_UFNIA 3 7 21 100 Yices2; CVC4; z3-4.5.0n
Yices2; CVC4; z3-4.5.0n
QF_UFNRA 4 36 144 100 z3-4.5.0n; Yices2; CVC4; veriT+raSAT+Redlog
z3-4.5.0n; Yices2; CVC4; veriT+raSAT+Redlog
UF 4 7562 30248 100 vampire 4.2; CVC4; veriT; z3-4.5.0n
vampire 4.2; CVC4; veriT; z3-4.5.0n
UFBV 2 200 400 100 z3-4.5.0n; CVC4
z3-4.5.0n; CVC4
UFDT 2 4535 9070 100 CVC4; vampire 4.2
CVC4; vampire 4.2
UFDTLIA 2 303 606 100 vampire 4.2; CVC4
vampire 4.2; CVC4
UFIDL 4 68 272 100 CVC4; z3-4.5.0n; veriT; vampire 4.2
CVC4; z3-4.5.0n; veriT; vampire 4.2
UFLIA 4 10136 40544 100 CVC4; vampire 4.2; veriT; z3-4.5.0n
CVC4; vampire 4.2; veriT; z3-4.5.0n
UFLRA 4 15 60 100 z3-4.5.0n; CVC4; veriT; vampire 4.2
z3-4.5.0n; CVC4; vampire 4.2; veriT
UFNIA 3 3308 9924 100 vampire 4.2; CVC4; z3-4.5.0n
vampire 4.2; CVC4; z3-4.5.0n

n. Non-competing.