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

ALIA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
SMTInterpolSMTInterpolSMTInterpol CVC4 SMTInterpol

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 19 1.181 1.1821911800 0
z3n 0 19 1.258 1.2611911800 0
SMTInterpol-fixedn 0 19 152.058 61.9971911800 0
SMTInterpol 0 19 154.548 62.4811911800 0
CVC4 0 18 3.189 3.1911801810 0
Alt-Ergo 0 18 11.288 4.6451801810 0
Vampire 0 15 5381.224 5090.6511501544 0
veriT 0 4 17886.136 17889.3054041514 0
veriT+viten 0 4 17998.358 18000.454041514 1
UltimateEliminator+MathSAT 0 0 15632.998 15621.1770001913 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 19 1.181 1.1821911800 0
z3n 0 19 1.258 1.2611911800 0
SMTInterpol-fixedn 0 19 152.058 61.9971911800 0
SMTInterpol 0 19 154.548 62.4811911800 0
CVC4 0 18 3.189 3.1911801810 0
Alt-Ergo 0 18 11.288 4.6451801810 0
Vampire 0 17 7771.684 3953.2711701722 0
veriT 0 4 17888.316 17888.7154041514 0
veriT+viten 0 4 18000.058 18000.064041514 1
UltimateEliminator+MathSAT 0 0 15632.998 15621.1770001913 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 1 0.051 0.051110180 0
2018-Z3n 0 1 0.054 0.054110180 0
SMTInterpol 0 1 0.695 0.428110180 0
SMTInterpol-fixedn 0 1 0.693 0.433110180 0
CVC4 0 0 0.289 0.296000190 0
Alt-Ergo 0 0 1.148 0.434000190 0
UltimateEliminator+MathSAT 0 0 3.452 2.4410001913 0
veriT 0 0 1088.25 1088.650001914 0
veriT+viten 0 0 1200.0 1200.00001914 1
Vampire 0 0 1200.0 1200.0000192 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 18 1.126 1.1281801810 0
z3n 0 18 1.208 1.211801810 0
CVC4 0 18 2.9 2.8951801810 0
Alt-Ergo 0 18 10.139 4.2121801810 0
SMTInterpol-fixedn 0 18 151.366 61.5641801810 0
SMTInterpol 0 18 153.853 62.0531801810 0
Vampire 0 17 6571.684 2753.2711701722 0
veriT+viten 0 4 16800.058 16800.064041514 1
veriT 0 4 16800.066 16800.0654041514 0
UltimateEliminator+MathSAT 0 0 15629.546 15618.7360001913 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 19 1.181 1.1821911800 0
z3n 0 19 1.258 1.2611911800 0
SMTInterpol-fixedn 0 19 152.058 61.9971911800 0
SMTInterpol 0 19 154.548 62.4811911800 0
CVC4 0 18 3.189 3.1911801810 0
Alt-Ergo 0 18 11.288 4.6451801810 0
Vampire 0 7 301.916 295.4247071212 0
veriT+viten 0 4 360.058 360.064041514 1
veriT 0 4 360.066 360.0654041515 0
UltimateEliminator+MathSAT 0 0 344.998 333.1770001913 0

n Non-competing.