Home Rules Benchmarks Tools Specs Participants Results SMT-LIB Previous

Summary

Main Track

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

non competitive divisions

Logic Solvers Benchmarks # pairs Complete % Complete Order (sequential performance)
Order (parallel performance)
Order (sequential performance on industrial benchmarks)
Order (parallel performance on industrial benchmarks)
ALIA542210100[Z3]; CVC4 (exp); CVC4; veriT; CVC3
[Z3]; CVC4 (exp); CVC4; veriT; CVC3
[Z3]; CVC4 (exp); CVC4; veriT; CVC3
[Z3]; CVC4 (exp); CVC4; veriT; CVC3
AUFLIA5420100CVC4 (exp); CVC3; CVC4; [Z3]; veriT
CVC4 (exp); CVC3; CVC4; [Z3]; veriT
CVC4; CVC4 (exp); [Z3]; CVC3; veriT
CVC4; [Z3]; CVC4 (exp); CVC3; veriT
AUFLIRA51984999245100[Z3]; CVC4 (exp); CVC4; CVC3; veriT
[Z3]; CVC4 (exp); CVC4; CVC3; veriT
[Z3]; CVC4; CVC4 (exp); CVC3; veriT
[Z3]; CVC4; CVC4 (exp); CVC3; veriT
AUFNIRA410504200100CVC4; CVC4 (exp); [Z3]; CVC3
CVC4; CVC4 (exp); [Z3]; CVC3
CVC4; CVC4 (exp); [Z3]; CVC3
CVC4; CVC4 (exp); [Z3]; CVC3
BV485340100[Z3]; CVC4; CVC4 (exp); CVC3
[Z3]; CVC4 (exp); CVC4; CVC3
[Z3]; CVC4; CVC4 (exp); CVC3
[Z3]; CVC4 (exp); CVC4; CVC3
LIA52011005100CVC4 (exp); [Z3]; CVC4; CVC3; veriT
CVC4 (exp); [Z3]; CVC4; CVC3; veriT
CVC4 (exp); [Z3]; CVC4; CVC3; veriT
CVC4 (exp); [Z3]; CVC4; CVC3; veriT
LRA53391695100CVC4 (exp); CVC4; [Z3]; CVC3; veriT
CVC4 (exp); CVC4; [Z3]; CVC3; veriT
CVC4; CVC4 (exp); [Z3]; CVC3; veriT
CVC4 (exp); CVC4; [Z3]; CVC3; veriT
NIA4936100[Z3]; CVC4; CVC4 (exp); CVC3
[Z3]; CVC4; CVC4 (exp); CVC3
[Z3]; CVC4; CVC4 (exp); CVC3
[Z3]; CVC4; CVC4 (exp); CVC3
NRA4378815152100CVC4 (exp); CVC4; CVC3; [Z3]
CVC4 (exp); CVC4; CVC3; [Z3]
CVC4 (exp); CVC4; CVC3; [Z3]
CVC4 (exp); CVC4; CVC3; [Z3]
QF_ABV61472088320100Boolector (QF_AUFBV); Yices; [MathSat]; CVC4 (exp); CVC4; [Z3]
Boolector (QF_AUFBV); Yices; [MathSat]; CVC4 (exp); CVC4; [Z3]
Boolector (QF_AUFBV); Yices; [MathSat]; CVC4 (exp); CVC4; [Z3]
Boolector (QF_AUFBV); Yices; [MathSat]; CVC4 (exp); CVC4; [Z3]
QF_ALIA7134938100Yices; [MathSat]; SMTInterpol; CVC4 (exp); [Z3]; CVC4; veriT
Yices; [MathSat]; SMTInterpol; CVC4 (exp); [Z3]; CVC4; veriT
Yices; [MathSat]; SMTInterpol; CVC4 (exp); [Z3]; CVC4; veriT
Yices; [MathSat]; SMTInterpol; CVC4 (exp); [Z3]; CVC4; veriT
QF_ANIA3618100[Z3]; CVC4 (exp); CVC4
[Z3]; CVC4 (exp); CVC4
[Z3]; CVC4 (exp); CVC4
[Z3]; CVC4 (exp); CVC4
QF_AUFBV637222100[MathSat]; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); [Z3]
[MathSat]; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); [Z3]
[MathSat]; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); [Z3]
[MathSat]; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); [Z3]
QF_AUFLIA710097063100Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; [Z3]; [MathSat]; CVC4 (exp); SMTInterpol; CVC4; veriT
[Z3]; Yices; SMTInterpol; CVC4 (exp); [MathSat]; CVC4; veriT
[Z3]; Yices; SMTInterpol; CVC4 (exp); [MathSat]; CVC4; veriT
QF_AUFNIA32163100CVC4; CVC4 (exp); [Z3]
CVC4; CVC4 (exp); [Z3]
CVC4; CVC4 (exp); [Z3]
CVC4; CVC4 (exp); [Z3]
QF_AX75513857100Yices; [MathSat]; [Z3]; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; [MathSat]; [Z3]; CVC4 (exp); CVC4; SMTInterpol; veriT
-
-
QF_BV1126414290554100Boolector (QF_BV); CVC4 (exp); STP-CMSat4; [Z3]; CVC4; [MathSat]; Yices; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15)
Boolector (QF_BV); CVC4 (exp); STP-CMSat4; [Z3]; CVC4; [MathSat]; Yices; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15)
Boolector (QF_BV); [Z3]; STP-CMSat4; Yices; CVC4 (exp); [MathSat]; CVC4; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15)
Boolector (QF_BV); [Z3]; CVC4 (exp); STP-CMSat4; Yices; [MathSat]; CVC4; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15)
QF_BVFP3721100Z3 (FP); [MathSat]; Z3 (ijcar14)
Z3 (FP); [MathSat]; Z3 (ijcar14)
-
-
QF_FP334413103239100Z3 (FP); Z3 (ijcar14); [MathSat]
Z3 (FP); Z3 (ijcar14); [MathSat]
-
-
QF_IDL6209412564100[Z3]; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT
[Z3]; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT
[Z3]; Yices; CVC4 (exp); CVC4; veriT; SMTInterpol
[Z3]; Yices; CVC4 (exp); CVC4; veriT; SMTInterpol
QF_LIA8583946712100[MathSat]; CVC4 (exp); CVC4; Yices; [Z3]; SMTInterpol; SMT-RAT; veriT
[MathSat]; CVC4 (exp); CVC4; Yices; [Z3]; SMTInterpol; SMT-RAT; veriT
[Z3]; [MathSat]; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT; SMT-RAT
[Z3]; [MathSat]; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT; SMT-RAT
QF_LIRA6636100Yices; CVC4; CVC4 (exp); [Z3]; SMT-RAT; SMTInterpol
Yices; CVC4; CVC4 (exp); [Z3]; SMT-RAT; SMTInterpol
Yices; CVC4; CVC4 (exp); [Z3]; SMT-RAT; SMTInterpol
Yices; CVC4; CVC4 (exp); [Z3]; SMT-RAT; SMTInterpol
QF_LRA8162613008100CVC4; CVC4 (exp); Yices; [MathSat]; veriT; [Z3]; SMTInterpol; SMT-RAT
CVC4; CVC4 (exp); Yices; [MathSat]; veriT; [Z3]; SMTInterpol; SMT-RAT
CVC4; CVC4 (exp); Yices; [MathSat]; veriT; [Z3]; SMTInterpol; SMT-RAT
CVC4; CVC4 (exp); Yices; [MathSat]; veriT; [Z3]; SMTInterpol; SMT-RAT
QF_NIA8847567800100[Z3]; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp)
[Z3]; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp)
[Z3]; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp)
[Z3]; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp)
QF_NIRA428100CVC4 (exp); CVC4; SMT-RAT; [Z3]
CVC4 (exp); CVC4; SMT-RAT; [Z3]
CVC4 (exp); CVC4; SMT-RAT; [Z3]
CVC4 (exp); CVC4; SMT-RAT; [Z3]
QF_NRA71018471288100[Z3]; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4 (exp); CVC4
[Z3]; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4; CVC4 (exp)
[Z3]; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4 (exp); CVC4
[Z3]; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4; CVC4 (exp)
QF_RDL62201320100Yices; [Z3]; veriT; CVC4 (exp); CVC4; SMTInterpol
Yices; [Z3]; veriT; CVC4 (exp); CVC4; SMTInterpol
Yices; [Z3]; CVC4; CVC4 (exp); veriT; SMTInterpol
Yices; [Z3]; CVC4; CVC4 (exp); veriT; SMTInterpol
QF_UF10664966490100Yices; veriT; CVC4; CVC4 (exp); OpenSMT2; [Z3]; [MathSat]; SMTInterpol; SMT-RAT; OpenSMT2 (parallel)
Yices; veriT; CVC4; CVC4 (exp); OpenSMT2; [Z3]; [MathSat]; SMTInterpol; SMT-RAT; OpenSMT2 (parallel)
Yices; veriT; SMT-RAT; CVC4 (exp); CVC4; OpenSMT2 (parallel); OpenSMT2; [MathSat]; [Z3]; SMTInterpol
Yices; CVC4; SMT-RAT; veriT; CVC4 (exp); OpenSMT2 (parallel); OpenSMT2; [MathSat]; [Z3]; SMTInterpol
QF_UFBV631186100Boolector (QF_AUFBV); Yices; CVC4 (exp); [Z3]; [MathSat]; CVC4
Boolector (QF_AUFBV); Yices; CVC4 (exp); [Z3]; [MathSat]; CVC4
Boolector (QF_AUFBV); Yices; CVC4 (exp); [Z3]; [MathSat]; CVC4
Boolector (QF_AUFBV); Yices; CVC4 (exp); [Z3]; [MathSat]; CVC4
QF_UFIDL64412646100Yices; [Z3]; SMTInterpol; veriT; CVC4 (exp); CVC4
Yices; [Z3]; SMTInterpol; veriT; CVC4 (exp); CVC4
Yices; [Z3]; SMTInterpol; CVC4 (exp); CVC4; veriT
Yices; [Z3]; SMTInterpol; CVC4 (exp); CVC4; veriT
QF_UFLIA75984186100[Z3]; Yices; CVC4; CVC4 (exp); [MathSat]; SMTInterpol; veriT
[Z3]; Yices; CVC4; CVC4 (exp); [MathSat]; SMTInterpol; veriT
[Z3]; Yices; CVC4; CVC4 (exp); [MathSat]; SMTInterpol; veriT
[Z3]; Yices; CVC4; CVC4 (exp); SMTInterpol; [MathSat]; veriT
QF_UFLRA7162711389100Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT
Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT
QF_UFNIA4728100CVC4 (exp); CVC4; [Z3]; CVC3
CVC4 (exp); CVC4; [Z3]; CVC3
CVC4 (exp); CVC4; [Z3]; CVC3
CVC4 (exp); CVC4; [Z3]; CVC3
QF_UFNRA434136100[Z3]; CVC3; CVC4 (exp); CVC4
[Z3]; CVC3; CVC4 (exp); CVC4
[Z3]; CVC3; CVC4 (exp); CVC4
[Z3]; CVC3; CVC4 (exp); CVC4
UF5283914195100CVC4 (exp); CVC4; [Z3]; CVC3; veriT
CVC4 (exp); CVC4; [Z3]; CVC3; veriT
CVC4 (exp); CVC4; [Z3]; CVC3; veriT
CVC4 (exp); CVC4; [Z3]; CVC3; veriT
UFBV471284100[Z3]; CVC4; CVC4 (exp); CVC3
[Z3]; CVC4; CVC4 (exp); CVC3
[Z3]; CVC4; CVC4 (exp); CVC3
[Z3]; CVC4; CVC4 (exp); CVC3
UFIDL568340100[Z3]; CVC4; CVC4 (exp); veriT; CVC3
[Z3]; CVC4; CVC4 (exp); veriT; CVC3
[Z3]; CVC4; CVC4 (exp); veriT; CVC3
[Z3]; CVC4; CVC4 (exp); veriT; CVC3
UFLIA5840442020100CVC4; CVC4 (exp); [Z3]; veriT; CVC3
CVC4; CVC4 (exp); [Z3]; veriT; CVC3
CVC4; CVC4 (exp); [Z3]; veriT; CVC3
CVC4; CVC4 (exp); [Z3]; veriT; CVC3
UFLRA525125100CVC3; veriT; CVC4; CVC4 (exp); [Z3]
CVC3; veriT; CVC4; CVC4 (exp); [Z3]
veriT; CVC3; CVC4 (exp); CVC4; [Z3]
veriT; CVC3; CVC4; CVC4 (exp); [Z3]
UFNIA423199276100CVC4; CVC4 (exp); [Z3]; CVC3
CVC4; CVC4 (exp); [Z3]; CVC3
CVC4; CVC4 (exp); [Z3]; CVC3
CVC4; CVC4 (exp); [Z3]; CVC3
Home Rules Benchmarks Tools Specs Participants Results SMT-LIB Previous

Last modified: Fri 30 Oct 2015 12:49 UTC
Valid XHTML 1.0 Valid CSS!