SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Equality (Unsat Core Track)

Competition results for the Equality division in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 845518 19072.98 19410.45 2672 2672 26 0 24 0
SMTInterpol 0 488029 64959.36 50355.57 1590 1590 1108 0 651 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 1704 994 0 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 845518 19072.98 19410.45 2672 2672 26 0 24 0
SMTInterpol 0 488426 69130.72 52501.10 1590 1590 1108 0 651 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 1704 994 0 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 845518 19072.98 19410.45 2672 2672 26 0 24 0
SMTInterpol 0 488426 69130.72 52501.10 1590 1590 1108 0 651 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 1704 994 0 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 802053 1090.80 1407.52 2526 2526 2 170 0 0
SMTInterpol 0 421171 8498.15 4086.01 1344 1344 4 1350 0 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 1704 994 0 0