SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_Equality_Bitvec (Model Validation Track)

Competition results for the QF_Equality_Bitvec division in the Model Validation Track.

Results were generated on 2024-07-08

Benchmarks: 384
Time Limit: 1200 seconds
Memory Limit: 20480 GB

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2Yices2-Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203835305.1662985344.68910938338301000
Bitwuzla03821874.7833651913.35161638238202020
cvc5037510443.50606310482.34789337537509081
SMTInterpol030325195.81920618023.585043043040800330

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203835305.1662985344.68910938338301000
Bitwuzla03821874.7833651913.35161638238202020
cvc5037510443.50606310482.34789337537509081
SMTInterpol030426453.54279219184.1741973043040800330

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203835305.1662985344.68910938338301000
Bitwuzla03821874.7833651913.35161638238202020
cvc5037510443.50606310482.34789337537509081
SMTInterpol030426453.54279219184.1741973043040800330

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20370273.834468310.986732370370001400
Bitwuzla0361377.634111413.901607361361002300
cvc50329537.928809570.902568329329005500
SMTInterpol02044472.9821031619.5674672042040117900