SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

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

Previous Competitions

SMT-LIB

UF (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4VampireVampire Par4 Vampire

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 1141 4406118.838 4436448.822114137676516751675 0
2018-CVC4n 0 1130 4244586.494 4260633.827113037175916861686 0
Par4 0 1128 4575063.664 4226640.975112836376516881420 268
Vampire 0 1120 4233800.251 4111634.178112042369716961696 0
2018-Vampiren 0 1078 4381857.552 4224340.257107842765117381738 0
veriT 0 665 5111250.699 5111636.509665066521511855 158
Alt-Ergo 0 640 5157073.351 5117379.075640064021762035 91
Z3n 0 455 3237148.569 3237695.064455414142361861 67
SMTInterpol 0 16 6695278.855 6679894.1071641228002777 0
UltimateEliminator+MathSAT-5.5.4 0 0 10021.874 7369.0400028160 0
UltimateEliminator+SMTInterpol 0 0 16950.182 13252.99100028163 0
UltimateEliminator+Yices-2.6.1 0 0 17216.907 13888.84400028163 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Vampiren 0 1171 6257667.952 4099803.018117143473716451645 0
Vampire 0 1157 5071140.731 4070434.872115742773016591659 0
Par4 0 1142 4585000.064 4207563.01114237077216741406 268
CVC4 0 1141 4430946.398 4436373.452114137676516751675 0
2018-CVC4n 0 1130 4257953.294 4260560.957113037175916861686 0
veriT 0 665 5112293.149 5111316.269665066521511851 158
Alt-Ergo 0 664 5371320.651 5088014.59664066421522011 91
Z3n 0 455 3237499.609 3237656.524455414142361861 67
SMTInterpol 0 16 6815660.745 6664398.4471641228002744 0
UltimateEliminator+MathSAT-5.5.4 0 0 10021.874 7369.0400028160 0
UltimateEliminator+SMTInterpol 0 0 16950.182 13252.99100028163 0
UltimateEliminator+Yices-2.6.1 0 0 17216.907 13888.84400028163 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Vampiren 0 434 157419.768 75400.861434434023821645 0
Vampire 0 427 180023.992 95517.912427427023891659 0
CVC4 0 376 558407.519 563371.256376376024401675 0
2018-CVC4n 0 371 393712.229 396192.331371371024451686 0
Par4 0 370 710592.709 381552.636370370024461406 268
Z3n 0 41 584817.156 584856.326414102775861 67
SMTInterpol 0 4 1093231.24 1072619.47544028122744 0
UltimateEliminator+MathSAT-5.5.4 0 0 1608.55 1077.02400028160 0
UltimateEliminator+SMTInterpol 0 0 8793.984 8182.67600028163 0
UltimateEliminator+Yices-2.6.1 0 0 8792.47 8277.23100028163 0
Alt-Ergo 0 0 1037976.002 1006996.02800028162011 91
veriT 0 0 1039068.218 1039073.23600028161851 158

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 772 212007.356 163610.373772077220441406 268
CVC4 0 765 210138.879 210602.197765076520511675 0
2018-CVC4n 0 759 201841.065 201968.625759075920571686 0
2018-Vampiren 0 737 918615.444 363787.298737073720791645 0
Vampire 0 730 595102.038 313020.29730073020861659 0
veriT 0 665 426531.004 426519.5665066521511851 158
Alt-Ergo 0 664 576044.213 441301.567664066421522011 91
Z3n 0 414 611765.708 611779.4841404142402861 67
SMTInterpol 0 12 2003103.087 1953209.8071201228042744 0
UltimateEliminator+SMTInterpol 0 0 2881.321 1784.65600028163 0
UltimateEliminator+Yices-2.6.1 0 0 2976.003 1975.20300028163 0
UltimateEliminator+MathSAT-5.5.4 0 0 2987.91 2670.38500028160 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Vampiren 0 847 54045.681 49072.35984739245519691969 0
Vampire 0 774 58178.322 51417.48577426351120422042 0
Par4 0 718 52111.04 51030.7317184767120981830 268
CVC4 0 606 53596.519 53582.489606759922102210 0
2018-CVC4n 0 606 53619.463 53616.958606759922102210 0
veriT 0 603 53868.688 53853.304603060322132033 158
Alt-Ergo 0 563 57194.142 54238.07563056322532122 91
Z3n 0 412 58138.267 58114.7584123837424042332 67
SMTInterpol 0 10 67264.719 67221.542104628062799 0
UltimateEliminator+SMTInterpol 0 0 9822.182 6124.99100028163 0
UltimateEliminator+MathSAT-5.5.4 0 0 10041.565 6703.20600028161 0
UltimateEliminator+Yices-2.6.1 0 0 10088.907 6760.84400028163 0

n Non-competing.