SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

AUFLIA (Single Query Track)

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

Page generated on 2019-07-23 17:56:09 +0000

Benchmarks: 1638
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4VampireCVC4 Vampire Vampire

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2018-CVC4n 0 1383 581043.979 587924.14913831371246255231 0
CVC4-SymBreakn 0 1381 596278.608 607017.88213811371244257231 0
CVC4 0 1381 604438.313 617291.03213811371244257231 0
Vampire 0 1375 640132.477 624671.3241375991276263258 0
Z3n 0 1300 674937.988 677221.99313001551145338201 24
Alt-Ergo 0 1217 758501.014 736654.555121701217421265 38
veriT 0 1169 766139.798 766183.373116901169469287 15
SMTInterpol 0 893 1652269.898 1630275.95189393800745665 0
UltimateEliminator+SMTInterpol 0 14 166473.705 162509.3381459162465 0
UltimateEliminator+MathSAT-5.5.4 0 13 166768.621 162412.5821349162565 0
UltimateEliminator+Yices-2.6.1 0 7 166646.497 162887.45734163165 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2018-CVC4n 0 1383587410.849587913.96913831371246255231 0
Vampire 0 1382687185.437616673.9811382991283256251 0
CVC4-SymBreakn 0 1381606248.838607006.61213811371244257231 0
CVC4 0 1381616468.103617280.48213811371244257231 0
Z3n 0 1300675012.238677212.77313001551145338201 24
Alt-Ergo 0 1229794253.464720273.105122901229409253 38
veriT 0 1169766211.978766171.143116901169469287 15
SMTInterpol 0 8951732196.1981620506.26189593802743638 0
UltimateEliminator+SMTInterpol 0 14196335.485157729.6551459162457 0
UltimateEliminator+MathSAT-5.5.4 0 13177996.481158154.921349162560 0
UltimateEliminator+Yices-2.6.1 0 7173572.937158938.424734163161 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 15523734.07923735.215515501483201 24
2018-CVC4n 0 13731376.65431565.32313713701501231 0
CVC4-SymBreakn 0 13737956.0938259.26113713701501231 0
CVC4 0 13746160.61446551.50913713701501231 0
Vampire 0 99163680.17156126.925999901539251 0
SMTInterpol 0 9360868.76456093.476939301545638 0
UltimateEliminator+SMTInterpol 0 57031.3414746.39550163357 0
UltimateEliminator+MathSAT-5.5.4 0 47614.8654559.691440163460 0
UltimateEliminator+Yices-2.6.1 0 36989.3794992.815330163561 0
veriT 0 087096.15387090.0780001638287 15
Alt-Ergo 0 0142781.919142643.5280001638253 38

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 128386193.49646991.541128301283355251 0
2018-CVC4n 0 1246138434.195138748.646124601246392231 0
CVC4-SymBreakn 0 1244150692.748151147.351124401244394231 0
CVC4 0 1244152707.489153128.973124401244394231 0
Alt-Ergo 0 1229248456.484182814.691122901229409253 38
veriT 0 1169310293.021310255.595116901169469287 15
Z3n 0 1145290572.637292456.469114501145493201 24
SMTInterpol 0 8021267718.6961181493.6568020802836638 0
UltimateEliminator+SMTInterpol 0 9108577.9188421.65909162957 0
UltimateEliminator+MathSAT-5.5.4 0 997069.41288808.782909162960 0
UltimateEliminator+Yices-2.6.1 0 497292.15188767.632404163461 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Vampire 0 13519527.3317707.2881351991252287287 0
Z3n 0 12719222.719222.74612711551116367342 24
2018-CVC4n 0 12399636.4019635.9361239871152399391 0
CVC4-SymBreakn 0 12369695.3289694.8481236881148402394 0
CVC4 0 12359705.259704.7861235881147403395 0
Alt-Ergo 0 116510881.0249272.146116501165473322 38
veriT 0 110810066.74510049.121110801108530365 15
SMTInterpol 0 82320632.69719458.57282393730815754 0
UltimateEliminator+SMTInterpol 0 147675.8155595.3681459162483 0
UltimateEliminator+MathSAT-5.5.4 0 137663.9165823.0541349162582 0
UltimateEliminator+Yices-2.6.1 0 77559.955793.901734163181 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.