QF_Equality+NonLinearArith (Single Query Track)

Competition results for the QF_Equality+NonLinearArith division in the Single Query Track.

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

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

Logics:

• QF_ANIA : 102 benchmarks
• QF_AUFNIA : 9 benchmarks
• QF_UFNIA : 249 benchmarks
• QF_UFNRA : 27 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
cvc5	cvc5	cvc5	cvc5	cvc5

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-CVC4n	0	326	53841.198	53846.879	326	241	85	61	0	41	0
cvc5	0	326	80172.798	80165.064	326	241	85	61	0	61	0
z3-4.8.17n	0	322	81521.229	81526.795	322	229	93	65	0	65	0
MathSATn	0	260	91464.508	91474.776	260	194	66	127	0	73	0
Yices2	0	246	43418.604	43424.827	246	194	52	30	111	30	0
smtinterpol	0	169	13739.711	13207.968	169	131	38	218	0	10	0
veriT+raSAT+Redlog	0	1	31196.498	31200.824	1	1	0	26	360	26	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-CVC4n	0	326	53847.908	53845.539	326	241	85	61	0	41	0
cvc5	0	326	80184.058	80162.454	326	241	85	61	0	61	0
z3-4.8.17n	0	322	81533.939	81524.205	322	229	93	65	0	65	0
MathSATn	0	260	91471.398	91471.796	260	194	66	127	0	73	0
Yices2	0	246	43422.884	43423.767	246	194	52	30	111	30	0
smtinterpol	0	169	13739.711	13207.968	169	131	38	218	0	10	0
veriT+raSAT+Redlog	0	1	31200.008	31200.014	1	1	0	26	360	26	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-CVC4n	0	241	33819.354	33820.091	241	241	0	34	112	41	0
cvc5	0	241	46869.422	46851.472	241	241	0	34	112	61	0
z3-4.8.17n	0	229	58522.484	58513.938	229	229	0	46	112	65	0
Yices2	0	194	11020.664	11021.476	194	194	0	3	190	30	0
MathSATn	0	194	52907.407	52907.635	194	194	0	81	112	73	0
smtinterpol	0	131	835.14	557.715	131	131	0	144	112	10	0
veriT+raSAT+Redlog	0	1	27600.008	27600.014	1	1	0	23	363	26	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	93	15811.454	15810.268	93	0	93	13	281	65	0
2020-CVC4n	0	85	17627.427	17624.32	85	0	85	21	281	41	0
cvc5	0	85	26114.636	26110.982	85	0	85	21	281	61	0
MathSATn	0	66	31363.991	31364.161	66	0	66	40	281	73	0
Yices2	0	52	25202.22	25202.291	52	0	52	21	314	30	0
smtinterpol	0	38	12901.128	12647.97	38	0	38	68	281	10	0
veriT+raSAT+Redlog	0	0	2400.0	2400.0	0	0	0	2	385	26	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	303	2342.661	2332.462	303	212	91	84	0	84	0
2020-CVC4n	0	299	1830.174	1826.895	299	220	79	88	0	68	0
cvc5	0	288	2762.967	2740.611	288	212	76	99	0	99	0
MathSATn	0	247	2418.008	2418.134	247	185	62	140	0	86	0
Yices2	0	224	1276.121	1276.273	224	172	52	52	111	52	0
smtinterpol	0	163	1037.833	697.431	163	130	33	224	0	16	0
veriT+raSAT+Redlog	0	1	624.008	624.014	1	1	0	26	360	26	0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.