SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_UF (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

Benchmarks: 2800
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices2Yices2Yices2 Yices2 Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 2800 374.008 383.56428001130167000 0
Yices2-fixedn 0 2800 374.281 388.79328001130167000 0
2019-Yices 2.6.2n 0 2800 376.185 386.99428001130167000 0
2019-Par4n 0 2800 496.93 376.24528001130167000 0
veriT 0 2800 791.191 790.4728001130167000 0
z3n 0 2799 5949.848 5913.73527991130166911 0
OpenSMT 0 2798 9544.475 9488.88727981130166822 0
CVC4 0 2797 11686.981 11675.98427971130166733 0
SMTInterpol 0 2765 59323.135 53413.4452765113016353535 0
SMTInterpol-fixedn 0 2765 59331.033 53428.1122765113016353535 0
MathSAT5n 0 2745 45284.991 45280.0542745111316325534 0
Alt-Ergo 0 1164 1222753.458 957418.6641164011641636654 19

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2800 496.93 376.24528001130167000 0
Yices2 0 2800 374.008 383.56428001130167000 0
2019-Yices 2.6.2n 0 2800 376.185 386.99428001130167000 0
Yices2-fixedn 0 2800 374.281 388.79328001130167000 0
veriT 0 2800 791.191 790.4728001130167000 0
z3n 0 2799 5949.848 5913.73527991130166911 0
OpenSMT 0 2798 9544.665 9488.85727981130166822 0
CVC4 0 2797 11687.231 11675.93427971130166733 0
SMTInterpol 0 2765 59323.135 53413.4452765113016353535 0
SMTInterpol-fixedn 0 2765 59331.033 53428.1122765113016353535 0
MathSAT5n 0 2745 45289.771 45278.4942745111316325534 0
Alt-Ergo 0 1415 1594315.558 791512.7571415014151385352 19

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 1130 47.447 51.94111301130016700 0
2019-Par4n 0 1130 21.092 53.34311301130016700 0
2019-Yices 2.6.2n 0 1130 48.682 53.86711301130016700 0
Yices2-fixedn 0 1130 47.507 54.45211301130016700 0
veriT 0 1130 107.604 106.69411301130016700 0
z3n 0 1130 199.771 199.911301130016701 0
OpenSMT 0 1130 429.615 428.86911301130016702 0
CVC4 0 1130 1004.907 1003.09811301130016703 0
SMTInterpol 0 1130 2659.411 1084.878113011300167035 0
SMTInterpol-fixedn 0 1130 2632.145 1085.452113011300167035 0
MathSAT5n 0 1113 131.999 132.117111311130168734 0
Alt-Ergo 0 0 426891.637 270549.5070002800352 19

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1670 475.838 322.90216700167011300 0
Yices2 0 1670 326.562 331.62416700167011300 0
2019-Yices 2.6.2n 0 1670 327.503 333.12716700167011300 0
Yices2-fixedn 0 1670 326.773 334.34116700167011300 0
veriT 0 1670 683.587 683.77616700167011300 0
z3n 0 1669 5750.077 5713.83516690166911311 0
OpenSMT 0 1668 9115.05 9059.98816680166811322 0
CVC4 0 1667 10682.324 10672.83616670166711333 0
SMTInterpol 0 1635 56663.725 52328.567163501635116535 0
SMTInterpol-fixedn 0 1635 56698.888 52342.66163501635116535 0
MathSAT5n 0 1632 45157.772 45146.377163201632116834 0
Alt-Ergo 0 1415 1167423.921 520963.251415014151385352 19

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2798 188.71 246.03727981130166822 0
Yices2 0 2798 247.793 257.34527981130166822 0
2019-Yices 2.6.2n 0 2798 248.427 259.21827981130166822 0
Yices2-fixedn 0 2798 247.625 262.12627981130166822 0
veriT 0 2798 351.712 350.94427981130166822 0
z3n 0 2769 1986.953 1975.6662769112816413131 0
OpenSMT 0 2766 2770.973 2760.0912766112716393434 0
CVC4 0 2760 2974.161 2961.7992760112716334040 0
SMTInterpol 0 2719 11269.114 5793.572719112915908181 0
SMTInterpol-fixedn 0 2719 11282.511 5796.4932719112915908181 0
MathSAT5n 0 2715 2419.792 2408.1162715111316028564 0
Alt-Ergo 0 777 72671.753 51200.421777077720231770 19

n Non-competing.