SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

SMT-LIB

UFLRA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Alt-ErgoAlt-Ergo veriT Alt-Ergo

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 5 4901.023 4901.34753222 0
Z3n 0 4 7207.683 7208.31442233 0
Alt-Ergo 0 2 5614.731 5132.96420252 0
veriT 0 2 9613.46 9615.1620254 0
Vampire 0 2 11098.071 10004.20520254 0
CVC4 0 2 11709.135 11710.70420254 0
SMTInterpol 0 1 12000.773 12000.5910165 0
UltimateEliminator+Yices-2.6.1 0 0 22.998 15.73200070 0
UltimateEliminator+MathSAT-5.5.4 0 0 23.258 16.84600070 0
UltimateEliminator+SMTInterpol 0 0 23.294 14.93200070 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 5 4901.213 4901.23753222 0
Z3n 0 4 7208.243 7208.24442233 0
Alt-Ergo 0 2 5614.731 5132.96420252 0
veriT 0 2 9615.08 9615.0720254 0
Vampire 0 2 11098.071 10004.20520254 0
CVC4 0 2 11710.245 11710.46420254 0
SMTInterpol 0 1 12000.773 12000.5910165 0
UltimateEliminator+SMTInterpol 0 0 23.294 14.93200070 0
UltimateEliminator+Yices-2.6.1 0 0 22.998 15.73200070 0
UltimateEliminator+MathSAT-5.5.4 0 0 23.258 16.84600070 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 3 4901.141 4901.16633042 0
Z3n 0 2 7208.171 7208.17122053 0
UltimateEliminator+SMTInterpol 0 0 16.618 10.6200070 0
UltimateEliminator+Yices-2.6.1 0 0 16.464 11.34100070 0
UltimateEliminator+MathSAT-5.5.4 0 0 16.541 11.52100070 0
Alt-Ergo 0 0 5614.679 5132.91300072 0
SMTInterpol 0 0 9600.403 9600.30700075 0
veriT 0 0 9615.054 9615.04500074 0
Vampire 0 0 11097.53 10003.82700074 0
CVC4 0 0 11710.21 11710.4300074 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
veriT 0 2 0.025 0.02520254 0
CVC4 0 2 0.035 0.03420254 0
Alt-Ergo 0 2 0.052 0.05120252 0
2018-Z3n 0 2 0.072 0.07220252 0
Z3n 0 2 0.073 0.07320253 0
Vampire 0 2 0.541 0.37820254 0
SMTInterpol 0 1 2400.37 2400.28210165 0
UltimateEliminator+SMTInterpol 0 0 6.676 4.31100070 0
UltimateEliminator+Yices-2.6.1 0 0 6.535 4.39100070 0
UltimateEliminator+MathSAT-5.5.4 0 0 6.717 5.32600070 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 4 80.243 80.24442233 0
2018-Z3n 0 4 98.807 98.80842233 0
Alt-Ergo 0 2 96.207 96.10720254 0
veriT 0 2 111.08 111.0720254 0
CVC4 0 2 120.035 120.03420255 0
Vampire 0 2 120.541 120.37820255 0
SMTInterpol 0 1 120.773 120.5910165 0
UltimateEliminator+SMTInterpol 0 0 23.294 14.93200070 0
UltimateEliminator+Yices-2.6.1 0 0 22.998 15.73200070 0
UltimateEliminator+MathSAT-5.5.4 0 0 23.258 16.84600070 0

n Non-competing.