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

AUFLIRA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4Vampire Vampire Vampire

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1280 79349.713 79314.47812804112396664 2
CVC4 0 1246 121889.106 122603.612460124610099 0
z3n 0 1238 94608.574 94628.12812380123810870 0
Vampire 0 1225 149640.278 146519.88122501225121121 0
Alt-Ergo 0 1206 155046.141 148710.889120601206140120 2
veriT 0 1073 327539.443 327585.059107301073273272 0
veriT+viten 0 1071 330065.753 330085.935107101071275202 73
SMTInterpol-fixedn 0 995 423622.196 421760.1429950995351348 0
SMTInterpol 0 995 423936.011 421945.7189950995351348 0
UltimateEliminator+MathSAT 0 0 44721.524 40887.366000134630 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1280 79349.713 79314.47812804112396664 2
Vampire 0 1248 166260.748 129581.6651248012489898 0
CVC4 0 1246 122588.736 122599.6712460124610099 0
z3n 0 1238 94623.044 94625.56812380123810870 0
Alt-Ergo 0 1217 173319.081 142481.244121701217129109 2
veriT 0 1073 327574.453 327575.269107301073273272 0
veriT+viten 0 1071 330078.823 330079.485107101071275202 73
SMTInterpol 0 995 442284.741 416608.2059950995351333 0
SMTInterpol-fixedn 0 995 433182.626 417552.3819950995351338 0
UltimateEliminator+MathSAT 0 0 44721.524 40887.366000134630 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 41 1311.384 1260.12341410130564 2
UltimateEliminator+MathSAT 0 0 167.487 107.533000134630 0
z3n 0 0 43408.828 43408.839000134670 0
SMTInterpol-fixedn 0 0 48995.933 48360.5160001346338 0
Alt-Ergo 0 0 49200.4 49200.130001346109 2
SMTInterpol 0 0 49225.143 49212.7940001346333 0
CVC4 0 0 49474.22 49474.347000134699 0
veriT 0 0 49876.34 49876.4870001346272 0
veriT+viten 0 0 50400.0 50400.00001346202 73
Vampire 0 0 50400.0 50400.0000134698 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1248 48660.408 15585.4951248012489898 0
CVC4 0 1246 9514.516 9525.32312460124610099 0
2019-Par4n 0 1239 14438.329 14454.35412390123910764 2
z3n 0 1238 14826.481 14826.66112380123810870 0
Alt-Ergo 0 1217 75901.492 48868.345121701217129109 2
veriT 0 1073 214098.113 214098.782107301073273272 0
veriT+viten 0 1071 216078.823 216079.485107101071275202 73
SMTInterpol 0 995 329039.148 304392.2159950995351333 0
SMTInterpol-fixedn 0 995 319951.773 306130.9789950995351338 0
UltimateEliminator+MathSAT 0 0 44367.757 40652.648000134630 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1280 1733.713 1698.47812804112396664 2
z3n 0 1238 2383.554 2383.69412380123810894 0
Vampire 0 1214 4347.846 3590.148121401214132132 0
CVC4 0 1198 3663.935 3663.643119801198148148 0
Alt-Ergo 0 1189 4230.507 3638.529118901189157138 2
veriT+viten 0 1071 6678.823 6679.485107101071275202 73
veriT 0 1070 6690.062 6690.721107001070276276 0
SMTInterpol-fixedn 0 987 9417.32 9072.2159870987359358 0
SMTInterpol 0 987 9422.607 9072.7189870987359358 0
UltimateEliminator+MathSAT 0 0 5775.429 4218.25000134643 0

n Non-competing.