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

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

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

Benchmarks: 394
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
Bitwuzla-fixedn 0 394 778.029 778.41739418620800 0
Bitwuzla 0 394 781.529 777.60439418620800 0
CVC4 0 394 1686.879 1663.3739418620800 0
2019-Par4n 0 393 2699.895 1818.44839318520811 0
MathSAT5n 0 391 5739.129 5737.69339118620533 0
z3n 0 386 13314.509 13313.79638618520188 0
COLIBRI 0 366 3075.447 3076.625366181185282 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 394 781.529 777.60439418620800 0
Bitwuzla-fixedn 0 394 778.029 778.41739418620800 0
CVC4 0 394 1686.879 1663.3739418620800 0
2019-Par4n 0 393 2699.895 1818.44839318520811 0
MathSAT5n 0 391 5739.249 5737.53339118620533 0
z3n 0 386 13315.999 13313.58638618520188 0
COLIBRI 0 366 3075.557 3076.605366181185282 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 186 159.292 159.34718618602080 0
Bitwuzla 0 186 161.223 159.7318618602080 0
MathSAT5n 0 186 382.88 381.88218618602083 0
CVC4 0 186 856.244 837.67118618602080 0
2019-Par4n 0 185 1534.342 1370.64318518502091 0
z3n 0 185 2316.911 2315.64718518502098 0
COLIBRI 0 181 271.591 271.92418118102132 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 208 1165.554 447.80520802081861 0
Bitwuzla 0 208 620.306 617.87420802081860 0
Bitwuzla-fixedn 0 208 618.736 619.0720802081860 0
CVC4 0 208 830.635 825.69920802081860 0
MathSAT5n 0 205 5356.369 5355.65220502051893 0
z3n 0 201 10999.089 10997.93920102011938 0
COLIBRI 0 185 2803.967 2804.68118501852092 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 387 540.718 541.0138718420377 0
Bitwuzla 0 387 545.18 541.22638718420377 0
2019-Par4n 0 387 940.689 543.60338718420377 0
CVC4 0 384 1080.887 1057.2533841832011010 0
MathSAT5n 0 375 1013.913 1011.8523751831921919 0
z3n 0 358 1829.669 1826.6143581771813636 0
COLIBRI 0 356 611.02 611.9783561771793812 0

n Non-competing.