SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

BVFP (Single Query Track)

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

Page generated on 2022-08-10 11:17:44 +0000

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 177 31681.238 31688.136177165122824 0
cvc5 0 171 48662.935 48996.93817116473434 0
Bitwuzla 0 148 68193.382 68164.812148134145756 0
2021-cvc5n 0 128 92794.235 94019.20412812177777 0
UltimateEliminator+MathSAT 0 25 1379.402 980.684252501800 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 17731686.95831687.046177165122824 0
cvc5 0 17148809.56548995.40817116473434 0
Bitwuzla 0 14868201.65268162.652148134145756 0
2021-cvc5n 0 12894011.34294015.64412812177777 0
UltimateEliminator+MathSAT 0 251379.402980.684252501800 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
z3-4.8.17n 0 16527153.57427153.5881651650221824 0
cvc5 0 16434678.91734864.5451641640231834 0
Bitwuzla 0 13462504.47462465.1991341340531856 0
2021-cvc5n 0 12180130.15480134.0771211210661877 0
UltimateEliminator+MathSAT 0 251283.094903.86125250162180 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Bitwuzla 0 14897.179897.45414014019156 0
z3-4.8.17n 0 123303.8113303.8712012219124 0
2021-cvc5n 0 79081.1889081.567707719177 0
cvc5 0 79330.6489330.863707719134 0
UltimateEliminator+MathSAT 0 077.18360.99000141910 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 1671020.8141020.52216716073835 0
Bitwuzla 0 1451474.8041474.82145133126059 0
cvc5 0 1391614.091614.04113913906666 0
2021-cvc5n 0 1212052.9692052.38412111838484 0
UltimateEliminator+MathSAT 0 191209.106825.343191901866 0

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