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

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

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

Benchmarks: 34
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
Yices2-fixedn 0 25 15017.022 15019.2212581799 0
2019-Yices 2.6.2n 0 25 15038.346 15040.0812581799 0
Yices2 0 25 15127.059 15129.1822581799 0
z3n 0 19 19206.98 19211.257194151515 0
MathSAT5n 0 17 22764.421 22769.753173141717 0
Bitwuzla 0 14 5399.081 5401.90914410204 0
Bitwuzla-fixedn 0 14 5402.079 5403.64814410204 0
CVC4 0 11 26776.435 27711.066111102323 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2-fixedn 0 25 15018.192 15018.9112581799 0
2019-Yices 2.6.2n 0 25 15039.206 15039.7712581799 0
Yices2 0 25 15128.229 15128.7922581799 0
z3n 0 19 19210.24 19210.607194151515 0
MathSAT5n 0 17 22768.631 22769.113173141717 0
Bitwuzla 0 14 5401.291 5401.63914410204 0
Bitwuzla-fixedn 0 14 5403.009 5403.38814410204 0
CVC4 0 11 27709.925 27709.926111102323 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2-fixedn 0 8 7104.92 7105.556880269 0
2019-Yices 2.6.2n 0 8 7126.662 7127.088880269 0
Yices2 0 8 7128.94 7129.456880269 0
Bitwuzla 0 4 562.554 562.814440304 0
Bitwuzla-fixedn 0 4 563.406 563.636440304 0
z3n 0 4 8767.423 8767.624403015 0
MathSAT5n 0 3 9766.923 9766.9473303117 0
CVC4 0 1 12081.038 12081.041103323 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 17 3112.544 3112.68317017179 0
Yices2-fixedn 0 17 3113.272 3113.35517017179 0
Yices2 0 17 3199.288 3199.33617017179 0
z3n 0 15 5642.817 5642.987150151915 0
MathSAT5n 0 14 8201.709 8202.167140142017 0
Bitwuzla 0 10 38.737 38.82510010244 0
Bitwuzla-fixedn 0 10 39.603 39.75210010244 0
CVC4 0 10 10828.887 10828.886100102423 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 16 468.288 468.29162141818 0
Yices2 0 16 469.117 469.13162141818 0
Yices2-fixedn 0 16 469.24 469.245162141818 0
z3n 0 13 558.623 558.631132112121 0
MathSAT5n 0 11 567.898 567.914111102323 0
Bitwuzla 0 10 196.231 196.3911019248 0
Bitwuzla-fixedn 0 10 196.191 196.431019248 0
CVC4 0 10 604.887 604.886100102424 0

n Non-competing.