QF_AUFLIA (Single Query Track)

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

Page generated on 2021-07-18 17:29:06 +0000

Benchmarks: 558
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	Yices2	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	558	17.954	18.085	558	271	287	0	0	0
2019-Yices 2.6.2n	0	558	18.5	20.207	558	271	287	0	0	0
Yices2	0	558	22.025	25.324	558	271	287	0	0	0
MathSAT5n	0	558	132.023	132.354	558	271	287	0	0	0
cvc5	0	558	184.807	183.086	558	271	287	0	0	0
cvc5 - fixedn	0	558	188.607	184.542	558	271	287	0	0	0
SMTInterpol	0	558	883.299	397.044	558	271	287	0	0	0
veriT	0	39	21.784	20.978	39	0	39	519	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	558	17.954	18.085	558	271	287	0	0	0
2019-Yices 2.6.2n	0	558	18.5	20.207	558	271	287	0	0	0
Yices2	0	558	22.025	25.324	558	271	287	0	0	0
MathSAT5n	0	558	132.023	132.354	558	271	287	0	0	0
cvc5	0	558	184.807	183.086	558	271	287	0	0	0
cvc5 - fixedn	0	558	188.607	184.542	558	271	287	0	0	0
SMTInterpol	0	558	883.299	397.044	558	271	287	0	0	0
veriT	0	39	21.784	20.978	39	0	39	519	0	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
z3n	0	271	5.734	5.833	271	271	0	0	287	0	0
2019-Yices 2.6.2n	0	271	6.655	7.723	271	271	0	0	287	0	0
Yices2	0	271	7.642	9.589	271	271	0	0	287	0	0
MathSAT5n	0	271	44.386	44.409	271	271	0	0	287	0	0
cvc5	0	271	81.819	80.065	271	271	0	0	287	0	0
cvc5 - fixedn	0	271	80.479	80.387	271	271	0	0	287	0	0
SMTInterpol	0	271	244.888	125.262	271	271	0	0	287	0	0
veriT	0	0	10.417	10.494	0	0	0	271	287	0	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
z3n	0	287	12.22	12.252	287	0	287	0	271	0	0
2019-Yices 2.6.2n	0	287	11.845	12.484	287	0	287	0	271	0	0
Yices2	0	287	14.383	15.735	287	0	287	0	271	0	0
MathSAT5n	0	287	87.637	87.945	287	0	287	0	271	0	0
cvc5	0	287	102.988	103.021	287	0	287	0	271	0	0
cvc5 - fixedn	0	287	108.127	104.155	287	0	287	0	271	0	0
SMTInterpol	0	287	638.411	271.782	287	0	287	0	271	0	0
veriT	0	39	11.367	10.483	39	0	39	248	271	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	558	17.954	18.085	558	271	287	0	0	0
2019-Yices 2.6.2n	0	558	18.5	20.207	558	271	287	0	0	0
Yices2	0	558	22.025	25.324	558	271	287	0	0	0
MathSAT5n	0	558	132.023	132.354	558	271	287	0	0	0
SMTInterpol	0	558	883.299	397.044	558	271	287	0	0	0
cvc5	0	557	182.957	181.234	557	271	286	1	1	0
cvc5 - fixedn	0	557	186.187	182.121	557	271	286	1	1	0
veriT	0	39	21.784	20.978	39	0	39	519	0	0

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