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

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-Bitwuzla-fixedn 0 484 2101.451 2099.87948422126300 0
2020-Bitwuzlan 0 484 2140.414 2115.66148422126300 0
Bitwuzla 0 484 2578.135 2569.83448422126300 0
cvc5 0 482 4945.124 4909.62548222126122 0
2020-CVC4n 0 482 5361.275 5311.73348222126122 0
MathSAT5n 0 478 10344.199 10343.63347822125766 0
2020-MathSAT5n 0 478 10462.524 10438.29647822125766 0
z3n 0 477 16432.982 16378.25547722125677 0
2020-COLIBRIn 0 451 3086.423 3087.23451214237332 0
COLIBRI - fixedn 0 451 3354.019 3354.624451214237332 0
COLIBRI 4 447 2813.715 2812.891447210237372 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-Bitwuzla-fixedn 0 4842101.4512099.87948422126300 0
2020-Bitwuzlan 0 4842140.4142115.66148422126300 0
Bitwuzla 0 4842578.1352569.83448422126300 0
cvc5 0 4824945.7044909.57548222126122 0
2020-CVC4n 0 4825362.4355311.66348222126122 0
MathSAT5n 0 47810344.65910343.35347822125766 0
2020-MathSAT5n 0 47810463.53410437.98647822125766 0
z3n 0 47716433.75216377.79547722125677 0
2020-COLIBRIn 0 4513086.4933087.17451214237332 0
COLIBRI - fixedn 0 4513354.4293354.494451214237332 0
COLIBRI 4 4472813.8452812.831447210237372 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Bitwuzla 0 221181.982178.279221221002630 0
2020-Bitwuzla-fixedn 0 221237.728235.528221221002630 0
2020-Bitwuzlan 0 221236.587236.667221221002630 0
cvc5 0 221638.875628.195221221002632 0
2020-CVC4n 0 221725.248722.4221221002632 0
MathSAT5n 0 2211172.7991173.152221221002636 0
2020-MathSAT5n 0 2211213.1411213.468221221002636 0
z3n 0 2212089.1092089.739221221002637 0
COLIBRI - fixedn 0 2141446.7181445.523214214072632 0
2020-COLIBRIn 0 2141528.8511529.399214214072632 0
COLIBRI 0 2101429.9831428.6442102100112632 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-Bitwuzla-fixedn 0 2631863.7241864.351263026302210 0
2020-Bitwuzlan 0 2631903.8261878.994263026302210 0
Bitwuzla 0 2632396.1522391.555263026302210 0
cvc5 0 2614306.8294281.381261026122212 0
2020-CVC4n 0 2614637.1874589.263261026122212 0
MathSAT5n 0 2579171.8619170.201257025762216 0
2020-MathSAT5n 0 2579250.3939224.518257025762216 0
z3n 0 25614344.64214288.056256025672217 0
2020-COLIBRIn 0 2371557.6421557.7712370237262212 0
COLIBRI - fixedn 0 2371907.7111908.9712370237262212 0
COLIBRI 4 2371383.8621384.1872370237262212 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 474734.209725.7594742202541010 0
2020-Bitwuzla-fixedn 0 473726.453724.4184732192541111 0
2020-Bitwuzlan 0 473724.72724.9394732192541111 0
2020-CVC4n 0 4671433.3671429.1554672142531717 0
cvc5 0 4651815.0681778.7834652162491919 0
MathSAT5n 0 4551340.5951338.6134552142412929 0
2020-MathSAT5n 0 4531400.6341374.4714532142393131 0
COLIBRI - fixedn 0 449548.032548.078449214235354 0
2020-COLIBRIn 0 446666.054666.712446212234387 0
z3n 0 4202682.1552677.9624201992216464 0
COLIBRI 4 447461.845460.831447210237372 0

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