QF_UFLIA (Single Query Track)

Competition results for the QF_UFLIA logic in the Single Query Track.

Page generated on 2022-08-10 11:17:45 +0000

Benchmarks: 300
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices2	Yices2	Yices2	OpenSMT	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	300	75.286	76.232	300	238	62	0	0	0
z3-4.8.17n	0	300	145.938	142.473	300	238	62	0	0	0
OpenSMT	0	300	692.196	680.376	300	238	62	0	0	0
cvc5	0	300	797.754	796.852	300	238	62	0	0	0
smtinterpol	0	300	2381.769	1426.209	300	238	62	0	0	0
2021-SMTInterpoln	0	299	2772.425	1818.541	299	238	61	1	0	0
MathSATn	0	298	5036.611	5037.292	298	238	60	2	2	0
veriT	0	263	36267.656	36269.256	263	204	59	37	13	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	300	75.286	76.232	300	238	62	0	0	0
z3-4.8.17n	0	300	145.938	142.473	300	238	62	0	0	0
OpenSMT	0	300	692.196	680.376	300	238	62	0	0	0
cvc5	0	300	797.754	796.852	300	238	62	0	0	0
smtinterpol	0	300	2381.769	1426.209	300	238	62	0	0	0
2021-SMTInterpoln	0	299	2772.425	1818.541	299	238	61	1	0	0
MathSATn	0	298	5036.841	5037.252	298	238	60	2	2	0
veriT	0	263	36268.606	36269.006	263	204	59	37	13	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Yices2	0	238	6.33	7.03	238	238	0	0	62	0	0
z3-4.8.17n	0	238	34.849	34.465	238	238	0	0	62	0	0
cvc5	0	238	250.005	249.008	238	238	0	0	62	0	0
OpenSMT	0	238	642.962	633.297	238	238	0	0	62	0	0
smtinterpol	0	238	1402.881	740.257	238	238	0	0	62	0	0
2021-SMTInterpoln	0	238	2078.823	1342.497	238	238	0	0	62	0	0
MathSATn	0	238	2115.236	2115.595	238	238	0	0	62	2	0
veriT	0	204	31245.48	31245.683	204	204	0	34	62	13	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
OpenSMT	0	62	49.234	47.079	62	0	62	0	238	0	0
Yices2	0	62	68.956	69.201	62	0	62	0	238	0	0
z3-4.8.17n	0	62	111.09	108.008	62	0	62	0	238	0	0
cvc5	0	62	547.75	547.844	62	0	62	0	238	0	0
smtinterpol	0	62	978.888	685.952	62	0	62	0	238	0	0
2021-SMTInterpoln	0	61	693.602	476.043	61	0	61	1	238	0	0
MathSATn	0	60	2921.605	2921.657	60	0	60	2	238	2	0
veriT	0	59	5023.126	5023.323	59	0	59	3	238	13	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	299	65.616	66.556	299	238	61	1	1	0
z3-4.8.17n	0	299	91.356	87.88	299	238	61	1	1	0
OpenSMT	0	299	677.552	665.724	299	237	62	1	1	0
cvc5	0	293	444.789	443.783	293	237	56	7	7	0
2021-SMTInterpoln	0	292	1202.135	585.317	292	235	57	8	8	0
smtinterpol	0	289	1402.129	705.282	289	232	57	11	11	0
MathSATn	0	283	586.336	586.397	283	226	57	17	17	0
veriT	0	178	3758.183	3756.182	178	126	52	122	114	0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.