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

UF (Single Query Track)

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

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

Benchmarks: 2816
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 Vampire Par4 Vampire

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
CVC4 0 1141 4406118.838 4436448.822 1141 376 765 1675 1675 0
2018-CVC4n 0 1130 4244586.494 4260633.827 1130 371 759 1686 1686 0
Par4 0 1128 4575063.664 4226640.975 1128 363 765 1688 1420 268
Vampire 0 1120 4233800.251 4111634.178 1120 423 697 1696 1696 0
2018-Vampiren 0 1078 4381857.552 4224340.257 1078 427 651 1738 1738 0
veriT 0 665 5111250.699 5111636.509 665 0 665 2151 1855 158
Alt-Ergo 0 640 5157073.351 5117379.075 640 0 640 2176 2035 91
Z3n 0 455 3237148.569 3237695.064 455 41 414 2361 861 67
SMTInterpol 0 16 6695278.855 6679894.107 16 4 12 2800 2777 0
UltimateEliminator+MathSAT-5.5.4 0 0 10021.874 7369.04 0 0 0 2816 0 0
UltimateEliminator+SMTInterpol 0 0 16950.182 13252.991 0 0 0 2816 3 0
UltimateEliminator+Yices-2.6.1 0 0 17216.907 13888.844 0 0 0 2816 3 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Vampiren 0 1171 6257667.952 4099803.018 1171 434 737 1645 1645 0
Vampire 0 1157 5071140.731 4070434.872 1157 427 730 1659 1659 0
Par4 0 1142 4585000.064 4207563.01 1142 370 772 1674 1406 268
CVC4 0 1141 4430946.398 4436373.452 1141 376 765 1675 1675 0
2018-CVC4n 0 1130 4257953.294 4260560.957 1130 371 759 1686 1686 0
veriT 0 665 5112293.149 5111316.269 665 0 665 2151 1851 158
Alt-Ergo 0 664 5371320.651 5088014.59 664 0 664 2152 2011 91
Z3n 0 455 3237499.609 3237656.524 455 41 414 2361 861 67
SMTInterpol 0 16 6815660.745 6664398.447 16 4 12 2800 2744 0
UltimateEliminator+MathSAT-5.5.4 0 0 10021.874 7369.04 0 0 0 2816 0 0
UltimateEliminator+SMTInterpol 0 0 16950.182 13252.991 0 0 0 2816 3 0
UltimateEliminator+Yices-2.6.1 0 0 17216.907 13888.844 0 0 0 2816 3 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Vampiren 0 434 157419.768 75400.861 434 434 0 2382 1645 0
Vampire 0 427 180023.992 95517.912 427 427 0 2389 1659 0
CVC4 0 376 558407.519 563371.256 376 376 0 2440 1675 0
2018-CVC4n 0 371 393712.229 396192.331 371 371 0 2445 1686 0
Par4 0 370 710592.709 381552.636 370 370 0 2446 1406 268
Z3n 0 41 584817.156 584856.326 41 41 0 2775 861 67
SMTInterpol 0 4 1093231.24 1072619.475 4 4 0 2812 2744 0
UltimateEliminator+MathSAT-5.5.4 0 0 1608.55 1077.024 0 0 0 2816 0 0
UltimateEliminator+SMTInterpol 0 0 8793.984 8182.676 0 0 0 2816 3 0
UltimateEliminator+Yices-2.6.1 0 0 8792.47 8277.231 0 0 0 2816 3 0
Alt-Ergo 0 0 1037976.002 1006996.028 0 0 0 2816 2011 91
veriT 0 0 1039068.218 1039073.236 0 0 0 2816 1851 158

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 772 212007.356 163610.373 772 0 772 2044 1406 268
CVC4 0 765 210138.879 210602.197 765 0 765 2051 1675 0
2018-CVC4n 0 759 201841.065 201968.625 759 0 759 2057 1686 0
2018-Vampiren 0 737 918615.444 363787.298 737 0 737 2079 1645 0
Vampire 0 730 595102.038 313020.29 730 0 730 2086 1659 0
veriT 0 665 426531.004 426519.5 665 0 665 2151 1851 158
Alt-Ergo 0 664 576044.213 441301.567 664 0 664 2152 2011 91
Z3n 0 414 611765.708 611779.48 414 0 414 2402 861 67
SMTInterpol 0 12 2003103.087 1953209.807 12 0 12 2804 2744 0
UltimateEliminator+SMTInterpol 0 0 2881.321 1784.656 0 0 0 2816 3 0
UltimateEliminator+Yices-2.6.1 0 0 2976.003 1975.203 0 0 0 2816 3 0
UltimateEliminator+MathSAT-5.5.4 0 0 2987.91 2670.385 0 0 0 2816 0 0

24s Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Vampiren 0 847 54045.681 49072.359 847 392 455 1969 1969 0
Vampire 0 774 58178.322 51417.485 774 263 511 2042 2042 0
Par4 0 718 52111.04 51030.731 718 47 671 2098 1830 268
CVC4 0 606 53596.519 53582.489 606 7 599 2210 2210 0
2018-CVC4n 0 606 53619.463 53616.958 606 7 599 2210 2210 0
veriT 0 603 53868.688 53853.304 603 0 603 2213 2033 158
Alt-Ergo 0 563 57194.142 54238.07 563 0 563 2253 2122 91
Z3n 0 412 58138.267 58114.758 412 38 374 2404 2332 67
SMTInterpol 0 10 67264.719 67221.542 10 4 6 2806 2799 0
UltimateEliminator+SMTInterpol 0 0 9822.182 6124.991 0 0 0 2816 3 0
UltimateEliminator+MathSAT-5.5.4 0 0 10041.565 6703.206 0 0 0 2816 1 0
UltimateEliminator+Yices-2.6.1 0 0 10088.907 6760.844 0 0 0 2816 3 0

n Non-competing.