SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Equality_NonLinearArith (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 10232
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 cvc5

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 6722 268105.11 268967.71 6722 712 6010 3510 0 3136 1
iProver v3.9.3 0 3992 393224.91 103781.36 4511 0 4511 5721 0 5682 39
SMTInterpol 0 2924 22955.33 15345.68 2924 80 2844 7308 0 3404 0
UltimateEliminator+MathSAT 0 619 9612.56 8253.36 619 434 185 6341 3272 476 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 6722 268105.11 268967.71 6722 712 6010 3510 0 3136 1
iProver v3.9.3 0 4511 1893686.16 481584.81 4511 0 4511 5721 0 5682 39
SMTInterpol 0 2924 22955.33 15345.68 2924 80 2844 7308 0 3404 0
UltimateEliminator+MathSAT 0 619 9612.56 8253.36 619 434 185 6341 3272 476 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 712 31881.73 31973.82 712 712 0 81 9439 5 0
UltimateEliminator+MathSAT 0 434 8600.11 7645.99 434 434 0 359 9439 236 0
SMTInterpol 0 80 56.08 45.04 80 80 0 713 9439 59 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 793 9439 793 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 6010 236223.38 236993.89 6010 0 6010 371 3851 297 1
iProver v3.9.3 0 4511 1893686.16 481584.81 4511 0 4511 1870 3851 1831 39
SMTInterpol 0 2844 22899.25 15300.64 2844 0 2844 3537 3851 1762 0
UltimateEliminator+MathSAT 0 185 1012.45 607.37 185 0 185 3244 6803 148 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
cvc5 0 5875 4500.96 5224.86 5875 642 5233 362 3995 0 0
iProver v3.9.3 0 3116 39898.25 12635.10 3116 0 3116 0 7116 0 0
SMTInterpol 0 2876 9704.94 4353.16 2876 80 2796 2700 4656 0 0
UltimateEliminator+MathSAT 0 590 3617.73 2332.73 590 407 183 5806 3836 0 0