SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

FPArith (Single Query Track)

Competition results for the FPArith division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Bitwuzla 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 1751 30946.12 31170.01 1751 566 1185 98 0 98 0
cvc5 0 1697 29165.35 29378.99 1697 514 1183 152 0 150 1
UltimateEliminator+MathSAT 0 272 39903.61 39231.26 272 103 169 1577 0 90 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 1751 30946.12 31170.01 1751 566 1185 98 0 98 0
cvc5 0 1697 29165.35 29378.99 1697 514 1183 152 0 150 1
UltimateEliminator+MathSAT 0 272 39903.61 39231.26 272 103 169 1577 0 90 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 566 11487.55 11560.42 566 566 0 1 1282 1 0
cvc5 0 514 19842.30 19908.59 514 514 0 53 1282 52 0
UltimateEliminator+MathSAT 0 103 39183.55 38880.75 103 103 0 464 1282 61 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 1185 19458.57 19609.59 1185 0 1185 27 637 27 0
cvc5 0 1183 9323.05 9470.39 1183 0 1183 29 637 29 0
UltimateEliminator+MathSAT 0 169 720.06 350.51 169 0 169 1043 637 9 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 1612 1218.75 1419.00 1612 487 1125 0 237 0 0
cvc5 0 1598 1683.66 1881.23 1598 459 1139 1 250 0 0
UltimateEliminator+MathSAT 0 215 1017.40 544.75 215 46 169 1482 152 0 0