Arith (Single Query Track)

Competition results for the Arith division in the Single Query Track.

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

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

Logics:

• LIA : 300 benchmarks
• LRA : 1003 benchmarks
• NIA : 208 benchmarks
• NRA : 99 benchmarks

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2021-z3n	0	1421	170603.567	170614.779	1421	581	840	189	0	105	0
z3-4.8.17n	0	1414	272643.369	272653.379	1414	578	836	196	0	191	0
cvc5	0	1410	265415.73	265612.1	1410	552	858	200	0	200	0
YicesQS	0	1359	301582.231	301629.241	1359	568	791	251	0	250	0
UltimateEliminator+MathSAT	0	1210	365335.856	359169.993	1210	433	777	400	0	282	0
Vampire	0	787	1037507.403	996673.016	787	3	784	823	0	819	0
smtinterpol	0	261	186009.206	181129.144	261	9	252	1042	307	136	0
veriT	0	75	24505.539	24482.283	75	0	75	225	1310	19	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2021-z3n	0	1421	170618.417	170610.989	1421	581	840	189	0	105	0
z3-4.8.17n	0	1414	272658.159	272646.379	1414	578	836	196	0	191	0
cvc5	0	1410	265589.23	265602.44	1410	552	858	200	0	200	0
YicesQS	0	1359	301618.421	301618.791	1359	568	791	251	0	250	0
UltimateEliminator+MathSAT	0	1212	365409.656	359080.563	1212	435	777	398	0	280	0
Vampire	0	790	1169413.233	994363.407	790	3	787	820	0	816	0
smtinterpol	0	261	186009.206	181129.144	261	9	252	1042	307	136	0
veriT	0	75	24507.659	24481.683	75	0	75	225	1310	19	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2021-z3n	0	581	42956.1	42955.83	581	581	0	39	990	105	0
z3-4.8.17n	0	578	57906.223	57903.647	578	578	0	42	990	191	0
YicesQS	0	568	62451.361	62451.56	568	568	0	52	990	250	0
cvc5	0	552	88246.3	88231.655	552	552	0	68	990	200	0
UltimateEliminator+MathSAT	0	435	199212.279	196217.767	435	435	0	185	990	280	0
smtinterpol	0	9	140403.124	138233.128	9	9	0	536	1065	136	0
Vampire	0	3	837607.985	740247.579	3	3	0	617	990	816	0
veriT	0	0	1196.067	1186.716	0	0	0	137	1473	19	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	858	176142.93	176170.785	858	0	858	131	621	200	0
2021-z3n	0	840	126462.316	126455.159	840	0	840	149	621	105	0
z3-4.8.17n	0	836	213551.936	213542.732	836	0	836	153	621	191	0
YicesQS	0	791	237967.06	237967.231	791	0	791	198	621	250	0
Vampire	0	787	330605.248	252915.828	787	0	787	202	621	816	0
UltimateEliminator+MathSAT	0	777	166192.658	162860.008	777	0	777	212	621	280	0
smtinterpol	0	252	45606.081	42896.016	252	0	252	506	852	136	0
veriT	0	75	23311.592	23294.968	75	0	75	88	1447	19	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
YicesQS	0	1344	6718.319	6718.574	1344	556	788	266	0	265	0
2021-z3n	0	1306	7009.611	6997.344	1306	557	749	304	0	227	0
z3-4.8.17n	0	1297	8743.814	8728.563	1297	553	744	313	0	313	0
cvc5	0	1280	8622.774	8612.808	1280	495	785	330	0	330	0
UltimateEliminator+MathSAT	0	1149	17458.747	13054.634	1149	405	744	461	0	344	0
Vampire	0	495	28451.989	27231.488	495	3	492	1115	0	1114	0
smtinterpol	0	255	10116.584	6790.569	255	9	246	1048	307	200	0
veriT	0	75	804.494	778.296	75	0	75	225	1310	24	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.