SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

UFLIA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4SMTInterpol CVC4 CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1329 1154965.807 1144351.663132951324949907 42
CVC4 0 1307 1166696.778 1180752.12130721305971955 0
veriT 0 1263 1242519.129 1242652.0941263012631015972 12
Vampire 0 1223 1334156.22 1283319.0512230122310551055 0
veriT+viten 0 1206 1250242.688 1250340.74612060120610721029 4
Alt-Ergo 0 1078 1427231.281 1392943.90610780107812001129 20
z3n 0 1057 1198690.108 1201019.4381057510521221829 9
SMTInterpol 0 284 2333003.764 2331054.501284328119941938 0
SMTInterpol-fixedn 0 284 2333069.191 2331097.743284328119941938 0
UltimateEliminator+MathSAT 0 0 25174.454 22529.603000227814 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1345 1163033.407 1134270.494134571338933891 42
CVC4 0 1307 1180355.998 1180708.28130721305971955 0
veriT 0 1263 1242635.439 1242614.7541263012631015972 12
Vampire 0 1255 1439814.88 1264098.10812550125510231023 0
veriT+viten 0 1206 1250335.438 1250304.12612060120610721029 4
Alt-Ergo 0 1112 1474430.401 1370608.81211120111211661094 20
z3n 0 1057 1199972.418 1200982.6681057510521221829 9
SMTInterpol 0 284 2342704.484 2328601.656284328119941931 0
SMTInterpol-fixedn 0 284 2346851.701 2328906.414284328119941930 0
UltimateEliminator+MathSAT 0 0 25174.454 22529.603000227814 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 7 4117.96 2176.6317702271891 42
z3n 0 5 3600.277 3600.2775502273829 9
SMTInterpol 0 3 4803.715 4802.04833022751931 0
SMTInterpol-fixedn 0 3 4803.747 4802.08633022751930 0
CVC4 0 2 5270.981 5279.3612202276955 0
UltimateEliminator+MathSAT 0 0 27.816 19.201000227814 0
Alt-Ergo 0 0 2401.413 2400.49300022781094 20
veriT+viten 0 0 3010.593 3010.69800022781029 4
veriT 0 0 6921.984 6922.3790002278972 12
Vampire 0 0 9600.0 9600.000022781023 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1338 104115.447 77293.864133801338940891 42
CVC4 0 1305 134112.021 134453.687130501305973955 0
veriT 0 1263 194775.559 194751.0541263012631015972 12
Vampire 0 1255 314211.52 199752.08812550125510231023 0
veriT+viten 0 1206 226046.526 226014.7212060120610721029 4
Alt-Ergo 0 1112 451501.515 362512.67311120111211661094 20
z3n 0 1052 344594.655 344728.2081052010521226829 9
SMTInterpol 0 281 1341409.22 1333181.901281028119971931 0
SMTInterpol-fixedn 0 281 1339373.04 1333464.798281028119971930 0
UltimateEliminator+MathSAT 0 0 21928.031 20167.339000227814 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1276 25918.42 24805.9871276512711002960 42
veriT+viten 0 1185 27169.124 27136.91111850118510931062 4
CVC4 0 1161 28023.312 27964.89411610116111171108 0
Vampire 0 1047 37735.654 31743.18410470104712311231 0
z3n 0 1012 31547.757 31526.22110125100712661257 9
Alt-Ergo 0 1000 38900.417 32221.64810000100012781222 20
veriT 0 951 32349.708 32345.11951095113271315 12
SMTInterpol 0 263 48976.823 47809.23263326020151960 0
SMTInterpol-fixedn 0 263 48968.879 47813.358263326020151960 0
UltimateEliminator+MathSAT 0 0 8750.685 5903.693000227816 0

n Non-competing.