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_UFLRA (Single Query Track)

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

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

Benchmarks: 432
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-SMTInterpoln 0 431 3979.857 2865.78443125018111 0
Yices2 0 430 2435.753 2436.89443024918122 0
Yices2-fixedn 0 430 2435.76 2437.42943024918122 0
veriT 0 430 2475.953 2476.36743024918122 0
MathSAT5n 0 430 2511.952 2512.6743024918122 0
CVC4 0 430 2994.438 2995.11143024918122 0
SMTInterpol 0 430 4241.553 3214.89743024918122 0
SMTInterpol-fixedn 0 430 4266.487 3218.19243024918122 0
z3n 0 412 24281.095 24283.5334122311812020 0
Alt-Ergo 0 170 138940.3 74346.897170017026232 8

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-SMTInterpoln 0 431 3979.857 2865.78443125018111 0
Yices2 0 430 2435.923 2436.76443024918122 0
Yices2-fixedn 0 430 2435.93 2437.32943024918122 0
veriT 0 430 2476.263 2476.29743024918122 0
MathSAT5n 0 430 2512.562 2512.6243024918122 0
CVC4 0 430 2995.068 2994.99143024918122 0
SMTInterpol 0 430 4241.553 3214.89743024918122 0
SMTInterpol-fixedn 0 430 4266.487 3218.19243024918122 0
z3n 0 412 24282.585 24282.6534122311812020 0
Alt-Ergo 0 172 150111.79 65655.268172017226019 8

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-SMTInterpoln 0 250 2064.865 1399.94825025001821 0
Yices2 0 249 1229.894 1230.33824924901832 0
Yices2-fixedn 0 249 1229.898 1230.67124924901832 0
veriT 0 249 1268.023 1268.07324924901832 0
MathSAT5n 0 249 1301.549 1301.58724924901832 0
CVC4 0 249 1759.028 1759.00524924901832 0
SMTInterpol 0 249 2363.334 1764.0324924901832 0
SMTInterpol-fixedn 0 249 2370.627 1764.50724924901832 0
z3n 0 231 23043.083 23043.132231231020120 0
Alt-Ergo 0 0 103020.926 44808.93600043219 8

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 181 6.029 6.42618101812512 0
Yices2-fixedn 0 181 6.032 6.65918101812512 0
veriT 0 181 8.24 8.22418101812512 0
MathSAT5n 0 181 11.013 11.03318101812512 0
CVC4 0 181 36.04 35.98618101812512 0
z3n 0 181 39.501 39.521181018125120 0
SMTInterpol 0 181 678.22 250.86718101812512 0
SMTInterpol-fixedn 0 181 695.86 253.68518101812512 0
2019-SMTInterpoln 0 181 714.992 265.83518101812511 0
Alt-Ergo 0 172 45890.864 19646.332172017226019 8

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 430 83.923 84.76443024918122 0
Yices2-fixedn 0 430 83.93 85.32943024918122 0
veriT 0 430 124.263 124.29743024918122 0
MathSAT5n 0 429 157.561 157.61842924818133 0
SMTInterpol-fixedn 0 427 1523.489 645.98842724618155 0
SMTInterpol 0 427 1506.36 648.5442724618155 0
2019-SMTInterpoln 0 427 1532.293 656.30642724618155 0
CVC4 0 426 243.183 243.07242624518166 0
z3n 0 409 656.627 656.6714092281812323 0
Alt-Ergo 0 66 13248.031 9138.71766066366307 8

n Non-competing.