SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous

SMT-LIB

AUFLIA (Single Query Track)

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

Page generated on 2019-07-07 12:14:30 +0000

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
CVC4 Vampire CVC4 Vampire Vampire

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-CVC4n 0 1383 581043.979 587924.149 1383 137 1246 255 231 0
CVC4-SymBreakn 0 1381 596278.608 607017.882 1381 137 1244 257 231 0
CVC4 0 1381 604438.313 617291.032 1381 137 1244 257 231 0
Vampire 0 1375 640132.477 624671.324 1375 99 1276 263 258 0
Z3n 0 1300 674937.988 677221.993 1300 155 1145 338 201 24
Alt-Ergo 0 1217 758501.014 736654.555 1217 0 1217 421 265 38
veriT 0 1169 766139.798 766183.373 1169 0 1169 469 287 15
SMTInterpol 0 893 1652269.898 1630275.951 893 93 800 745 665 0
UltimateEliminator+SMTInterpol 0 14 166473.705 162509.338 14 5 9 1624 65 0
UltimateEliminator+MathSAT-5.5.4 0 13 166768.621 162412.582 13 4 9 1625 65 0
UltimateEliminator+Yices-2.6.1 0 7 166646.497 162887.45 7 3 4 1631 65 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-CVC4n 0 1383 587410.849 587913.969 1383 137 1246 255 231 0
Vampire 0 1382 687185.437 616673.981 1382 99 1283 256 251 0
CVC4-SymBreakn 0 1381 606248.838 607006.612 1381 137 1244 257 231 0
CVC4 0 1381 616468.103 617280.482 1381 137 1244 257 231 0
Z3n 0 1300 675012.238 677212.773 1300 155 1145 338 201 24
Alt-Ergo 0 1229 794253.464 720273.105 1229 0 1229 409 253 38
veriT 0 1169 766211.978 766171.143 1169 0 1169 469 287 15
SMTInterpol 0 895 1732196.198 1620506.261 895 93 802 743 638 0
UltimateEliminator+SMTInterpol 0 14 196335.485 157729.655 14 5 9 1624 57 0
UltimateEliminator+MathSAT-5.5.4 0 13 177996.481 158154.92 13 4 9 1625 60 0
UltimateEliminator+Yices-2.6.1 0 7 173572.937 158938.424 7 3 4 1631 61 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Z3n 0 155 23734.079 23735.2 155 155 0 1483 201 24
2018-CVC4n 0 137 31376.654 31565.323 137 137 0 1501 231 0
CVC4-SymBreakn 0 137 37956.09 38259.261 137 137 0 1501 231 0
CVC4 0 137 46160.614 46551.509 137 137 0 1501 231 0
Vampire 0 99 163680.17 156126.925 99 99 0 1539 251 0
SMTInterpol 0 93 60868.764 56093.476 93 93 0 1545 638 0
UltimateEliminator+SMTInterpol 0 5 7031.341 4746.39 5 5 0 1633 57 0
UltimateEliminator+MathSAT-5.5.4 0 4 7614.865 4559.691 4 4 0 1634 60 0
UltimateEliminator+Yices-2.6.1 0 3 6989.379 4992.815 3 3 0 1635 61 0
veriT 0 0 87096.153 87090.078 0 0 0 1638 287 15
Alt-Ergo 0 0 142781.919 142643.528 0 0 0 1638 253 38

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Vampire 0 1283 86193.496 46991.541 1283 0 1283 355 251 0
2018-CVC4n 0 1246 138434.195 138748.646 1246 0 1246 392 231 0
CVC4-SymBreakn 0 1244 150692.748 151147.351 1244 0 1244 394 231 0
CVC4 0 1244 152707.489 153128.973 1244 0 1244 394 231 0
Alt-Ergo 0 1229 248456.484 182814.691 1229 0 1229 409 253 38
veriT 0 1169 310293.021 310255.595 1169 0 1169 469 287 15
Z3n 0 1145 290572.637 292456.469 1145 0 1145 493 201 24
SMTInterpol 0 802 1267718.696 1181493.656 802 0 802 836 638 0
UltimateEliminator+SMTInterpol 0 9 108577.91 88421.65 9 0 9 1629 57 0
UltimateEliminator+MathSAT-5.5.4 0 9 97069.412 88808.782 9 0 9 1629 60 0
UltimateEliminator+Yices-2.6.1 0 4 97292.151 88767.632 4 0 4 1634 61 0

24s Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Vampire 0 1351 9527.331 7707.288 1351 99 1252 287 287 0
Z3n 0 1271 9222.71 9222.746 1271 155 1116 367 342 24
2018-CVC4n 0 1239 9636.401 9635.936 1239 87 1152 399 391 0
CVC4-SymBreakn 0 1236 9695.328 9694.848 1236 88 1148 402 394 0
CVC4 0 1235 9705.25 9704.786 1235 88 1147 403 395 0
Alt-Ergo 0 1165 10881.024 9272.146 1165 0 1165 473 322 38
veriT 0 1108 10066.745 10049.121 1108 0 1108 530 365 15
SMTInterpol 0 823 20632.697 19458.572 823 93 730 815 754 0
UltimateEliminator+SMTInterpol 0 14 7675.815 5595.368 14 5 9 1624 83 0
UltimateEliminator+MathSAT-5.5.4 0 13 7663.916 5823.054 13 4 9 1625 82 0
UltimateEliminator+Yices-2.6.1 0 7 7559.95 5793.901 7 3 4 1631 81 0

n Non-competing.