SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_AUFBVFP (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Bitwuzla Bitwuzla Bitwuzla - Bitwuzla

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 1 0.25 0.37 1 1 0 0 0 0 0
cvc5 0 1 1.43 1.55 1 1 0 0 0 0 0
COLIBRI 0 0 0.00 0.00 0 0 0 1 0 1 0
colibri2 0 0 0.00 0.00 0 0 0 1 0 1 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 1 0.25 0.37 1 1 0 0 0 0 0
cvc5 0 1 1.43 1.55 1 1 0 0 0 0 0
COLIBRI 0 0 0.00 0.00 0 0 0 1 0 1 0
colibri2 0 0 0.00 0.00 0 0 0 1 0 1 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 1 0.25 0.37 1 1 0 0 0 0 0
cvc5 0 1 1.43 1.55 1 1 0 0 0 0 0
COLIBRI 0 0 0.00 0.00 0 0 0 1 0 1 0
colibri2 0 0 0.00 0.00 0 0 0 1 0 1 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 1 0.25 0.37 1 1 0 0 0 0 0
cvc5 0 1 1.43 1.55 1 1 0 0 0 0 0