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

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 1 0.336 0.33611000 0
MathSATn 0 1 2.267 2.26711000 0
cvc5 0 1 2.541 2.5411000 0
2021-cvc5n 0 1 6.673 6.67311000 0
z3-4.8.17n 0 1 89.212 89.29211000 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 10.3360.33611000 0
MathSATn 0 12.2672.26711000 0
cvc5 0 12.5412.5411000 0
2021-cvc5n 0 16.6736.67311000 0
z3-4.8.17n 0 189.21289.29211000 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Bitwuzla 0 10.3360.336110000 0
MathSATn 0 12.2672.267110000 0
cvc5 0 12.5412.54110000 0
2021-cvc5n 0 16.6736.673110000 0
z3-4.8.17n 0 189.21289.292110000 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2021-cvc5n 0 00.00.0000010 0
Bitwuzla 0 00.00.0000010 0
cvc5 0 00.00.0000010 0
MathSATn 0 00.00.0000010 0
z3-4.8.17n 0 00.00.0000010 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 10.3360.33611000 0
MathSATn 0 12.2672.26711000 0
cvc5 0 12.5412.5411000 0
2021-cvc5n 0 16.6736.67311000 0
z3-4.8.17n 0 024.024.000011 0

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