QF_AUFLIA (Single Query Track)

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

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

Benchmarks: 539
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
z3-4.8.17n	0	539	19.567	18.71	539	262	277	0	0	0
Yices2	0	539	21.29	23.246	539	262	277	0	0	0
cvc5	0	539	337.051	334.848	539	262	277	0	0	0
2021-SMTInterpoln	0	539	936.456	396.393	539	262	277	0	0	0
smtinterpol	0	539	1191.834	550.681	539	262	277	0	0	0
MathSATn	0	538	1549.757	1546.33	538	262	276	1	1	0
veriT	0	18	18.281	17.855	18	0	18	521	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	539	19.567	18.71	539	262	277	0	0	0
Yices2	0	539	21.29	23.246	539	262	277	0	0	0
cvc5	0	539	337.051	334.848	539	262	277	0	0	0
2021-SMTInterpoln	0	539	936.456	396.393	539	262	277	0	0	0
smtinterpol	0	539	1191.834	550.681	539	262	277	0	0	0
MathSATn	0	538	1549.857	1546.29	538	262	276	1	1	0
veriT	0	18	18.281	17.855	18	0	18	521	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
z3-4.8.17n	0	262	6.14	5.703	262	262	0	0	277	0	0
Yices2	0	262	6.253	7.42	262	262	0	0	277	0	0
MathSATn	0	262	38.444	38.499	262	262	0	0	277	1	0
2021-SMTInterpoln	0	262	242.296	122.97	262	262	0	0	277	0	0
cvc5	0	262	149.027	148.988	262	262	0	0	277	0	0
smtinterpol	0	262	284.479	168.947	262	262	0	0	277	0	0
veriT	0	0	9.667	9.953	0	0	0	262	277	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
z3-4.8.17n	0	277	13.427	13.007	277	0	277	0	262	0	0
Yices2	0	277	15.037	15.826	277	0	277	0	262	0	0
cvc5	0	277	188.024	185.86	277	0	277	0	262	0	0
2021-SMTInterpoln	0	277	694.16	273.422	277	0	277	0	262	0	0
smtinterpol	0	277	907.354	381.734	277	0	277	0	262	0	0
MathSATn	0	276	1511.413	1507.792	276	0	276	1	262	1	0
veriT	0	18	8.614	7.902	18	0	18	259	262	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	539	19.567	18.71	539	262	277	0	0	0
Yices2	0	539	21.29	23.246	539	262	277	0	0	0
2021-SMTInterpoln	0	539	936.456	396.393	539	262	277	0	0	0
smtinterpol	0	539	1191.834	550.681	539	262	277	0	0	0
MathSATn	0	537	188.197	184.568	537	262	275	2	2	0
cvc5	0	537	330.518	328.308	537	262	275	2	2	0
veriT	0	18	18.281	17.855	18	0	18	521	0	0

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