SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_UFIDL (Unsat Core Track)

Competition results for the QF_UFIDL logic in the Unsat Core Track.

Results were generated on 2024-07-08

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

Winners

winner_seqwinner_parwinner_satwinner_unsatwinner_24s
SMTInterpolcvc5-cvc5Yices2

Sequential Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0710385070.4233422383.99315724024890890
cvc5015965735.148182737.14550816016970970
OpenSMT259404527127.11106427140.99745267067460440
Yices2371632621166.73926921178.98755669069440410

Parallel Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501.161123e+06117224.780275117304.50967216016970970
SMTInterpol01.120061e+06156899.359976113346.48839124024890890
OpenSMT21.150563e+0679967.65845179999.22775267067460440
Yices231.14553e+0670400.54183370429.83969069440410

UNSAT Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501.161123e+06117224.780275117304.50967216016970970
SMTInterpol01.120061e+06156899.359976113346.48839124024890890
OpenSMT21.150563e+0679967.65845179999.22775267067460440
Yices231.14553e+0670400.54183370429.83969069440410

24 seconds Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices204033266.61239568.3264751701709600
cvc50191.8163833.11789213013010000
SMTInterpol0195.4216135.39482813013010000
OpenSMT0171.7330913.04707213013010000