SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

Largest Contribution Ranking - Unsat Core Track

Page generated on 2021-07-18 17:31:37 +0000

Winners

Sequential Performance Parallel Performance
cvc5-uc cvc5-uc

Sequential Performance

Solver Correct Score Time Score Division
cvc5-uc 0.30384024 0.55415168 Equality+LinearArith
cvc5-uc 0.04913906 0.05938823 Equality
cvc5-uc 0.01421682 0.04331043 Equality+NonLinearArith
cvc5-uc 0.01014006 0.00206619 QF_Equality
Yices2 0.00719293 0.00235458 QF_Equality+LinearArith
cvc5-uc 0.00595642 0.00020911 Arith
cvc5-uc 0.00269884 0.00097884 QF_Bitvec
cvc5-uc 0.00139313 0.00086424 QF_Equality+Bitvec
cvc5-uc 0.0006712 0.00046508 QF_LinearIntArith
Yices2 0.00061889 0.00098661 QF_LinearRealArith

Parallel Performance

Solver Correct Score Time Score Division
cvc5-uc 0.30304423 0.53787669 Equality+LinearArith
cvc5-uc 0.04883744 0.0579719 Equality
cvc5-uc 0.01304166 0.04355396 Equality+NonLinearArith
cvc5-uc 0.00908387 0.00063631 QF_Equality
Yices2 0.0070977 0.00212395 QF_Equality+LinearArith
cvc5-uc 0.00595642 0.000209 Arith
cvc5-uc 0.00269884 0.0010049 QF_Bitvec
cvc5-uc 0.00139313 0.00081231 QF_Equality+Bitvec
cvc5-uc 0.00067015 0.00050061 QF_LinearIntArith
Yices2 0.00061813 0.00087431 QF_LinearRealArith

n Non-competing.
e Experimental.