Unknown Benchmarks Track (Summary)

Competition results as of Thu Jul 7 07:28:02 GMT

Logic	Solvers	Benchmarks	Order (parallel performance)
UFLIA	5	3736	vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; veriT-dev; z3n
NIA	5	5	z3n; vampire_smt_4.1_parallel; CVC4; ProB; vampire_smt_4.1
AUFNIRA	4	445	vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; z3n
AUFLIRA	5	165	vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; z3n; veriT-dev
QF_ABV	5	174	Yices2; CVC4; MathSat5n; Boolector; z3n
BV	4	106	Q3B; Boolector; z3n; CVC4
UFIDL	5	12	vampire_smt_4.1_parallel; vampire_smt_4.1; z3n; CVC4; veriT-dev
QF_UF	8	1	Yices2; veriT-dev; OpenSMT2; CVC4; SMTInterpol; z3n; MathSat5n; toysmt
UFNIA	4	1033	vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; z3n
UF	5	2909	vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; veriT-dev; z3n
QF_UFNRA	3	9	z3n; Yices2; CVC4
QF_NIRA	5	1	raSAT 0.3; z3n; raSAT 0.4; CVC4; Yices2
LIA	6	189	CVC4; z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev; ProB
QF_UFLRA	7	3	toysmt; veriT-dev; MathSat5n; Yices2; SMTInterpol; CVC4; z3n
QF_NIA	8	927	Yices2; z3n; SMT-RAT; CVC4; raSAT 0.4; ProB; raSAT 0.3; AProVE
QF_LIRA	4	1	z3n; Yices2; CVC4; SMTInterpol
QF_IDL	5	104	Yices2; z3n; SMTInterpol; veriT-dev; CVC4
QF_RDL	7	35	Yices2; CVC4; SMTInterpol; veriT-dev; toysmt; z3n; OpenSMT2
QF_FP	1	215	MathSat5n
QF_BV	16	17504	Yices2; Minkeyrink; ABC_glucose; Boolector (preprop); Boolector; stp-cms-mt; stp-cms-st; MathSat5n; CVC4; stp-cms-exp; MapleSTP-mt; stp-minisat-st; ABC_default; MapleSTP; z3n; Q3B
QF_NRA	6	1356	Yices2; z3n; SMT-RAT; raSAT 0.4; raSAT 0.3; CVC4
QF_LRA	9	56	Yices2; SMTInterpol; CVC4; veriT-dev; MathSat5n; toysmt; z3n; OpenSMT2; SMT-RAT
NRA	4	25	vampire_smt_4.1_parallel; vampire_smt_4.1; z3n; CVC4
QF_LIA	8	302	MathSat5n; SMT-RAT; CVC4; Yices2; z3n; SMTInterpol; veriT-dev; ProB
LRA	5	282	CVC4; z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev
UFBV	3	129	Boolector; z3n; CVC4

n. Non-competitive.