SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2023

Rules
Benchmarks
Specs
Model Validation Track
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results

QF_Equality+LinearArith (Single Query Track)

Competition results for the QF_Equality+LinearArith division in the Single Query Track.

Page generated on 2023-07-06 16:04:54 +0000

Benchmarks: 1922
Time Limit: 1200 seconds
Memory Limit: 60 GB

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
SMTInterpolSMTInterpolSMTInterpol OpenSMT Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTInterpol 0 1809 52677.755 40237.027180910587511130113 0
OpenSMT 0 1772 40949.939 40862.7981772993779658565 0
2022-z3-4.8.17n 0 1749 28616.218 28611.8351749976773977697 0
cvc5 0 1740 61435.265 61281.34117409767641820182 0
Yices2 0 1735 27167.152 27168.868173596077510285102 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTInterpol 0 181662150.87546637.515181610597571060106 0
OpenSMT 0 177240949.93940862.7981772993779658565 0
2022-z3-4.8.17n 0 174928616.21828611.8351749976773977697 0
cvc5 0 174061435.26561281.34117409767641820182 0
Yices2 0 173527167.15227168.868173596077510285102 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
SMTInterpol 0 105935517.41329611.16110591059014849106 0
OpenSMT 0 99321039.39420957.3999399302890165 0
2022-z3-4.8.17n 0 97613533.69913533.03597697605089697 0
cvc5 0 97634579.55934490.907976976097849182 0
Yices2 0 96014966.93714969.038960960061901102 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
OpenSMT 0 77919910.54519905.407779077926111765 0
Yices2 0 77512200.21512199.837750775301117102 0
2022-z3-4.8.17n 0 77315082.51915078.8773077336111397 0
cvc5 0 76426855.70626790.4347640764561102182 0
SMTInterpol 0 75726633.46217026.3547570757631102106 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2 0 1675423.367422.249167592774816285162 0
2022-z3-4.8.17n 0 1665820.771813.288166593373218176181 0
SMTInterpol 0 16568365.3683285.95116569537032660266 0
OpenSMT 0 16092306.3672268.718160990570422885228 0
cvc5 0 15611208.121196.47915618896723610361 0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.