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

ALIA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
SMTInterpolSMTInterpolSMTInterpol Alt-Ergo CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 19 1.165 1.1661911800 0
Z3n 0 19 1.244 1.2441911800 0
SMTInterpol 0 19 1092.681 978.1381911800 0
CVC4 0 18 4.744 4.7351801810 0
Alt-Ergo 0 18 2409.881 2404.4161801811 0
Vampire 0 13 18018.486 15312.5241301366 0
veriT 0 4 35996.46 36000.7294041515 0
UltimateEliminator+SMTInterpol 0 0 28908.211 28859.1860001912 0
UltimateEliminator+Yices-2.6.1 0 0 28946.248 28876.7860001912 0
UltimateEliminator+MathSAT-5.5.4 0 0 28949.546 28877.510001912 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 19 1.165 1.1661911800 0
Z3n 0 19 1.244 1.2441911800 0
SMTInterpol 0 19 1092.681 978.1381911800 0
CVC4 0 18 4.744 4.7351801810 0
Alt-Ergo 0 18 2409.881 2404.4161801811 0
Vampire 0 15 28678.916 14507.9141501544 0
veriT 0 4 36000.07 36000.0694041515 0
UltimateEliminator+Yices-2.6.1 0 0 44351.318 27591.446000199 0
UltimateEliminator+MathSAT-5.5.4 0 0 45313.206 27841.39000199 0
UltimateEliminator+SMTInterpol 0 0 39040.021 27967.9560001910 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 1 0.055 0.055110180 0
Z3n 0 1 0.056 0.056110180 0
SMTInterpol 0 1 1.383 0.59110180 0
CVC4 0 0 0.279 0.277000190 0
UltimateEliminator+SMTInterpol 0 0 3.344 2.2690001910 0
UltimateEliminator+Yices-2.6.1 0 0 3.295 2.359000199 0
UltimateEliminator+MathSAT-5.5.4 0 0 3.39 2.363000199 0
Alt-Ergo 0 0 2400.0 2400.0000191 0
Vampire 0 0 2400.0 2400.0000194 0
veriT 0 0 2400.0 2400.00001915 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 18 1.11 1.1111801810 0
Z3n 0 18 1.187 1.1881801810 0
Alt-Ergo 0 18 9.881 4.4161801811 0
CVC4 0 18 4.465 4.4581801810 0
SMTInterpol 0 18 1091.298 977.5471801810 0
Vampire 0 15 26278.916 12107.9141501544 0
veriT 0 4 33600.07 33600.0694041515 0
UltimateEliminator+Yices-2.6.1 0 0 44348.023 27589.087000199 0
UltimateEliminator+MathSAT-5.5.4 0 0 45309.816 27839.027000199 0
UltimateEliminator+SMTInterpol 0 0 39036.677 27965.6870001910 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Z3n 0 19 1.165 1.1661911800 0
Z3n 0 19 1.244 1.2441911800 0
CVC4 0 18 4.744 4.7351801810 0
Alt-Ergo 0 18 33.881 28.4161801811 0
SMTInterpol 0 14 230.497 176.7261411355 0
Vampire 0 5 364.996 343.7865051414 0
veriT 0 4 360.07 360.0694041515 0
UltimateEliminator+SMTInterpol 0 0 344.452 332.3420001913 0
UltimateEliminator+Yices-2.6.1 0 0 343.827 333.4390001913 0
UltimateEliminator+MathSAT-5.5.4 0 0 344.049 333.440001913 0

n Non-competing.