SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2018

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Summary

Main Track

Competition results as of Fri Jul 13 00:02:11 GMT

Logic Solvers Benchmarks # pairs Complete % Complete Order (sequential performance)
Order (parallel performance)
ABVFP 1 1 1 100 CVC4
CVC4
ALIA 5 42 210 100 z3-4.7.1n; CVC4; Alt-Ergo; veriT; Vampire 4.3
z3-4.7.1n; CVC4; Alt-Ergo; Vampire 4.3; veriT
AUFBVDTLIA 1 1709 1709 100 CVC4
CVC4
AUFDTLIA 2 728 1456 100 CVC4; Vampire 4.3
CVC4; Vampire 4.3
AUFLIA 5 4 20 100 CVC4; veriT; z3-4.7.1n; Alt-Ergo; Vampire 4.3
CVC4; veriT; z3-4.7.1n; Alt-Ergo; Vampire 4.3
AUFLIRA 5 20011 100055 100 z3-4.7.1n; CVC4; Alt-Ergo; Vampire 4.3; veriT
z3-4.7.1n; CVC4; Vampire 4.3; Alt-Ergo; veriT
AUFNIRA 4 1480 5920 100 CVC4; Vampire 4.3; z3-4.7.1n; Alt-Ergo
CVC4; Vampire 4.3; z3-4.7.1n; Alt-Ergo
BV 4 5751 23004 100 CVC4; Boolector; z3-4.7.1n; Q3B
CVC4; Boolector; z3-4.7.1n; Q3B
BVFP 1 24 24 100 CVC4
CVC4
FP 1 61 61 100 CVC4
CVC4
LIA 4 388 1552 100 z3-4.7.1n; CVC4; Vampire 4.3; veriT
z3-4.7.1n; CVC4; Vampire 4.3; veriT
LRA 3 2419 7257 100 z3-4.7.1n; CVC4; Vampire 4.3
z3-4.7.1n; CVC4; Vampire 4.3
NIA 3 14 42 100 z3-4.7.1n; CVC4; Vampire 4.3
z3-4.7.1n; CVC4; Vampire 4.3
NRA 3 3813 11439 100 z3-4.7.1n; Vampire 4.3; CVC4
Vampire 4.3; z3-4.7.1n; CVC4
QF_ABV 5 15066 75330 100 Boolector; Yices 2.6.0; z3-4.7.1n; CVC4; MathSATn
Boolector; Yices 2.6.0; z3-4.7.1n; CVC4; MathSATn
QF_ABVFP 2 18129 36258 100 CVC4; COLIBRI
CVC4; COLIBRI
QF_ALIA 6 139 834 100 Yices 2.6.0; SMTInterpol; CVC4; z3-4.7.1n; veriT; MathSATn
Yices 2.6.0; SMTInterpol; CVC4; z3-4.7.1n; veriT; MathSATn
QF_ANIA 2 8 16 100 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
QF_AUFBV 5 31 155 100 CVC4; Yices 2.6.0; Boolector; z3-4.7.1n; MathSATn
CVC4; Yices 2.6.0; z3-4.7.1n; Boolector; MathSATn
QF_AUFLIA 6 1009 6054 100 Yices 2.6.0; z3-4.7.1n; SMTInterpol; CVC4; veriT; MathSATn
Yices 2.6.0; z3-4.7.1n; SMTInterpol; CVC4; veriT; MathSATn
QF_AUFNIA 2 17 34 100 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
QF_AX 5 551 2755 100 Yices 2.6.0; z3-4.7.1n; CVC4; SMTInterpol; MathSATn
Yices 2.6.0; z3-4.7.1n; CVC4; SMTInterpol; MathSATn
QF_BV 10 40102 401020 100 Boolector; Minkeyrink-ST; CVC4; STP-CMS-st-2018; Minkeyrink-MT; STP-Riss-st-2018; STP-CMS-mt-2018; z3-4.7.1n; Yices 2.6.0; MathSATn
Minkeyrink-MT; Boolector; Minkeyrink-ST; STP-CMS-mt-2018; CVC4; STP-CMS-st-2018; STP-Riss-st-2018; z3-4.7.1n; Yices 2.6.0; MathSATn
QF_BVFP 3 17215 51645 100 CVC4; z3-4.7.1n; COLIBRI
CVC4; z3-4.7.1n; COLIBRI
QF_DT 2 8000 16000 100 CVC4; z3-4.7.1n
CVC4; z3-4.7.1n
QF_FP 3 40300 120900 100 COLIBRI; CVC4; z3-4.7.1n
COLIBRI; CVC4; z3-4.7.1n
QF_IDL 8 2193 17544 100 Yices 2.6.0; z3-4.7.1n; CVC4; veriT; SMTInterpol; MathSATn; SMTRAT-Rat; CVC4-experimental-idl-2
Yices 2.6.0; z3-4.7.1n; CVC4; veriT; SMTInterpol; MathSATn; SMTRAT-Rat; CVC4-experimental-idl-2
QF_LIA 9 6947 62523 100 SPASS-SATT; Ctrl-Ergo; MathSATn; SMTInterpol; CVC4; Yices 2.6.0; z3-4.7.1n; SMTRAT-Rat; veriT
SPASS-SATT; Ctrl-Ergo; MathSATn; SMTInterpol; CVC4; Yices 2.6.0; z3-4.7.1n; SMTRAT-Rat; veriT
QF_LIRA 5 7 35 100 z3-4.7.1n; Yices 2.6.0; CVC4; SMTRAT-Rat; SMTInterpol
z3-4.7.1n; Yices 2.6.0; CVC4; SMTRAT-Rat; SMTInterpol
QF_LRA 11 1649 18139 100 CVC4; SPASS-SATT; Yices 2.6.0; veriT; SMTInterpol; MathSATn; z3-4.7.1n; opensmt2; Ctrl-Ergo; SMTRAT-Rat; SMTRAT-MCSAT
CVC4; SPASS-SATT; Yices 2.6.0; veriT; SMTInterpol; MathSATn; z3-4.7.1n; opensmt2; Ctrl-Ergo; SMTRAT-Rat; SMTRAT-MCSAT
QF_NIA 5 23876 119380 100 CVC4; Yices 2.6.0; z3-4.7.1n; AProVE; SMTRAT-Rat
CVC4; Yices 2.6.0; z3-4.7.1n; AProVE; SMTRAT-Rat
QF_NIRA 4 3 12 100 SMTRAT-Rat; z3-4.7.1n; CVC4; Yices 2.6.0
SMTRAT-Rat; z3-4.7.1n; CVC4; Yices 2.6.0
QF_NRA 6 11489 68934 100 z3-4.7.1n; Yices 2.6.0; veriT+raSAT+Reduce; SMTRAT-MCSAT; CVC4; SMTRAT-Rat
z3-4.7.1n; Yices 2.6.0; veriT+raSAT+Reduce; SMTRAT-MCSAT; CVC4; SMTRAT-Rat
QF_RDL 8 255 2040 100 Yices 2.6.0; CVC4; z3-4.7.1n; veriT; MathSATn; SMTInterpol; opensmt2; SMTRAT-Rat
Yices 2.6.0; CVC4; z3-4.7.1n; veriT; MathSATn; SMTInterpol; opensmt2; SMTRAT-Rat
QF_SLIA 1 72705 72705 100 CVC4
CVC4
QF_UF 7 7423 51961 100 Yices 2.6.0; veriT; CVC4; z3-4.7.1n; SMTInterpol; MathSATn; opensmt2
Yices 2.6.0; veriT; CVC4; z3-4.7.1n; SMTInterpol; MathSATn; opensmt2
QF_UFBV 5 1224 6120 100 Boolector; CVC4; Yices 2.6.0; MathSATn; z3-4.7.1n
Boolector; CVC4; Yices 2.6.0; MathSATn; z3-4.7.1n
QF_UFIDL 6 428 2568 100 Yices 2.6.0; z3-4.7.1n; SMTInterpol; MathSATn; veriT; CVC4
Yices 2.6.0; z3-4.7.1n; SMTInterpol; MathSATn; veriT; CVC4
QF_UFLIA 6 583 3498 100 Yices 2.6.0; z3-4.7.1n; CVC4; SMTInterpol; MathSATn; veriT
Yices 2.6.0; z3-4.7.1n; CVC4; SMTInterpol; MathSATn; veriT
QF_UFLRA 6 1284 7704 100 Yices 2.6.0; MathSATn; veriT; CVC4; SMTInterpol; z3-4.7.1n
Yices 2.6.0; MathSATn; veriT; CVC4; SMTInterpol; z3-4.7.1n
QF_UFNIA 3 7 21 100 Yices 2.6.0; CVC4; z3-4.7.1n
Yices 2.6.0; CVC4; z3-4.7.1n
QF_UFNRA 4 36 144 100 Yices 2.6.0; z3-4.7.1n; CVC4; veriT+raSAT+Reduce
Yices 2.6.0; z3-4.7.1n; CVC4; veriT+raSAT+Reduce
UF 4 7562 30248 100 CVC4; Vampire 4.3; veriT; z3-4.7.1n
Vampire 4.3; CVC4; veriT; z3-4.7.1n
UFBV 2 200 400 100 z3-4.7.1n; CVC4
z3-4.7.1n; CVC4
UFDT 2 4527 9054 100 CVC4; Vampire 4.3
CVC4; Vampire 4.3
UFDTLIA 2 303 606 100 CVC4; Vampire 4.3
CVC4; Vampire 4.3
UFIDL 4 68 272 100 z3-4.7.1n; CVC4; veriT; Vampire 4.3
z3-4.7.1n; CVC4; veriT; Vampire 4.3
UFLIA 4 10137 40548 100 CVC4; veriT; z3-4.7.1n; Vampire 4.3
CVC4; Vampire 4.3; veriT; z3-4.7.1n
UFLRA 4 15 60 100 z3-4.7.1n; CVC4; veriT; Vampire 4.3
z3-4.7.1n; CVC4; veriT; Vampire 4.3
UFNIA 3 3308 9924 100 z3-4.7.1n; Vampire 4.3; CVC4
Vampire 4.3; z3-4.7.1n; CVC4

n. Non-competing.