SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_RDL (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices2Yices2Yices2 Yices2 Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 213 42884.954 42888.3172131051083434 0
Yices2 0 213 43119.556 43110.4592131051083434 0
Yices2-fixedn 0 213 43120.051 43122.6152131051083434 0
CVC4 0 209 52520.291 52520.2042091021073838 0
z3n 0 207 53535.916 53456.854207991084040 0
veriT 0 206 55093.107 55099.7272061021044141 0
MathSAT5n 0 198 66820.566 66785.806198102964949 0
SMTInterpol 0 187 88612.642 87026.63518797906060 0
SMTInterpol-fixedn 0 187 88722.538 87146.63218797906060 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 213 42887.264 42887.5472131051083434 0
Yices2 0 213 43121.186 43109.9192131051083434 0
Yices2-fixedn 0 213 43122.521 43121.8952131051083434 0
CVC4 0 209 52523.661 52518.8242091021073838 0
z3n 0 207 53541.516 53455.484207991084040 0
veriT 0 206 55097.727 55098.4272061021044141 0
MathSAT5n 0 198 66828.686 66784.066198102964949 0
SMTInterpol 0 187 88612.642 87026.63518797906060 0
SMTInterpol-fixedn 0 187 88722.538 87146.63218797906060 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 105 466.779 466.885105105014234 0
Yices2-fixedn 0 105 494.354 494.497105105014234 0
Yices2 0 105 495.218 495.303105105014234 0
veriT 0 102 6701.181 6701.613102102014541 0
CVC4 0 102 6982.237 6976.905102102014538 0
MathSAT5n 0 102 7719.635 7720.442102102014549 0
z3n 0 99 9439.553 9354.5149999014840 0
SMTInterpol 0 97 15648.538 14844.2739797015060 0
SMTInterpol-fixedn 0 97 15665.129 14866.7649797015060 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 108 2820.485 2820.662108010813934 0
Yices2 0 108 3025.968 3014.615108010813934 0
Yices2-fixedn 0 108 3028.167 3027.398108010813934 0
z3n 0 108 4501.963 4500.97108010813940 0
CVC4 0 107 5941.424 5941.919107010714038 0
veriT 0 104 8796.546 8796.814104010414341 0
MathSAT5n 0 96 19509.052 19463.6249609615149 0
SMTInterpol 0 90 33364.104 32582.3629009015760 0
SMTInterpol-fixedn 0 90 33457.409 32679.8679009015760 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 193 1631.563 1631.72919398955454 0
Yices2 0 191 1675.275 1663.87319198935656 0
Yices2-fixedn 0 191 1665.46 1664.65819198935656 0
z3n 0 180 2164.244 2136.67718088926767 0
veriT 0 169 2304.838 2304.86116982877878 0
MathSAT5n 0 165 2471.205 2467.3516589768282 0
CVC4 0 165 2563.289 2557.18516585808282 0
SMTInterpol 0 132 4090.097 3365.3511327260115115 0
SMTInterpol-fixedn 0 132 4066.534 3368.6871327260115115 0

n Non-competing.