SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2024

QF_AX (Single Query Track)

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

Results were generated on 2024-07-08

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Yices2	Yices2	Yices2	Yices2	Yices2

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	300	40.503397	70.597156	300	155	145	0	0	0	0
Z3-alpha	0	300	62.684488	92.846602	300	155	145	0	0	0	0
cvc5	0	300	114.899111	144.913468	300	155	145	0	0	0	0
OpenSMT	0	300	200.59477	230.830423	300	155	145	0	0	0	0
SMTInterpol	0	297	636.577052	288.487764	297	152	145	3	0	0	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	300	40.503397	70.597156	300	155	145	0	0	0	0
Z3-alpha	0	300	62.684488	92.846602	300	155	145	0	0	0	0
cvc5	0	300	114.899111	144.913468	300	155	145	0	0	0	0
OpenSMT	0	300	200.59477	230.830423	300	155	145	0	0	0	0
SMTInterpol	0	297	636.577052	288.487764	297	152	145	3	0	0	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	155	19.774435	35.321471	155	155	0	0	145	0	0
cvc5	0	155	25.464626	40.955677	155	155	0	0	145	0	0
Z3-alpha	0	155	29.127013	44.702966	155	155	0	0	145	0	0
OpenSMT	0	155	30.76109	46.342954	155	155	0	0	145	0	0
SMTInterpol	0	152	151.333097	89.408803	152	152	0	3	145	0	0

UNSAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	145	20.728961	35.275685	145	0	145	0	155	0	0
Z3-alpha	0	145	33.557475	48.143637	145	0	145	0	155	0	0
cvc5	0	145	89.434485	103.957792	145	0	145	0	155	0	0
OpenSMT	0	145	169.83368	184.487469	145	0	145	0	155	0	0
SMTInterpol	0	145	485.243955	199.07896	145	0	145	0	155	0	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	300	40.503397	70.597156	300	155	145	0	0	0	0
Z3-alpha	0	300	62.684488	92.846602	300	155	145	0	0	0	0
cvc5	0	300	114.899111	144.913468	300	155	145	0	0	0	0
OpenSMT	0	299	175.549634	205.67258	299	155	144	0	1	0	0
SMTInterpol	0	297	636.577052	288.487764	297	152	145	0	3	0	0