SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_UFIDL (Single Query Track)

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

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

Benchmarks: 300
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 298 3107.252 3106.5882987322522 0
Yices2-fixedn 0 298 3122.561 3123.2472987322522 0
Yices2 0 298 3125.209 3125.7362987322522 0
z3n 0 298 4189.782 4185.9172987322522 0
SMTInterpol-fixedn 0 284 31141.602 29274.155284732111616 0
SMTInterpol 0 284 31185.149 29161.75284732111616 0
MathSAT5n 0 283 27266.965 27250.609283732101717 0
veriT 0 275 32446.764 32451.847275732022521 0
CVC4 0 270 50143.226 50117.145270731973030 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 298 3107.392 3106.5282987322522 0
Yices2-fixedn 0 298 3122.661 3123.1472987322522 0
Yices2 0 298 3125.409 3125.6862987322522 0
z3n 0 298 4189.852 4185.8472987322522 0
SMTInterpol 0 284 31185.149 29161.75284732111616 0
SMTInterpol-fixedn 0 284 31141.602 29274.155284732111616 0
MathSAT5n 0 283 27269.975 27249.679283732101717 0
veriT 0 275 32449.884 32450.977275732022521 0
CVC4 0 270 50147.566 50115.955270731973030 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 73 3.783 3.984737302272 0
Yices2 0 73 4.427 4.556737302272 0
Yices2-fixedn 0 73 4.464 4.744737302272 0
veriT 0 73 11.5 11.4877373022721 0
MathSAT5n 0 73 29.795 29.8017373022717 0
z3n 0 73 106.461 102.176737302272 0
SMTInterpol 0 73 306.005 106.8697373022716 0
SMTInterpol-fixedn 0 73 312.403 110.3277373022716 0
CVC4 0 73 752.308 752.3427373022730 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 225 3103.609 3102.5442250225752 0
Yices2-fixedn 0 225 3118.197 3118.4032250225752 0
Yices2 0 225 3120.981 3121.1292250225752 0
z3n 0 225 4083.391 4083.6722250225752 0
SMTInterpol 0 211 30879.143 29054.88121102118916 0
SMTInterpol-fixedn 0 211 30829.199 29163.82821102118916 0
MathSAT5n 0 210 27240.18 27219.87821002109017 0
veriT 0 202 32438.384 32439.4920202029821 0
CVC4 0 197 49395.257 49363.613197019710330 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 293 336.242 335.3452937322077 0
Yices2 0 293 343.059 343.3142937322077 0
Yices2-fixedn 0 293 343.011 343.4352937322077 0
z3n 0 290 596.367 592.123290732171010 0
SMTInterpol 0 258 3488.77 1982.211258731854242 0
SMTInterpol-fixedn 0 258 3390.075 1989.102258731854242 0
veriT 0 256 1383.431 1383.416256731834444 0
MathSAT5n 0 256 1742.391 1720.819256731834444 0
CVC4 0 205 2800.046 2798.523205721339595 0

n Non-competing.