SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Equality_NonLinearArith (Unsat Core Track)

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

Results were generated on 2025-08-11

Benchmarks: 5682
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 458029 129829.33 130479.15 5099 5099 583 0 475 1
SMTInterpol 0 220570 23448.24 15960.16 3377 3377 2305 0 1276 0
UltimateEliminator+MathSAT 0 683 2478.29 1899.50 158 158 2768 2756 154 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 458029 129829.33 130479.15 5099 5099 583 0 475 1
SMTInterpol 0 220570 23448.24 15960.16 3377 3377 2305 0 1276 0
UltimateEliminator+MathSAT 0 683 2478.29 1899.50 158 158 2768 2756 154 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 458029 129829.33 130479.15 5099 5099 583 0 475 1
SMTInterpol 0 220570 23448.24 15960.16 3377 3377 2305 0 1276 0
UltimateEliminator+MathSAT 0 683 2478.29 1899.50 158 158 2768 2756 154 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 326020 2530.63 3103.66 4630 4630 79 973 0 0
SMTInterpol 0 204716 10445.43 4968.36 3335 3335 445 1902 0 0
UltimateEliminator+MathSAT 0 649 932.03 516.64 140 140 2469 3073 0 0