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

UFLRA (Single Query Track)

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

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

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Alt-Ergo Alt-Ergo veriT Alt-Ergo

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Z3n 0 5 4901.023 4901.347 5 3 2 2 2 0
Z3n 0 4 7207.683 7208.314 4 2 2 3 3 0
Alt-Ergo 0 2 5614.731 5132.964 2 0 2 5 2 0
veriT 0 2 9613.46 9615.16 2 0 2 5 4 0
Vampire 0 2 11098.071 10004.205 2 0 2 5 4 0
CVC4 0 2 11709.135 11710.704 2 0 2 5 4 0
SMTInterpol 0 1 12000.773 12000.59 1 0 1 6 5 0
UltimateEliminator+Yices-2.6.1 0 0 22.998 15.732 0 0 0 7 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 23.258 16.846 0 0 0 7 0 0
UltimateEliminator+SMTInterpol 0 0 23.294 14.932 0 0 0 7 0 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Z3n 0 5 4901.213 4901.237 5 3 2 2 2 0
Z3n 0 4 7208.243 7208.244 4 2 2 3 3 0
Alt-Ergo 0 2 5614.731 5132.964 2 0 2 5 2 0
veriT 0 2 9615.08 9615.07 2 0 2 5 4 0
Vampire 0 2 11098.071 10004.205 2 0 2 5 4 0
CVC4 0 2 11710.245 11710.464 2 0 2 5 4 0
SMTInterpol 0 1 12000.773 12000.59 1 0 1 6 5 0
UltimateEliminator+SMTInterpol 0 0 23.294 14.932 0 0 0 7 0 0
UltimateEliminator+Yices-2.6.1 0 0 22.998 15.732 0 0 0 7 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 23.258 16.846 0 0 0 7 0 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Z3n 0 3 4901.141 4901.166 3 3 0 4 2 0
Z3n 0 2 7208.171 7208.171 2 2 0 5 3 0
UltimateEliminator+SMTInterpol 0 0 16.618 10.62 0 0 0 7 0 0
UltimateEliminator+Yices-2.6.1 0 0 16.464 11.341 0 0 0 7 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 16.541 11.521 0 0 0 7 0 0
Alt-Ergo 0 0 5614.679 5132.913 0 0 0 7 2 0
SMTInterpol 0 0 9600.403 9600.307 0 0 0 7 5 0
veriT 0 0 9615.054 9615.045 0 0 0 7 4 0
Vampire 0 0 11097.53 10003.827 0 0 0 7 4 0
CVC4 0 0 11710.21 11710.43 0 0 0 7 4 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
veriT 0 2 0.025 0.025 2 0 2 5 4 0
CVC4 0 2 0.035 0.034 2 0 2 5 4 0
Alt-Ergo 0 2 0.052 0.051 2 0 2 5 2 0
2018-Z3n 0 2 0.072 0.072 2 0 2 5 2 0
Z3n 0 2 0.073 0.073 2 0 2 5 3 0
Vampire 0 2 0.541 0.378 2 0 2 5 4 0
SMTInterpol 0 1 2400.37 2400.282 1 0 1 6 5 0
UltimateEliminator+SMTInterpol 0 0 6.676 4.311 0 0 0 7 0 0
UltimateEliminator+Yices-2.6.1 0 0 6.535 4.391 0 0 0 7 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 6.717 5.326 0 0 0 7 0 0

24s Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Z3n 0 4 80.243 80.244 4 2 2 3 3 0
2018-Z3n 0 4 98.807 98.808 4 2 2 3 3 0
Alt-Ergo 0 2 96.207 96.107 2 0 2 5 4 0
veriT 0 2 111.08 111.07 2 0 2 5 4 0
CVC4 0 2 120.035 120.034 2 0 2 5 5 0
Vampire 0 2 120.541 120.378 2 0 2 5 5 0
SMTInterpol 0 1 120.773 120.59 1 0 1 6 5 0
UltimateEliminator+SMTInterpol 0 0 23.294 14.932 0 0 0 7 0 0
UltimateEliminator+Yices-2.6.1 0 0 22.998 15.732 0 0 0 7 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 23.258 16.846 0 0 0 7 0 0

n Non-competing.