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

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 211 14843.88 14845.612111298266 0
Yices2-fixedn 0 211 15140.808 15143.2812111298266 0
2019-Yices 2.6.2n 0 210 14972.751 14972.4242101298177 0
Bitwuzla 0 207 3263.061 3263.7420712879100 0
Bitwuzla-fixedn 0 207 3351.628 3327.04120712879100 0
MathSAT5n 0 198 27676.285 27679.823198128701919 0
CVC4 0 197 31531.908 31538.491197128692020 0
z3n 0 186 43601.719 43528.375186124623131 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 211 14844.49 14845.372111298266 0
Yices2-fixedn 0 211 15141.398 15142.9512111298266 0
2019-Yices 2.6.2n 0 210 14973.141 14972.2642101298177 0
Bitwuzla 0 207 3263.061 3263.7420712879100 0
Bitwuzla-fixedn 0 207 3351.628 3327.04120712879100 0
MathSAT5n 0 198 27680.795 27678.973198128701919 0
CVC4 0 197 31539.118 31537.511197128692020 0
z3n 0 186 43605.689 43526.795186124623131 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 129 209.752 209.7851291290886 0
2019-Yices 2.6.2n 0 129 212.658 212.6871291290887 0
Yices2-fixedn 0 129 216.054 216.0911291290886 0
Bitwuzla 0 128 129.713 129.7341281280890 0
Bitwuzla-fixedn 0 128 133.795 131.1841281280890 0
MathSAT5n 0 128 1590.688 1588.12212812808919 0
CVC4 0 128 1646.306 1643.07112812808920 0
z3n 0 124 7406.0 7360.42112412409331 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 82 14634.738 14635.584820821356 0
Yices2-fixedn 0 82 14925.344 14926.86820821356 0
2019-Yices 2.6.2n 0 81 14760.483 14759.577810811367 0
Bitwuzla 0 79 3133.348 3134.007790791380 0
Bitwuzla-fixedn 0 79 3217.833 3195.857790791380 0
MathSAT5n 0 70 26090.107 26090.857007014719 0
CVC4 0 69 29892.811 29894.446906914820 0
z3n 0 62 36199.689 36166.3736206215531 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 198 612.988 613.1219812870199 0
Bitwuzla-fixedn 0 198 642.443 617.24519812870199 0
2019-Yices 2.6.2n 0 188 795.84 794.169188128602929 0
Yices2 0 188 795.276 795.301188128602929 0
Yices2-fixedn 0 188 796.132 796.159188128602929 0
CVC4 0 179 1553.473 1550.237179128513838 0
MathSAT5n 0 177 1376.339 1373.766177125524040 0
z3n 0 156 2043.464 2031.145156109476161 0

n Non-competing.