SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

QF_LinearRealArith (Single Query Track)

Competition results for the QF_LinearRealArith division in the Single Query Track.

Page generated on 2022-08-10 11:17:45 +0000

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices2Yices2Yices2 cvc5 Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2021-Yices2n 0 750 117940.692 119643.15375042932175075 0
Yices2 0 750 119545.138 119459.51475042932175075 0
cvc5 0 745 144008.508 144362.48974542032580080 0
OpenSMT 0 738 137400.525 137303.55473842331587087 0
z3-4.8.17n 0 726 162780.461 162770.8372641631099099 0
veriT 0 705 189366.081 189335.7557053943111200120 0
MathSATn 0 672 229157.873 229176.4886723982741530153 0
smtinterpol 0 655 289759.718 277705.3736554012541700170 0
solsmt 0 237 711620.364 715932.752371311065880325 224

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2 0 750119550.888119457.25475042932175075 0
2021-Yices2n 0 750119604.94119639.73375042932175075 0
cvc5 0 745144284.078144359.30974542032580080 0
OpenSMT 0 738137406.665137300.61473842331587087 0
z3-4.8.17n 0 726162795.611162766.9172641631099099 0
veriT 0 705189379.141189331.4757053943111200120 0
MathSATn 0 672229177.313229170.6886723982741530153 0
smtinterpol 0 661290658.688277169.2336614012601640164 0
solsmt 0 237711686.784715918.012371311065880325 224

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2 0 42933391.52233348.46242942901837875 0
2021-Yices2n 0 42933491.0533477.55942942901837875 0
OpenSMT 0 42348248.24948228.19642342302437887 0
cvc5 0 42058777.35158888.07742042002737880 0
z3-4.8.17n 0 41660462.57160452.53741641603137899 0
smtinterpol 0 401100331.09894881.004401401046378164 0
MathSATn 0 39881556.74781551.959398398049378153 0
veriT 0 39487212.05387176.343394394053378120 0
solsmt 0 131390182.871392231.2651311310316378325 224

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 32536306.72736271.23232503251248880 0
Yices2 0 32136959.36636908.79232103211648875 0
2021-Yices2n 0 32136913.8936962.17332103211648875 0
OpenSMT 0 31539958.41539872.41831503152248887 0
veriT 0 31152967.08852955.132311031126488120 0
z3-4.8.17n 0 31053133.0453114.37331003102748899 0
MathSATn 0 27498420.56698418.729274027463488153 0
smtinterpol 0 260141127.59133088.228260026077488164 0
solsmt 0 106272303.913274486.7451060106231488325 224

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2 0 6216622.7556524.9646213722492040204 0
2021-Yices2n 0 6206586.7216560.6276203712492050205 0
OpenSMT 0 5917837.4747801.8395913462452340234 0
z3-4.8.17n 0 5209040.9989005.415202992213050305 0
veriT 0 5129106.3629053.1225122912213130313 0
MathSATn 0 4969228.3499212.9434963031933290329 0
cvc5 0 4959965.5819952.3694952932023300330 0
smtinterpol 0 40815067.21812135.2214082631454170417 0
solsmt 0 10517559.10317573.42310546597200488 224

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.