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

UFLIA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Par4Par4Par4 Par4 Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1674 2872857.6 2836528.73916748166611741063 111
CVC4 0 1644 2876609.874 2944307.64416445163912041189 0
2018-CVC4n 0 1637 2908980.824 2926313.18116375163212111196 0
veriT 0 1545 3112585.538 3112960.05315450154513031164 69
Vampire 0 1423 3572991.47 3458795.00614230142314251425 0
Z3n 0 1405 2058425.405 2064145.6761405613991443595 20
Alt-Ergo 0 1356 3633265.225 3559959.6813560135614921395 77
SMTInterpol 0 47 6638832.092 6623072.1184754228012750 0
UltimateEliminator+Yices-2.6.1 0 0 19808.146 23625.71700028487 0
UltimateEliminator+SMTInterpol 0 0 21898.476 18623.41500028485 0
UltimateEliminator+MathSAT-5.5.4 0 0 22286.482 19950.49200028485 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1681 2890786.76 2831381.87316818167311671056 111
CVC4 0 1644 2942508.164 2944250.79416445163912041189 0
2018-CVC4n 0 1637 2925682.654 2926262.85116375163212111196 0
veriT 0 1545 3112958.678 3112913.57315450154513031164 69
Vampire 0 1479 4198978.49 3391947.71414790147913691369 0
Z3n 0 1405 2058727.995 2064116.8961405613991443595 20
Alt-Ergo 0 1401 3831462.325 3500680.89314010140114471349 77
SMTInterpol 0 47 6689951.452 6607955.4834754228012730 0
UltimateEliminator+SMTInterpol 0 0 21898.476 18623.41500028485 0
UltimateEliminator+MathSAT-5.5.4 0 0 22286.482 19950.49200028485 0
UltimateEliminator+Yices-2.6.1 0 0 33196.806 23565.46700028486 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 8 11739.589 8727.37888028401056 111
Z3n 0 6 10057.916 10058.1696602842595 20
SMTInterpol 0 5 10783.749 9273.20855028432730 0
2018-CVC4n 0 5 12330.535 12386.64555028431196 0
CVC4 0 5 14733.746 14910.88755028431189 0
UltimateEliminator+SMTInterpol 0 0 37.028 23.95300028485 0
UltimateEliminator+Yices-2.6.1 0 0 36.489 25.12900028486 0
UltimateEliminator+MathSAT-5.5.4 0 0 37.127 26.84500028485 0
Alt-Ergo 0 0 21601.167 14297.38900028481349 77
veriT 0 0 16740.238 16740.59400028481164 69
Vampire 0 0 26400.0 26400.000028481369 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1673 193447.17 137054.49516730167311751056 111
CVC4 0 1639 260187.921 261677.73516390163912091189 0
2018-CVC4n 0 1632 251097.445 251578.19616320163212161196 0
veriT 0 1545 450641.826 450588.98215450154513031164 69
Vampire 0 1479 1040560.28 680849.82414790147913691369 0
Alt-Ergo 0 1401 1068457.35 833883.82114010140114471349 77
Z3n 0 1399 441021.895 441972.651399013991449595 20
SMTInterpol 0 42 4008936.378 3978280.9224204228062730 0
UltimateEliminator+SMTInterpol 0 0 17990.102 16145.49700028485 0
UltimateEliminator+MathSAT-5.5.4 0 0 18236.732 17182.76100028485 0
UltimateEliminator+Yices-2.6.1 0 0 26770.475 18451.84900028486 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1583 32669.431 31293.42315835157812651154 111
2018-CVC4n 0 1450 35308.26 35303.12414501144913981397 0
CVC4 0 1448 35318.65 35311.62914481144714001399 0
veriT 0 1445 35350.032 35341.11814450144514031315 69
Z3n 0 1375 35888.239 35891.02513756136914731444 20
Alt-Ergo 0 1222 49515.905 41610.23612220122216261536 77
Vampire 0 1144 55770.176 44806.62611440114417041704 0
SMTInterpol 0 43 66883.566 66792.6454353828052780 0
UltimateEliminator+SMTInterpol 0 0 10038.748 6376.41300028486 0
UltimateEliminator+Yices-2.6.1 0 0 10359.006 6992.74700028487 0
UltimateEliminator+MathSAT-5.5.4 0 0 10488.142 7136.66600028489 0

n Non-competing.