SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Equality_LinearArith (Unsat Core Track)

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

Results were generated on 2025-08-11

Benchmarks: 23881
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 1838260 86720.92 89685.63 23694 23694 187 0 147 0
SMTInterpol 0 1135870 162362.54 121006.27 20252 20252 3629 0 2918 0
UltimateEliminator+MathSAT 1 9445 3542.56 1644.80 655 655 14630 8596 6 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 1838260 86720.92 89685.63 23694 23694 187 0 147 0
SMTInterpol 0 1136929 184090.00 135617.90 20252 20252 3629 0 2918 0
UltimateEliminator+MathSAT 1 9445 3542.56 1644.80 655 655 14630 8596 6 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 1838260 86720.92 89685.63 23694 23694 187 0 147 0
SMTInterpol 0 1136929 184090.00 135617.90 20252 20252 3629 0 2918 0
UltimateEliminator+MathSAT 1 9445 3542.56 1644.80 655 655 14630 8596 6 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 1753279 8212.92 11122.14 23337 23337 21 523 0 0
SMTInterpol 0 1097346 42471.57 22302.63 19722 19722 70 4089 0 0
UltimateEliminator+MathSAT 1 8860 3367.67 1478.77 654 654 14619 8608 0 0