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 PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2--Yices2

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedUnsolvedAbstainedTimeoutMemout
Yices201728320353.5820360.63010460150
SMTInterpol01720499021.9097321.76010460500
cvc501717583472.9383492.73010460584

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedUnsolvedAbstainedTimeoutMemout
Yices2017030994.29994.29010073920
cvc50158671507.491507.49087916780
SMTInterpol0141773255.793255.79085019620