SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

ABV (Single Query Track)

Competition results for the ABV logic in the Single Query Track.

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5cvc5cvc5cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc508375468.849025553.55471837327510165006460
SMTInterpol03915946.9716175066.29444339145346209602330
Bitwuzla0207256.915585277.7114842071822522800810

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc508375468.849025553.55471837327510165006460
SMTInterpol03915946.9716175066.29444339145346209602330
Bitwuzla0207256.915585277.7114842071822522800810

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc503272649.2302482682.4439413273270116204480
Bitwuzla018224.48697242.67872918218202612044280
SMTInterpol04533.13974324.35825645450398204440

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc505102819.6187712871.1107685100510181959180
SMTInterpol03465913.8318745041.93618834603461821959200
Bitwuzla025232.428613235.03275525025503195970

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50786923.5209161002.125078786294492108159300
SMTInterpol0370461.807427296.3667937045325174137600
Bitwuzla020627.95738748.5499832061822421928900