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

QF_AUFBV (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 27 15250.847 15253.9042712151111 0
z3-4.8.17n 0 21 20695.22 20700.52217141716 0
MathSATn 0 20 24441.721 24446.703208121818 0
Bitwuzla 0 19 6076.237 6078.58519109194 0
2020-Bitwuzlan 0 18 5415.101 5416.71618108204 0
cvc5 0 14 29134.137 30267.05914592424 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 2715253.19715253.4542712151111 0
z3-4.8.17n 0 2120699.5220699.79217141716 0
MathSATn 0 2024445.11124445.673208121818 0
Bitwuzla 0 196077.8776078.33519109194 0
2020-Bitwuzlan 0 185416.1815416.50618108204 0
cvc5 0 1430257.59730265.62914592424 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Yices2 0 127625.5057625.6881212052111 0
2020-Bitwuzlan 0 10575.176575.414101007214 0
Bitwuzla 0 101237.1941237.604101007214 0
MathSATn 0 811018.37311018.41588092118 0
z3-4.8.17n 0 712399.53512399.592770102116 0
cvc5 0 514714.53414714.552550122124 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Yices2 0 152827.6922827.7661501522111 0
z3-4.8.17n 0 144430.9844431.1851401432116 0
MathSATn 0 128626.7388627.2581201252118 0
Bitwuzla 0 940.68340.7319098214 0
cvc5 0 910743.06310751.07790982124 0
2020-Bitwuzlan 0 841.00541.0928089214 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 20464.835464.868208121818 0
Bitwuzla 0 15209.79209.8191578238 0
2020-Bitwuzlan 0 14200.44200.5851477248 0
MathSATn 0 14629.779629.80814682424 0
z3-4.8.17n 0 12688.3688.29912482626 0
cvc5 0 11692.142692.14211472727 0

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