SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2023

Rules
Benchmarks
Specs
Model Validation Track
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

Largest Contribution Ranking - Incremental Track

Page generated on 2023-07-06 16:05:26 +0000

Winners

Parallel Performance
cvc5

Parallel Performance

Solver Correct Score Time Score Division
cvc5 0.09119607 0.0001214 Equality
cvc5 0.06845721 0.01857075 Equality+NonLinearArith
Yices2 0.02804122 0.04534255 QF_Equality+LinearArith
cvc5 0.00140228 0.00024359 Equality+LinearArith
Yices2 0.00102606 0.00198779 QF_LinearIntArith
Bitwuzla 0.00095845 0.05196635 QF_Equality+Bitvec
Bitwuzla 0.00076854 0.0043158 QF_Bitvec
SMTInterpol 0.00049581 0.00052944 QF_NonLinearIntArith
Bitwuzla 0.00027731 0.00052002 FPArith
Bitwuzla 0.00018095 0.0002292 Equality+MachineArith
cvc5 0.00011741 0.0007693 Bitvec
OpenSMT 0.00010723 0.00022203 QF_LinearRealArith
Yices2 7.64e-06 0.03152066 QF_Equality+NonLinearArith
cvc5 0.0 0.05877938 QF_Equality
cvc5 0.0 0.00042655 Arith

n Non-competing.
e Experimental.