SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

AUFLIA (Single Query Track)

Competition results for the AUFLIA logic in the Single Query Track. Chart

Results were generated on 2025-08-11

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

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 1432 31250.19 31430.15 1432 175 1257 231 0 220 1
iProver v3.9.3 0 1242 20114.63 6088.77 1246 0 1246 417 0 315 0
SMTInterpol 0 1087 20316.57 15644.97 1090 83 1007 573 0 401 0
UltimateEliminator+MathSAT 0 83 363.70 168.07 83 24 59 1580 0 0 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 1432 31250.19 31430.15 1432 175 1257 231 0 220 1
iProver v3.9.3 0 1246 27323.49 7914.71 1246 0 1246 417 0 315 0
SMTInterpol 0 1090 24676.19 18981.30 1090 83 1007 573 0 401 0
UltimateEliminator+MathSAT 0 83 363.70 168.07 83 24 59 1580 0 0 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 175 17793.08 17816.22 175 175 0 9 1479 0 0
SMTInterpol 0 82 40.99 38.97 82 82 0 102 1479 20 0
UltimateEliminator+MathSAT 0 24 100.97 47.24 24 24 0 160 1479 0 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 184 1479 83 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 1257 13457.11 13613.93 1257 0 1257 23 383 23 0
iProver v3.9.3 0 1246 27323.49 7914.71 1246 0 1246 34 383 34 0
SMTInterpol 0 1007 24633.82 18941.58 1007 0 1007 273 383 219 0
UltimateEliminator+MathSAT 0 59 262.74 120.83 59 0 59 1221 383 0 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 1268 411.87 568.22 1268 119 1149 9 386 0 0
iProver v3.9.3 0 1171 6425.56 2447.67 1171 0 1171 84 408 0 0
SMTInterpol 0 1019 3227.16 1603.27 1019 83 936 95 549 0 0
UltimateEliminator+MathSAT 0 83 363.70 168.07 83 24 59 1577 3 0 0