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

UFLRA (Single Query Track)

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

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

Benchmarks: 7
Time Limit: 1200 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
z3n 0 5 2769.397 2769.48653222 0
2018-Z3n 0 5 3367.137 3367.71853222 0
veriT+viten 0 2 2478.152 2478.41420252 0
Alt-Ergo 0 2 3593.873 3056.14220252 0
SMTInterpol-fixedn 0 2 4801.761 4801.15820254 0
SMTInterpol 0 2 4801.778 4801.19420254 0
CVC4 0 2 5996.614 6000.43420255 0
veriT 0 2 5998.615 6000.25920255 0
Vampire 0 2 6005.8 6002.50420255 0
UltimateEliminator+MathSAT 0 0 23.435 16.4400070 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 5 2769.397 2769.48653222 0
2018-Z3n 0 5 3367.327 3367.64853222 0
veriT+viten 0 2 2478.312 2478.32420252 0
Alt-Ergo 0 2 3593.873 3056.14220252 0
SMTInterpol-fixedn 0 2 4801.761 4801.15820254 0
SMTInterpol 0 2 4801.778 4801.19420254 0
veriT 0 2 6000.025 6000.02920255 0
CVC4 0 2 6000.034 6000.03420255 0
Vampire 0 2 6005.8 6002.50420255 0
UltimateEliminator+MathSAT 0 0 23.435 16.4400070 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 3 2769.332 2769.42233042 0
2018-Z3n 0 3 3367.254 3367.57533042 0
UltimateEliminator+MathSAT 0 0 16.753 11.76500070 0
veriT+viten 0 0 2478.292 2478.29400072 0
Alt-Ergo 0 0 3593.821 3056.08900072 0
SMTInterpol-fixedn 0 0 4800.636 4800.40800074 0
SMTInterpol 0 0 4800.64 4800.43400074 0
veriT 0 0 6000.0 6000.000075 0
Vampire 0 0 6000.0 6000.000075 0
CVC4 0 0 6000.0 6000.000075 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
veriT 0 2 0.025 0.02920255 0
veriT+viten 0 2 0.02 0.0320252 0
CVC4 0 2 0.034 0.03420255 0
Alt-Ergo 0 2 0.053 0.05320252 0
z3n 0 2 0.064 0.06420252 0
2018-Z3n 0 2 0.073 0.07320252 0
SMTInterpol-fixedn 0 2 1.125 0.74920254 0
SMTInterpol 0 2 1.139 0.7620254 0
Vampire 0 2 5.8 2.50420255 0
UltimateEliminator+MathSAT 0 0 6.682 4.67400070 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 4 95.263 95.26342233 0
z3n 0 3 98.109 98.10931244 0
veriT+viten 0 2 73.499 73.50920253 0
Alt-Ergo 0 2 96.19 96.10420254 0
SMTInterpol-fixedn 0 2 97.761 97.15820254 0
SMTInterpol 0 2 97.778 97.19420254 0
veriT 0 2 120.025 120.02920255 0
CVC4 0 2 120.034 120.03420255 0
Vampire 0 2 125.8 122.50420255 0
UltimateEliminator+MathSAT 0 0 23.435 16.4400070 0

n Non-competing.