SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

QF_LinearRealArith (Single Query Track)

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

Page generated on 2021-07-18 17:29:06 +0000

Benchmarks: 829
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
Yices2 0 753 124300.762 124277.03375342632776076 0
cvc5 0 751 138777.821 140113.78675141933278078 0
OpenSMT 0 734 151930.267 151783.59173441232295095 0
z3n 0 733 160613.313 160795.58673340832596096 0
veriT 0 723 174316.165 174310.0837234033201060106 0
SMTInterpol 0 681 271570.147 261651.1586814032781480148 0
MathSAT5n 0 673 230948.127 231099.0686733922811560156 0
2020-OpenSMTn 0 543 69798.963 69785.7885433142293924739 0
2019-Par4n 0 536 105313.498 67940.7475363192174624746 0
2019-Yices 2.6.2n 0 213 43046.864 43118.9942131051083458234 0
mc2 0 201 49389.939 49245.453201123783812477 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2 0 753124307.302124275.29375342632776076 0
cvc5 0 751140063.078140109.82675141933278078 0
OpenSMT 0 734151937.707151780.84173441232295095 0
z3n 0 733160821.683160791.65673340832596096 0
veriT 0 723174326.675174306.2037234033201060106 0
SMTInterpol 0 684271764.007261548.0086844042801450145 0
MathSAT5n 0 673231110.727231092.4986733922811560156 0
2019-Par4n 0 565136198.30849817.5945653372281724717 0
2020-OpenSMTn 0 54369805.67369784.1585433142293924739 0
2019-Yices 2.6.2n 0 21343120.35443118.1142131051083458234 0
mc2 0 20149390.40949245.183201123783812477 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2 0 42636786.77136751.90742642602238176 0
cvc5 0 41960731.12560777.21741941902938178 0
OpenSMT 0 41265000.72464956.50841241203638195 0
z3n 0 40869826.90969818.71940840804038196 0
SMTInterpol 0 404103654.44297788.263404404044381145 0
veriT 0 40380766.86380765.879403403045381106 0
MathSAT5n 0 39289802.29389780.813392392056381156 0
2019-Par4n 0 33776444.16224807.4343373370648617 0
2020-OpenSMTn 0 31450396.72550399.48731431402948639 0
mc2 0 12321834.74621746.45412312302204867 0
2019-Yices 2.6.2n 0 105767.8766.9531051050072434 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 33236131.95236132.60933203321348478 0
Yices2 0 32744320.53144323.38632703271848476 0
z3n 0 32547794.77447772.93732503252048496 0
OpenSMT 0 32243736.98443624.33332203222348495 0
veriT 0 32050359.81250340.324320032025484106 0
MathSAT5n 0 28198108.43498111.685281028164484156 0
SMTInterpol 0 280124909.565120559.746280028065484145 0
2020-OpenSMTn 0 22915808.94815784.672290229759339 0
2019-Par4n 0 22856154.14721410.1612280228859317 0
2019-Yices 2.6.2n 0 1082752.5542751.1621080108172034 0
mc2 0 7827382.04327325.08780781585937 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2 0 6186604.7716569.3496183762422110211 0
OpenSMT 0 5528764.9658697.8095523122402770277 0
veriT 0 5228963.1898936.9275222922303070307 0
z3n 0 5209023.2959013.3115202992213090309 0
cvc5 0 5039637.4399593.2795032952083260326 0
MathSAT5n 0 4979265.3529265.8464972932043320332 0
SMTInterpol 0 41114610.03612026.8754112561554180418 0
2020-OpenSMTn 0 4035989.615964.999403227176179247179 0
2019-Par4n 0 40210611.9225947.62402246156180247180 0
2019-Yices 2.6.2n 0 1951624.8931622.445195100955258252 0
mc2 0 1758963.5438962.92217510273407247273 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.