SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_ABV (Model Validation Track)

Competition results for the QF_ABV logic in the Model Validation Track.

Results were generated on 2024-07-08

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

Winners

winner_seqwinner_parwinner_satwinner_unsatwinner_24s
BitwuzlaBitwuzlaBitwuzla-Bitwuzla

Sequential Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla051915186.9450085708.88742651915191022000
cvc504924123735.934835124248.68532249244924028902759
SMTInterpol04335378875.60869323783.65416843394339087407920

Parallel Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla051915186.9450085708.88742651915191022000
cvc504924123735.934835124248.68532249244924028902759
SMTInterpol04339383766.963843328474.45490943394339087407920

SAT Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla051915186.9450085708.88742651915191022000
cvc504924123735.934835124248.68532249244924028902759
SMTInterpol04339383766.963843328474.45490943394339087407920

24 seconds Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla051671242.415141760.68658516751670182800
cvc5041505806.2511616221.1970384150415002106100
SMTInterpol0322521987.1487288676.93275832253225043194500