SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_Bitvec_Arith (Incremental Track)

Competition results for the QF_Equality_Bitvec_Arith division in the Incremental Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Yices2 - - Yices2

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Unsolved Abstained Timeout Memout
Yices2 0 17283 20353.58 20360.63 0 1046 0 15 0
SMTInterpol 0 17204 99021.90 97321.76 0 1046 0 50 0
cvc5 0 17175 83472.93 83492.73 0 1046 0 58 4

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Unsolved Abstained Timeout Memout
Yices2 0 17030 994.29 994.29 0 1007 39 2 0
cvc5 0 15867 1507.49 1507.49 0 879 167 8 0
SMTInterpol 0 14177 3255.79 3255.79 0 850 196 2 0