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

AUFLIA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 1098 257281.701 262511.0431098111987212199 0
Vampire 0 1097 261861.107 257390.7351097811016213213 0
CVC4 0 1092 255795.226 261782.871092107985218201 0
z3n 0 1029 321149.757 323125.811029121908281232 11
veriT 0 968 352802.973 352854.1219680968342216 0
Alt-Ergo 0 954 334862.185 326384.1729540954356244 24
veriT+viten 0 953 274942.543 274951.6919530953357212 8
SMTInterpol-fixedn 0 801 520164.434 518127.05980152749509419 0
SMTInterpol 0 801 520208.63 518159.74480152749509419 0
UltimateEliminator+MathSAT 0 15 74114.268 72067.3051569129557 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1099 272122.177 256380.9021099811018211211 0
2018-CVC4n 0 1098 262178.991 262501.9231098111987212199 0
CVC4 0 1092 261524.776 261773.11092107985218201 0
z3n 0 1029 322128.537 323115.251029121908281232 11
veriT 0 968 352834.183 352845.5919680968342216 0
Alt-Ergo 0 965 356181.245 319964.8469650965345233 24
veriT+viten 0 953 274964.003 274942.9119530953357212 8
SMTInterpol-fixedn 0 802 520618.064 516957.60180252750508416 0
SMTInterpol 0 801 520629.81 517656.6280152749509418 0
UltimateEliminator+MathSAT 0 15 74114.268 72067.3051569129557 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3n 0 121 11679.088 11680.73612112101189232 11
2018-CVC4n 0 111 27060.282 27142.71611111101199199 0
CVC4 0 107 24353.515 24404.51510710701203201 0
Vampire 0 81 62411.936 62408.454818101229211 0
SMTInterpol 0 52 23287.777 23103.422525201258418 0
SMTInterpol-fixedn 0 52 23296.832 23105.78525201258416 0
UltimateEliminator+MathSAT 0 6 472.515 321.543660130457 0
veriT+viten 0 0 39693.356 39685.5320001310212 8
Alt-Ergo 0 0 68822.387 64670.4430001310233 24
veriT 0 0 92291.747 92298.6210001310216 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1018 27309.861 18777.919101801018292211 0
2018-CVC4n 0 987 60666.751 60907.1849870987323199 0
CVC4 0 985 62717.858 62915.0019850985325201 0
veriT 0 968 99615.147 99617.649680968342216 0
Alt-Ergo 0 965 120363.46 88657.7359650965345233 24
veriT+viten 0 953 90660.668 90647.7759530953357212 8
z3n 0 908 141316.784 142297.3469080908402232 11
SMTInterpol-fixedn 0 750 342630.863 339238.787500750560416 0
SMTInterpol 0 749 342663.581 339949.1187490749561418 0
UltimateEliminator+MathSAT 0 9 41683.783 40079.132909130157 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1080 6853.416 5946.875108081999230230 0
z3n 0 1011 7470.127 7470.2171011120891299288 11
2018-CVC4n 0 977 8124.811 8124.54997766911333331 0
CVC4 0 975 8002.191 8003.1797566909335326 0
veriT+viten 0 946 7591.149 7569.8189460946364238 8
Alt-Ergo 0 931 9664.048 7844.2589310931379274 24
veriT 0 880 10452.077 10451.9588800880430430 0
SMTInterpol 0 762 13216.868 12121.28176252710548465 0
SMTInterpol-fixedn 0 762 13219.219 12131.68476252710548465 0
UltimateEliminator+MathSAT 0 15 6133.584 4617.2531569129561 0

n Non-competing.