SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2024

QF_LinearRealArith (Model Validation Track)

Competition results for the QF_LinearRealArith division in the Model Validation Track.

Results were generated on 2024-07-08

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

Logics:

QF_LRA : 494 benchmarks
QF_RDL : 109 benchmarks

Winners

winner_seq	winner_par	winner_sat	winner_unsat	winner_24s
OpenSMT	OpenSMT	OpenSMT	-	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	590	18255.579166	18319.779283	590	590	0	13	0	13	0
Yices2	0	581	5075.37714	5134.84092	581	581	0	22	0	22	0
cvc5	0	581	19612.46327	19673.202809	581	581	0	22	0	22	0
SMTInterpol	0	572	36437.901157	31212.31038	572	572	0	31	0	29	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	590	18255.579166	18319.779283	590	590	0	13	0	13	0
Yices2	0	581	5075.37714	5134.84092	581	581	0	22	0	22	0
cvc5	0	581	19612.46327	19673.202809	581	581	0	22	0	22	0
SMTInterpol	0	572	36437.901157	31212.31038	572	572	0	31	0	29	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	590	18255.579166	18319.779283	590	590	0	13	0	13	0
Yices2	0	581	5075.37714	5134.84092	581	581	0	22	0	22	0
cvc5	0	581	19612.46327	19673.202809	581	581	0	22	0	22	0
SMTInterpol	0	572	36437.901157	31212.31038	572	572	0	31	0	29	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	544	810.120489	864.808291	544	544	0	0	59	0	0
OpenSMT	0	508	986.034057	1037.113991	508	508	0	0	95	0	0
cvc5	0	473	1042.711134	1090.131475	473	473	0	0	130	0	0
SMTInterpol	0	432	2916.089515	1261.204069	432	432	0	0	171	0	0