Home	•	Rules	•	Benchmarks	•	Tools	•	Specs	•	Participants	•	Results	•	SMT-LIB	•	Previous

Summary

Main Track

Competition results as of Thu Jul 7 07:24:34 GMT

Logic	Solvers	Benchmarks	# pairs Complete	% Complete	Order (sequential performance)
					Order (parallel performance)
ALIA	5	42	210	100	z3ⁿ; CVC4; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev
					z3ⁿ; CVC4; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev


AUFLIA	5	4	20	100	CVC4; vampire_smt_4.1; z3ⁿ; vampire_smt_4.1_parallel; veriT-dev
					CVC4; vampire_smt_4.1; vampire_smt_4.1_parallel; z3ⁿ; veriT-dev


AUFLIRA	5	19849	99245	100	z3ⁿ; vampire_smt_4.1; vampire_smt_4.1_parallel; CVC4; veriT-dev
					z3ⁿ; vampire_smt_4.1; vampire_smt_4.1_parallel; CVC4; veriT-dev


AUFNIRA	4	1050	4200	100	vampire_smt_4.1_parallel; vampire_smt_4.1; z3ⁿ; CVC4
					vampire_smt_4.1_parallel; vampire_smt_4.1; z3ⁿ; CVC4


BV	4	85	340	100	Q3B; z3ⁿ; CVC4; Boolector
					Q3B; z3ⁿ; CVC4; Boolector


LIA	6	201	1206	100	CVC4; z3ⁿ; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev; ProB
					CVC4; z3ⁿ; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev; ProB


LRA	5	339	1695	100	CVC4; z3ⁿ; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev
					CVC4; z3ⁿ; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev


NIA	5	9	45	100	z3ⁿ; ProB; vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4
					z3ⁿ; ProB; vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4


NRA	4	3788	15152	100	vampire_smt_4.1_parallel; vampire_smt_4.1; z3ⁿ; CVC4
					vampire_smt_4.1_parallel; vampire_smt_4.1; z3ⁿ; CVC4


QF_ABV	5	14720	73600	100	Boolector; Yices2; MathSat5ⁿ; CVC4; z3ⁿ
					Boolector; Yices2; MathSat5ⁿ; CVC4; z3ⁿ


QF_ALIA	6	139	834	100	Yices2; MathSat5ⁿ; SMTInterpol; CVC4; z3ⁿ; veriT-dev
					Yices2; MathSat5ⁿ; SMTInterpol; CVC4; z3ⁿ; veriT-dev


QF_ANIA	2	8	16	100	CVC4; z3ⁿ
					CVC4; z3ⁿ


QF_AUFBV	5	37	185	100	MathSat5ⁿ; CVC4; Yices2; Boolector; z3ⁿ
					MathSat5ⁿ; CVC4; Yices2; Boolector; z3ⁿ


QF_AUFLIA	6	1009	6054	100	Yices2; z3ⁿ; SMTInterpol; MathSat5ⁿ; CVC4; veriT-dev
					Yices2; z3ⁿ; SMTInterpol; MathSat5ⁿ; CVC4; veriT-dev


QF_AUFNIA	2	21	42	100	CVC4; z3ⁿ
					CVC4; z3ⁿ


QF_AX	5	551	2755	100	Yices2; MathSat5ⁿ; z3ⁿ; CVC4; SMTInterpol
					Yices2; MathSat5ⁿ; z3ⁿ; CVC4; SMTInterpol


QF_BV	16	26414	422624	100	Boolector (preprop); Boolector; stp-cms-st; z3ⁿ; stp-cms-exp; CVC4; Minkeyrink; stp-cms-mt; ABC_glucose; Yices2; MathSat5ⁿ; MapleSTP; MapleSTP-mt; stp-minisat-st; ABC_default; Q3B
					Boolector (preprop); Boolector; Minkeyrink; stp-cms-mt; stp-cms-st; CVC4; z3ⁿ; stp-cms-exp; ABC_glucose; Yices2; MathSat5ⁿ; MapleSTP-mt; MapleSTP; stp-minisat-st; ABC_default; Q3B


QF_BVFP	2	7	14	100	z3ⁿ; MathSat5ⁿ
					z3ⁿ; MathSat5ⁿ


QF_FP	1	34413	34413	100	MathSat5ⁿ
					MathSat5ⁿ


QF_IDL	5	2094	10470	100	z3ⁿ; Yices2; CVC4; veriT-dev; SMTInterpol
					z3ⁿ; Yices2; CVC4; veriT-dev; SMTInterpol


QF_LIA	8	5839	46712	100	MathSat5ⁿ; CVC4; Yices2; SMTInterpol; z3ⁿ; SMT-RAT; veriT-dev; ProB
					MathSat5ⁿ; CVC4; Yices2; SMTInterpol; z3ⁿ; SMT-RAT; veriT-dev; ProB


QF_LIRA	4	6	24	100	Yices2; CVC4; z3ⁿ; SMTInterpol
					Yices2; CVC4; z3ⁿ; SMTInterpol


QF_LRA	9	1626	14634	100	CVC4; Yices2; veriT-dev; MathSat5ⁿ; SMTInterpol; z3ⁿ; OpenSMT2; SMT-RAT; toysmt
					CVC4; Yices2; veriT-dev; MathSat5ⁿ; SMTInterpol; z3ⁿ; OpenSMT2; SMT-RAT; toysmt


QF_NIA	8	8593	68744	100	z3ⁿ; Yices2; CVC4; SMT-RAT; AProVE; raSAT 0.4; raSAT 0.3; ProB
					z3ⁿ; Yices2; CVC4; SMT-RAT; AProVE; raSAT 0.4; ProB; raSAT 0.3


QF_NIRA	5	2	10	100	CVC4; z3ⁿ; Yices2; raSAT 0.3; raSAT 0.4
					CVC4; z3ⁿ; Yices2; raSAT 0.3; raSAT 0.4


QF_NRA	6	10245	61470	100	z3ⁿ; Yices2; raSAT 0.4; raSAT 0.3; CVC4; SMT-RAT
					z3ⁿ; Yices2; raSAT 0.4; CVC4; SMT-RAT; raSAT 0.3


QF_RDL	7	220	1540	100	Yices2; veriT-dev; z3ⁿ; CVC4; SMTInterpol; OpenSMT2; toysmt
					Yices2; veriT-dev; z3ⁿ; CVC4; SMTInterpol; OpenSMT2; toysmt


QF_UF	8	6649	53192	100	Yices2; veriT-dev; CVC4; OpenSMT2; z3ⁿ; MathSat5ⁿ; SMTInterpol; toysmt
					Yices2; veriT-dev; CVC4; OpenSMT2; z3ⁿ; MathSat5ⁿ; SMTInterpol; toysmt


QF_UFBV	5	31	155	100	Boolector; Yices2; CVC4; z3ⁿ; MathSat5ⁿ
					Boolector; Yices2; CVC4; z3ⁿ; MathSat5ⁿ


QF_UFIDL	5	441	2205	100	Yices2; z3ⁿ; SMTInterpol; veriT-dev; CVC4
					Yices2; z3ⁿ; SMTInterpol; veriT-dev; CVC4


QF_UFLIA	6	598	3588	100	z3ⁿ; Yices2; CVC4; MathSat5ⁿ; SMTInterpol; veriT-dev
					z3ⁿ; Yices2; CVC4; MathSat5ⁿ; SMTInterpol; veriT-dev


QF_UFLRA	7	1627	11389	100	Yices2; z3ⁿ; veriT-dev; MathSat5ⁿ; CVC4; SMTInterpol; toysmt
					Yices2; z3ⁿ; veriT-dev; MathSat5ⁿ; CVC4; SMTInterpol; toysmt


QF_UFNIA	3	7	21	100	Yices2; CVC4; z3ⁿ
					CVC4; Yices2; z3ⁿ


QF_UFNRA	3	34	102	100	Yices2; z3ⁿ; CVC4
					Yices2; z3ⁿ; CVC4


UF	5	2839	14195	100	CVC4; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev; z3ⁿ
					CVC4; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev; z3ⁿ


UFBV	3	71	213	100	z3ⁿ; CVC4; Boolector
					z3ⁿ; CVC4; Boolector


UFIDL	5	68	340	100	CVC4; z3ⁿ; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev
					CVC4; z3ⁿ; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev


UFLIA	5	8404	42020	100	CVC4; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev; z3ⁿ
					CVC4; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev; z3ⁿ


UFLRA	5	25	125	100	z3ⁿ; vampire_smt_4.1; veriT-dev; vampire_smt_4.1_parallel; CVC4
					z3ⁿ; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev; CVC4


UFNIA	4	2319	9276	100	vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; z3ⁿ
					vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; z3ⁿ

n. Non-competitive.

Home	•	Rules	•	Benchmarks	•	Tools	•	Specs	•	Participants	•	Results	•	SMT-LIB	•	Previous

Last modified: Thu 07 Jul 2016 07:28 UTC