SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

QF_UFBV (Single Query Track)

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

Page generated on 2021-07-18 17:29:07 +0000

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-Bitwuzlan 0 288 17603.503 17578.776288163125125 0
Bitwuzla 0 286 44136.186 44085.632861621241414 0
cvc5 0 261 78005.906 78007.9142611521093939 0
2020-Yices2n 0 251 85127.472 85136.655251162894949 0
2020-Yices2-fixedn 0 250 85535.754 85533.792250162885050 0
Yices2 0 249 85015.687 84993.698249162875151 0
z3n 0 246 84393.371 84403.8252461421045454 0
MathSAT5n 0 237 96298.654 96287.23237145926363 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-Bitwuzlan 0 28817604.12317578.616288163125125 0
Bitwuzla 0 28644137.44644085.042861621241414 0
cvc5 0 26178014.32678006.4242611521093939 0
2020-Yices2n 0 25185132.02285134.955251162894949 0
2020-Yices2-fixedn 0 25085540.66485532.172250162885050 0
Yices2 0 24985019.37784992.338249162875151 0
z3n 0 24684401.37184401.7252461421045454 0
MathSAT5n 0 23796312.53496284.36237145926363 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-Bitwuzlan 0 1633194.8783195.226163163011365 0
Bitwuzla 0 1624058.8794025.1771621620213614 0
2020-Yices2n 0 1624512.0554512.4791621620213649 0
Yices2 0 1624527.3224527.6861621620213651 0
2020-Yices2-fixedn 0 1624538.9974528.4781621620213650 0
cvc5 0 15221182.65721180.10315215201213639 0
MathSAT5n 0 14524138.34124124.75714514501913663 0
z3n 0 14230668.56430666.52314214202213654 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-Bitwuzlan 0 12514409.24514383.391250125111645 0
Bitwuzla 0 12440078.56740059.86312401241216414 0
cvc5 0 10956831.66956826.32110901092716439 0
z3n 0 10453732.80853735.20210401043216454 0
MathSAT5n 0 9272174.19372159.603920924416463 0
2020-Yices2n 0 8980619.96780622.476890894716449 0
2020-Yices2-fixedn 0 8881001.66781003.694880884816450 0
Yices2 0 8780492.05580464.653870874916451 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-Yices2n 0 1952857.5562857.72919515144105105 0
2020-Yices2-fixedn 0 1952868.5212857.75719515144105105 0
Yices2 0 1952862.7342862.77519515144105105 0
2020-Bitwuzlan 0 1953021.7183021.8711951365910598 0
Bitwuzla 0 1893250.6983227.79418913653111111 0
MathSAT5n 0 1693747.4773715.38716912940131131 0
z3n 0 1474356.6884354.00414711136153153 0
cvc5 0 1424640.4994625.85114210735158158 0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.