SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2015

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Main Track (Summary)

Competition results as of Fri Oct 30 12:49:29 GMT

Logic Solvers Benchmarks # pairs Complete % Complete Order (sequential performance)
Order (parallel performance)
Order (sequential performance on industrial benchmarks)
Order (parallel performance on industrial benchmarks)
ALIA 5 42 210 100 Z3n; CVC4 (exp); CVC4; veriT; CVC3
Z3n; CVC4 (exp); CVC4; veriT; CVC3
Z3n; CVC4 (exp); CVC4; veriT; CVC3
Z3n; CVC4 (exp); CVC4; veriT; CVC3
AUFLIA 5 4 20 100 CVC4 (exp); CVC3; CVC4; Z3n; veriT
CVC4 (exp); CVC3; CVC4; Z3n; veriT
CVC4; CVC4 (exp); Z3n; CVC3; veriT
CVC4; Z3n; CVC4 (exp); CVC3; veriT
AUFLIRA 5 19849 99245 100 Z3n; CVC4 (exp); CVC4; CVC3; veriT
Z3n; CVC4 (exp); CVC4; CVC3; veriT
Z3n; CVC4; CVC4 (exp); CVC3; veriT
Z3n; CVC4; CVC4 (exp); CVC3; veriT
AUFNIRA 4 1050 4200 100 CVC4; CVC4 (exp); Z3n; CVC3
CVC4; CVC4 (exp); Z3n; CVC3
CVC4; CVC4 (exp); Z3n; CVC3
CVC4; CVC4 (exp); Z3n; CVC3
BV 4 85 340 100 Z3n; CVC4; CVC4 (exp); CVC3
Z3n; CVC4 (exp); CVC4; CVC3
Z3n; CVC4; CVC4 (exp); CVC3
Z3n; CVC4 (exp); CVC4; CVC3
LIA 5 201 1005 100 CVC4 (exp); Z3n; CVC4; CVC3; veriT
CVC4 (exp); Z3n; CVC4; CVC3; veriT
CVC4 (exp); Z3n; CVC4; CVC3; veriT
CVC4 (exp); Z3n; CVC4; CVC3; veriT
LRA 5 339 1695 100 CVC4 (exp); CVC4; Z3n; CVC3; veriT
CVC4 (exp); CVC4; Z3n; CVC3; veriT
CVC4; CVC4 (exp); Z3n; CVC3; veriT
CVC4 (exp); CVC4; Z3n; CVC3; veriT
NIA 4 9 36 100 Z3n; CVC4; CVC4 (exp); CVC3
Z3n; CVC4; CVC4 (exp); CVC3
Z3n; CVC4; CVC4 (exp); CVC3
Z3n; CVC4; CVC4 (exp); CVC3
NRA 4 3788 15152 100 CVC4 (exp); CVC4; CVC3; Z3n
CVC4 (exp); CVC4; CVC3; Z3n
CVC4 (exp); CVC4; CVC3; Z3n
CVC4 (exp); CVC4; CVC3; Z3n
QF_ABV 6 14720 88320 100 Boolector (QF_AUFBV); Yices; MathSatn; CVC4 (exp); CVC4; Z3n
Boolector (QF_AUFBV); Yices; MathSatn; CVC4 (exp); CVC4; Z3n
Boolector (QF_AUFBV); Yices; MathSatn; CVC4 (exp); CVC4; Z3n
Boolector (QF_AUFBV); Yices; MathSatn; CVC4 (exp); CVC4; Z3n
QF_ALIA 7 134 938 100 Yices; MathSatn; SMTInterpol; CVC4 (exp); Z3n; CVC4; veriT
Yices; MathSatn; SMTInterpol; CVC4 (exp); Z3n; CVC4; veriT
Yices; MathSatn; SMTInterpol; CVC4 (exp); Z3n; CVC4; veriT
Yices; MathSatn; SMTInterpol; CVC4 (exp); Z3n; CVC4; veriT
QF_ANIA 3 6 18 100 Z3n; CVC4 (exp); CVC4
Z3n; CVC4 (exp); CVC4
Z3n; CVC4 (exp); CVC4
Z3n; CVC4 (exp); CVC4
QF_AUFBV 6 37 222 100 MathSatn; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); Z3n
MathSatn; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); Z3n
MathSatn; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); Z3n
MathSatn; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); Z3n
QF_AUFLIA 7 1009 7063 100 Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; Z3n; MathSatn; CVC4 (exp); SMTInterpol; CVC4; veriT
Z3n; Yices; SMTInterpol; CVC4 (exp); MathSatn; CVC4; veriT
Z3n; Yices; SMTInterpol; CVC4 (exp); MathSatn; CVC4; veriT
QF_AUFNIA 3 21 63 100 CVC4; CVC4 (exp); Z3n
CVC4; CVC4 (exp); Z3n
CVC4; CVC4 (exp); Z3n
CVC4; CVC4 (exp); Z3n
QF_AX 7 551 3857 100 Yices; MathSatn; Z3n; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; MathSatn; Z3n; CVC4 (exp); CVC4; SMTInterpol; veriT
-
-
QF_BV 11 26414 290554 100 Boolector (QF_BV); CVC4 (exp); STP-CMSat4; Z3n; CVC4; MathSatn; Yices; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15)
Boolector (QF_BV); CVC4 (exp); STP-CMSat4; Z3n; CVC4; MathSatn; Yices; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15)
Boolector (QF_BV); Z3n; STP-CMSat4; Yices; CVC4 (exp); MathSatn; CVC4; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15)
Boolector (QF_BV); Z3n; CVC4 (exp); STP-CMSat4; Yices; MathSatn; CVC4; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15)
QF_BVFP 3 7 21 100 Z3 (FP); MathSatn; Z3 (ijcar14)
Z3 (FP); MathSatn; Z3 (ijcar14)
-
-
QF_FP 3 34413 103239 100 Z3 (FP); Z3 (ijcar14); MathSatn
Z3 (FP); Z3 (ijcar14); MathSatn
-
-
QF_IDL 6 2094 12564 100 Z3n; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT
Z3n; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT
Z3n; Yices; CVC4 (exp); CVC4; veriT; SMTInterpol
Z3n; Yices; CVC4 (exp); CVC4; veriT; SMTInterpol
QF_LIA 8 5839 46712 100 MathSatn; CVC4 (exp); CVC4; Yices; Z3n; SMTInterpol; SMT-RAT; veriT
MathSatn; CVC4 (exp); CVC4; Yices; Z3n; SMTInterpol; SMT-RAT; veriT
Z3n; MathSatn; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT; SMT-RAT
Z3n; MathSatn; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT; SMT-RAT
QF_LIRA 6 6 36 100 Yices; CVC4; CVC4 (exp); Z3n; SMT-RAT; SMTInterpol
Yices; CVC4; CVC4 (exp); Z3n; SMT-RAT; SMTInterpol
Yices; CVC4; CVC4 (exp); Z3n; SMT-RAT; SMTInterpol
Yices; CVC4; CVC4 (exp); Z3n; SMT-RAT; SMTInterpol
QF_LRA 8 1626 13008 100 CVC4; CVC4 (exp); Yices; MathSatn; veriT; Z3n; SMTInterpol; SMT-RAT
CVC4; CVC4 (exp); Yices; MathSatn; veriT; Z3n; SMTInterpol; SMT-RAT
CVC4; CVC4 (exp); Yices; MathSatn; veriT; Z3n; SMTInterpol; SMT-RAT
CVC4; CVC4 (exp); Yices; MathSatn; veriT; Z3n; SMTInterpol; SMT-RAT
QF_NIA 8 8475 67800 100 Z3n; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp)
Z3n; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp)
Z3n; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp)
Z3n; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp)
QF_NIRA 4 2 8 100 CVC4 (exp); CVC4; SMT-RAT; Z3n
CVC4 (exp); CVC4; SMT-RAT; Z3n
CVC4 (exp); CVC4; SMT-RAT; Z3n
CVC4 (exp); CVC4; SMT-RAT; Z3n
QF_NRA 7 10184 71288 100 Z3n; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4 (exp); CVC4
Z3n; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4; CVC4 (exp)
Z3n; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4 (exp); CVC4
Z3n; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4; CVC4 (exp)
QF_RDL 6 220 1320 100 Yices; Z3n; veriT; CVC4 (exp); CVC4; SMTInterpol
Yices; Z3n; veriT; CVC4 (exp); CVC4; SMTInterpol
Yices; Z3n; CVC4; CVC4 (exp); veriT; SMTInterpol
Yices; Z3n; CVC4; CVC4 (exp); veriT; SMTInterpol
QF_UF 10 6649 66490 100 Yices; veriT; CVC4; CVC4 (exp); OpenSMT2; Z3n; MathSatn; SMTInterpol; SMT-RAT; OpenSMT2 (parallel)
Yices; veriT; CVC4; CVC4 (exp); OpenSMT2; Z3n; MathSatn; SMTInterpol; SMT-RAT; OpenSMT2 (parallel)
Yices; veriT; SMT-RAT; CVC4 (exp); CVC4; OpenSMT2 (parallel); OpenSMT2; MathSatn; Z3n; SMTInterpol
Yices; CVC4; SMT-RAT; veriT; CVC4 (exp); OpenSMT2 (parallel); OpenSMT2; MathSatn; Z3n; SMTInterpol
QF_UFBV 6 31 186 100 Boolector (QF_AUFBV); Yices; CVC4 (exp); Z3n; MathSatn; CVC4
Boolector (QF_AUFBV); Yices; CVC4 (exp); Z3n; MathSatn; CVC4
Boolector (QF_AUFBV); Yices; CVC4 (exp); Z3n; MathSatn; CVC4
Boolector (QF_AUFBV); Yices; CVC4 (exp); Z3n; MathSatn; CVC4
QF_UFIDL 6 441 2646 100 Yices; Z3n; SMTInterpol; veriT; CVC4 (exp); CVC4
Yices; Z3n; SMTInterpol; veriT; CVC4 (exp); CVC4
Yices; Z3n; SMTInterpol; CVC4 (exp); CVC4; veriT
Yices; Z3n; SMTInterpol; CVC4 (exp); CVC4; veriT
QF_UFLIA 7 598 4186 100 Z3n; Yices; CVC4; CVC4 (exp); MathSatn; SMTInterpol; veriT
Z3n; Yices; CVC4; CVC4 (exp); MathSatn; SMTInterpol; veriT
Z3n; Yices; CVC4; CVC4 (exp); MathSatn; SMTInterpol; veriT
Z3n; Yices; CVC4; CVC4 (exp); SMTInterpol; MathSatn; veriT
QF_UFLRA 7 1627 11389 100 Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT
QF_UFNIA 4 7 28 100 CVC4 (exp); CVC4; Z3n; CVC3
CVC4 (exp); CVC4; Z3n; CVC3
CVC4 (exp); CVC4; Z3n; CVC3
CVC4 (exp); CVC4; Z3n; CVC3
QF_UFNRA 4 34 136 100 Z3n; CVC3; CVC4 (exp); CVC4
Z3n; CVC3; CVC4 (exp); CVC4
Z3n; CVC3; CVC4 (exp); CVC4
Z3n; CVC3; CVC4 (exp); CVC4
UF 5 2839 14195 100 CVC4 (exp); CVC4; Z3n; CVC3; veriT
CVC4 (exp); CVC4; Z3n; CVC3; veriT
CVC4 (exp); CVC4; Z3n; CVC3; veriT
CVC4 (exp); CVC4; Z3n; CVC3; veriT
UFBV 4 71 284 100 Z3n; CVC4; CVC4 (exp); CVC3
Z3n; CVC4; CVC4 (exp); CVC3
Z3n; CVC4; CVC4 (exp); CVC3
Z3n; CVC4; CVC4 (exp); CVC3
UFIDL 5 68 340 100 Z3n; CVC4; CVC4 (exp); veriT; CVC3
Z3n; CVC4; CVC4 (exp); veriT; CVC3
Z3n; CVC4; CVC4 (exp); veriT; CVC3
Z3n; CVC4; CVC4 (exp); veriT; CVC3
UFLIA 5 8404 42020 100 CVC4; CVC4 (exp); Z3n; veriT; CVC3
CVC4; CVC4 (exp); Z3n; veriT; CVC3
CVC4; CVC4 (exp); Z3n; veriT; CVC3
CVC4; CVC4 (exp); Z3n; veriT; CVC3
UFLRA 5 25 125 100 CVC3; veriT; CVC4; CVC4 (exp); Z3n
CVC3; veriT; CVC4; CVC4 (exp); Z3n
veriT; CVC3; CVC4 (exp); CVC4; Z3n
veriT; CVC3; CVC4; CVC4 (exp); Z3n
UFNIA 4 2319 9276 100 CVC4; CVC4 (exp); Z3n; CVC3
CVC4; CVC4 (exp); Z3n; CVC3
CVC4; CVC4 (exp); Z3n; CVC3
CVC4; CVC4 (exp); Z3n; CVC3

n. Non-competitive.