SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

AUFLIRA (Single Query Track)

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

Page generated on 2021-07-18 17:29:05 +0000

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 1608 90164.945 90135.39616085315557574 1
2020-CVC4n 0 1562 148513.397 149466.452156201562121120 0
cvc5 - fixedn 0 1555 80808.839 159244.378155501555128126 0
z3n 0 1554 110384.959 110499.1715540155412974 0
2020-z3n 0 1554 112292.198 112314.07715540155412981 0
cvc5 0 1553 75746.161 161455.373155301553130128 0
Vampire 0 1533 184721.149 181732.207153301533150150 0
Vampire - fixedn 0 1514 183423.582 179351.782151401514169148 0
2020-Vampiren 0 1510 183402.066 179368.739151001510173148 0
veriT 0 1335 416474.05 416511.216133501335348274 73
SMTInterpol 0 1244 533778.971 532928.15124401244439439 0
UltimateEliminator+MathSAT 0 12 11125.04 7715.4581201216710 2

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 160890164.94590135.39616085315557574 1
2020-CVC4n 0 1562149417.237149460.382156201562121120 0
cvc5 - fixedn 0 1555159144.564159237.778155501555128126 0
Vampire 0 1555210663.939168565.556155501555128128 0
z3n 0 1554110462.959110495.915540155412974 0
2020-z3n 0 1554112307.408112310.50715540155412981 0
cvc5 0 1553161372.051161449.143155301553130128 0
Vampire - fixedn 0 1542215644.902162798.213154201542141120 0
2020-Vampiren 0 1538209414.926160372.923153801538145120 0
veriT 0 1335416499.58416500.636133501335348274 73
SMTInterpol 0 1244539217.691530571.359124401244439434 0
UltimateEliminator+MathSAT 0 1211125.047715.4581201216710 2

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2019-Par4n 0 531313.4271262.452535301162974 1
UltimateEliminator+MathSAT 0 0288.151181.4050005416290 2
2020-z3n 0 055259.75855259.92500054162981 0
z3n 0 060040.96160040.97400054162974 0
veriT 0 063616.3263616.319000541629274 73
2020-CVC4n 0 063763.47563764.346000541629120 0
cvc5 - fixedn 0 063771.82163774.162000541629126 0
cvc5 0 063773.9663776.311000541629128 0
2020-Vampiren 0 064800.064800.0000541629120 0
SMTInterpol 0 064800.064800.0000541629434 0
Vampire 0 064800.064800.0000541629128 0
Vampire - fixedn 0 064800.064800.0000541629120 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-CVC4n 0 156211253.76211296.0361562015625116120 0
2019-Par4n 0 155514451.51814472.9441555015551211674 1
cvc5 - fixedn 0 155520972.74321063.61615550155512116126 0
Vampire 0 155571463.93929365.55615550155512116128 0
z3n 0 155411886.06411886.941554015541311674 0
2020-z3n 0 155415435.99715437.2441554015541311681 0
cvc5 0 155323198.09123272.83215530155314116128 0
Vampire - fixedn 0 154276444.90223598.21315420154225116120 0
2020-Vampiren 0 153870214.92621172.92315380153829116120 0
veriT 0 1335278483.26278484.317133501335232116274 73
SMTInterpol 0 1244395619.351392493.691124401244323116434 0
UltimateEliminator+MathSAT 0 1210525.6137345.5321201215551160 2

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 16081964.9451935.39616085315557574 1
2020-z3n 0 15542918.5892919.571155401554129116 0
z3n 0 15513091.3593091.555155101551132116 0
Vampire 0 15175733.8394582.249151701517166166 0
cvc5 - fixedn 0 14984556.2594555.536149801498185185 0
cvc5 0 14984556.5954556.113149801498185185 0
2020-CVC4n 0 14984575.4484575.1149801498185185 0
Vampire - fixedn 0 14965764.6824584.774149601496187166 0
2020-Vampiren 0 14905527.4694569.212149001490193168 0
veriT 0 13358427.588428.636133501335348274 73
SMTInterpol 0 122112225.97411732.255122101221462462 0
UltimateEliminator+MathSAT 0 128773.045363.4581201216710 2

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.