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

UFLIA (Single Query Track)

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

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

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Par4 Par4 Par4 Par4 Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 1674 2872857.6 2836528.739 1674 8 1666 1174 1063 111
CVC4 0 1644 2876609.874 2944307.644 1644 5 1639 1204 1189 0
2018-CVC4n 0 1637 2908980.824 2926313.181 1637 5 1632 1211 1196 0
veriT 0 1545 3112585.538 3112960.053 1545 0 1545 1303 1164 69
Vampire 0 1423 3572991.47 3458795.006 1423 0 1423 1425 1425 0
Z3n 0 1405 2058425.405 2064145.676 1405 6 1399 1443 595 20
Alt-Ergo 0 1356 3633265.225 3559959.68 1356 0 1356 1492 1395 77
SMTInterpol 0 47 6638832.092 6623072.118 47 5 42 2801 2750 0
UltimateEliminator+Yices-2.6.1 0 0 19808.146 23625.717 0 0 0 2848 7 0
UltimateEliminator+SMTInterpol 0 0 21898.476 18623.415 0 0 0 2848 5 0
UltimateEliminator+MathSAT-5.5.4 0 0 22286.482 19950.492 0 0 0 2848 5 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 1681 2890786.76 2831381.873 1681 8 1673 1167 1056 111
CVC4 0 1644 2942508.164 2944250.794 1644 5 1639 1204 1189 0
2018-CVC4n 0 1637 2925682.654 2926262.851 1637 5 1632 1211 1196 0
veriT 0 1545 3112958.678 3112913.573 1545 0 1545 1303 1164 69
Vampire 0 1479 4198978.49 3391947.714 1479 0 1479 1369 1369 0
Z3n 0 1405 2058727.995 2064116.896 1405 6 1399 1443 595 20
Alt-Ergo 0 1401 3831462.325 3500680.893 1401 0 1401 1447 1349 77
SMTInterpol 0 47 6689951.452 6607955.483 47 5 42 2801 2730 0
UltimateEliminator+SMTInterpol 0 0 21898.476 18623.415 0 0 0 2848 5 0
UltimateEliminator+MathSAT-5.5.4 0 0 22286.482 19950.492 0 0 0 2848 5 0
UltimateEliminator+Yices-2.6.1 0 0 33196.806 23565.467 0 0 0 2848 6 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 8 11739.589 8727.378 8 8 0 2840 1056 111
Z3n 0 6 10057.916 10058.169 6 6 0 2842 595 20
SMTInterpol 0 5 10783.749 9273.208 5 5 0 2843 2730 0
2018-CVC4n 0 5 12330.535 12386.645 5 5 0 2843 1196 0
CVC4 0 5 14733.746 14910.887 5 5 0 2843 1189 0
UltimateEliminator+SMTInterpol 0 0 37.028 23.953 0 0 0 2848 5 0
UltimateEliminator+Yices-2.6.1 0 0 36.489 25.129 0 0 0 2848 6 0
UltimateEliminator+MathSAT-5.5.4 0 0 37.127 26.845 0 0 0 2848 5 0
Alt-Ergo 0 0 21601.167 14297.389 0 0 0 2848 1349 77
veriT 0 0 16740.238 16740.594 0 0 0 2848 1164 69
Vampire 0 0 26400.0 26400.0 0 0 0 2848 1369 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 1673 193447.17 137054.495 1673 0 1673 1175 1056 111
CVC4 0 1639 260187.921 261677.735 1639 0 1639 1209 1189 0
2018-CVC4n 0 1632 251097.445 251578.196 1632 0 1632 1216 1196 0
veriT 0 1545 450641.826 450588.982 1545 0 1545 1303 1164 69
Vampire 0 1479 1040560.28 680849.824 1479 0 1479 1369 1369 0
Alt-Ergo 0 1401 1068457.35 833883.821 1401 0 1401 1447 1349 77
Z3n 0 1399 441021.895 441972.65 1399 0 1399 1449 595 20
SMTInterpol 0 42 4008936.378 3978280.922 42 0 42 2806 2730 0
UltimateEliminator+SMTInterpol 0 0 17990.102 16145.497 0 0 0 2848 5 0
UltimateEliminator+MathSAT-5.5.4 0 0 18236.732 17182.761 0 0 0 2848 5 0
UltimateEliminator+Yices-2.6.1 0 0 26770.475 18451.849 0 0 0 2848 6 0

24s Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 1583 32669.431 31293.423 1583 5 1578 1265 1154 111
2018-CVC4n 0 1450 35308.26 35303.124 1450 1 1449 1398 1397 0
CVC4 0 1448 35318.65 35311.629 1448 1 1447 1400 1399 0
veriT 0 1445 35350.032 35341.118 1445 0 1445 1403 1315 69
Z3n 0 1375 35888.239 35891.025 1375 6 1369 1473 1444 20
Alt-Ergo 0 1222 49515.905 41610.236 1222 0 1222 1626 1536 77
Vampire 0 1144 55770.176 44806.626 1144 0 1144 1704 1704 0
SMTInterpol 0 43 66883.566 66792.645 43 5 38 2805 2780 0
UltimateEliminator+SMTInterpol 0 0 10038.748 6376.413 0 0 0 2848 6 0
UltimateEliminator+Yices-2.6.1 0 0 10359.006 6992.747 0 0 0 2848 7 0
UltimateEliminator+MathSAT-5.5.4 0 0 10488.142 7136.666 0 0 0 2848 9 0

n Non-competing.