SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

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 UNSATUnsolvedTimeout 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 Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 1383 587410.849 587913.96913831371246255231 0
Vampire 0 1382 687185.437 616673.9811382991283256251 0
CVC4-SymBreakn 0 1381 606248.838 607006.61213811371244257231 0
CVC4 0 1381 616468.103 617280.48213811371244257231 0
Z3n 0 1300 675012.238 677212.77313001551145338201 24
Alt-Ergo 0 1229 794253.464 720273.105122901229409253 38
veriT 0 1169 766211.978 766171.143116901169469287 15
SMTInterpol 0 895 1732196.198 1620506.26189593802743638 0
UltimateEliminator+SMTInterpol 0 14 196335.485 157729.6551459162457 0
UltimateEliminator+MathSAT-5.5.4 0 13 177996.481 158154.921349162560 0
UltimateEliminator+Yices-2.6.1 0 7 173572.937 158938.424734163161 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 155 23734.079 23735.215515501483201 24
2018-CVC4n 0 137 31376.654 31565.32313713701501231 0
CVC4-SymBreakn 0 137 37956.09 38259.26113713701501231 0
CVC4 0 137 46160.614 46551.50913713701501231 0
Vampire 0 99 163680.17 156126.925999901539251 0
SMTInterpol 0 93 60868.764 56093.476939301545638 0
UltimateEliminator+SMTInterpol 0 5 7031.341 4746.39550163357 0
UltimateEliminator+MathSAT-5.5.4 0 4 7614.865 4559.691440163460 0
UltimateEliminator+Yices-2.6.1 0 3 6989.379 4992.815330163561 0
veriT 0 0 87096.153 87090.0780001638287 15
Alt-Ergo 0 0 142781.919 142643.5280001638253 38

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1283 86193.496 46991.541128301283355251 0
2018-CVC4n 0 1246 138434.195 138748.646124601246392231 0
CVC4-SymBreakn 0 1244 150692.748 151147.351124401244394231 0
CVC4 0 1244 152707.489 153128.973124401244394231 0
Alt-Ergo 0 1229 248456.484 182814.691122901229409253 38
veriT 0 1169 310293.021 310255.595116901169469287 15
Z3n 0 1145 290572.637 292456.469114501145493201 24
SMTInterpol 0 802 1267718.696 1181493.6568020802836638 0
UltimateEliminator+SMTInterpol 0 9 108577.91 88421.65909162957 0
UltimateEliminator+MathSAT-5.5.4 0 9 97069.412 88808.782909162960 0
UltimateEliminator+Yices-2.6.1 0 4 97292.151 88767.632404163461 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1351 9527.331 7707.2881351991252287287 0
Z3n 0 1271 9222.71 9222.74612711551116367342 24
2018-CVC4n 0 1239 9636.401 9635.9361239871152399391 0
CVC4-SymBreakn 0 1236 9695.328 9694.8481236881148402394 0
CVC4 0 1235 9705.25 9704.7861235881147403395 0
Alt-Ergo 0 1165 10881.024 9272.146116501165473322 38
veriT 0 1108 10066.745 10049.121110801108530365 15
SMTInterpol 0 823 20632.697 19458.57282393730815754 0
UltimateEliminator+SMTInterpol 0 14 7675.815 5595.3681459162483 0
UltimateEliminator+MathSAT-5.5.4 0 13 7663.916 5823.0541349162582 0
UltimateEliminator+Yices-2.6.1 0 7 7559.95 5793.901734163181 0

n Non-competing.