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

UFIDL (Single Query Track)

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

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

Benchmarks: 20
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 12 20236.029 19748.761123988 0
Z3n 0 11 15689.359 15692.729112996 0
2018-Z3n 0 11 16071.642 16073.027112996 0
CVC4 0 10 19802.131 20279.1551019108 0
veriT 0 7 26302.614 26306.9177071310 0
SMTInterpol 0 7 28947.169 28907.7647161312 0
Vampire 0 7 31220.601 31206.3917071313 0
UltimateEliminator+Yices-2.6.1 0 0 14449.287 14433.182000206 0
UltimateEliminator+MathSAT-5.5.4 0 0 14449.498 14433.097000206 0
UltimateEliminator+SMTInterpol 0 0 14451.431 14429.896000206 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 12 20236.029 19748.761123988 0
Z3n 0 11 15692.139 15692.639112996 0
2018-Z3n 0 11 16072.462 16072.907112996 0
CVC4 0 10 20175.351 20278.7451019108 0
veriT 0 7 26306.454 26306.6377071310 0
SMTInterpol 0 7 28947.169 28907.7647161312 0
Vampire 0 7 31220.601 31206.3917071313 0
UltimateEliminator+SMTInterpol 0 0 20655.421 14273.006000205 0
UltimateEliminator+Yices-2.6.1 0 0 20755.737 14308.432000205 0
UltimateEliminator+MathSAT-5.5.4 0 0 21032.878 14376.617000205 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 3 1035.971 548.098330178 0
2018-Z3n 0 2 2400.109 2400.109220186 0
Z3n 0 2 2400.113 2400.113220186 0
CVC4 0 1 974.039 1077.436110198 0
SMTInterpol 0 1 2401.044 2400.6541101912 0
UltimateEliminator+SMTInterpol 0 0 10.148 6.357000205 0
UltimateEliminator+MathSAT-5.5.4 0 0 10.076 7.01000205 0
UltimateEliminator+Yices-2.6.1 0 0 9.989 7.109000205 0
veriT 0 0 2400.236 2400.2120002010 0
Vampire 0 0 7200.0 7200.00002013 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 9 0.057 0.663909118 0
2018-Z3n 0 9 0.753 0.753909116 0
Z3n 0 9 0.778 0.778909116 0
CVC4 0 9 1.312 1.309909118 0
veriT 0 7 4706.218 4706.4267071310 0
Vampire 0 7 4820.601 4806.3917071313 0
SMTInterpol 0 6 7346.125 7307.116061412 0
UltimateEliminator+SMTInterpol 0 0 20614.607 14249.458000205 0
UltimateEliminator+Yices-2.6.1 0 0 20717.944 14282.526000205 0
UltimateEliminator+MathSAT-5.5.4 0 0 20994.753 14350.673000205 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 11 216.069 216.785112999 0
2018-Z3n 0 11 216.862 216.862112999 0
Z3n 0 11 216.891 216.891112999 0
CVC4 0 9 217.903 217.895909119 0
veriT 0 7 264.514 264.4877071311 0
Vampire 0 7 332.601 318.3917071313 0
SMTInterpol 0 6 366.146 337.0636151413 0
UltimateEliminator+SMTInterpol 0 0 195.431 173.896000206 0
UltimateEliminator+MathSAT-5.5.4 0 0 193.498 177.097000206 0
UltimateEliminator+Yices-2.6.1 0 0 193.287 177.182000206 0

n Non-competing.