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

AUFLIA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-CVC4n 0 1354 323098.765 331543.47113541371217284255 0
Vampire 0 1353 352366.428 344905.49213531001253285285 0
Vampire - fixedn 0 1341 347553.311 342652.1541341981243297283 0
2020-Vampiren 0 1333 349111.74 341383.97313331001233305282 0
cvc5 0 1332 188647.483 353990.80413321271205306281 0
cvc5 - fixedn 0 1327 179959.968 357364.64413271291198311285 0
z3n 0 1298 378668.041 379115.95512981761122340282 3
2020-z3n 0 1294 385487.123 387008.6312941741120344277 11
2018-CVC4n 0 1221 330661.564 338212.7711221981123417256 0
veriT 0 1212 312278.164 312325.992121201212426254 0
SMTInterpol 0 1115 524887.234 520707.1061115911024523409 0
UltimateEliminator+MathSAT 0 47 58093.298 49172.281471433159124 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 1360374996.308340735.70413601001260278278 0
2020-CVC4n 0 1354330880.675331530.87113541371217284255 0
Vampire - fixedn 0 1347362566.601338580.4061347981249291276 0
2020-Vampiren 0 1336360759.34339842.73113361001236302278 0
cvc5 0 1332353609.935353975.68413321271205306281 0
cvc5 - fixedn 0 1327356956.087357348.96413271291198311285 0
z3n 0 1298378747.441379104.07512981761122340282 3
2020-z3n 0 1294386406.903386996.0712941741120344277 11
2018-CVC4n 0 1221337733.004338202.2011221981123417256 0
veriT 0 1212312318.044312314.692121201212426254 0
SMTInterpol 0 1115541595.304508228.0671115911024523387 0
UltimateEliminator+MathSAT 0 4758093.29849172.281471433159124 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
z3n 0 1766825.1286825.64176176061456282 3
2020-z3n 0 1747373.0247373.867174174081456277 11
2020-CVC4n 0 13729136.93929273.5841371370451456255 0
cvc5 - fixedn 0 12941033.50541176.2711291290531456285 0
cvc5 0 12743824.13643904.5881271270551456281 0
2020-Vampiren 0 100102018.05298406.4711001000821456278 0
Vampire 0 100105617.14998407.6451001000821456278 0
2018-CVC4n 0 9834620.15334732.11698980841456256 0
Vampire - fixedn 0 9898415.52898410.71298980841456276 0
SMTInterpol 0 9122104.50421914.97491910911456387 0
UltimateEliminator+MathSAT 0 142020.8681336.99714140168145624 0
veriT 0 046446.43146446.2040001821456254 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Vampire 0 126052178.43932348.18912600126021357278 0
Vampire - fixedn 0 124950550.87330177.35412490124932357276 0
2020-Vampiren 0 123648741.28831436.2612360123645357278 0
2020-CVC4n 0 121791743.73692257.28712170121764357255 0
veriT 0 121287540.97687537.7312120121269357254 0
cvc5 0 120599785.799100071.09612050120576357281 0
cvc5 - fixedn 0 1198105922.582106172.69311980119883357285 0
2018-CVC4n 0 112393741.92694098.642112301123158357256 0
z3n 0 1122175110.897175464.882112201122159357282 3
2020-z3n 0 1120178549.042178888.757112001120161357277 11
SMTInterpol 0 1024338848.6312088.125102401024257357387 0
UltimateEliminator+MathSAT 0 3341746.15135780.68433033124835724 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Vampire 0 13329167.0487947.38313321001232306306 0
Vampire - fixedn 0 13219104.0817891.7041321981223317304 0
2020-Vampiren 0 13098901.9217860.26713091001209329306 0
z3n 0 12699218.4079218.65812691751094369366 3
2020-z3n 0 12649339.2699339.47912641741090374362 11
cvc5 0 12209823.0919825.08612201001120418399 0
cvc5 - fixedn 0 12209833.6849826.43912201001120418399 0
2018-CVC4n 0 121910202.84310198.2461219971122419411 0
2020-CVC4n 0 12159933.7979935.4291215991116423404 0
veriT 0 11987561.4037557.218119801198440279 0
SMTInterpol 0 103815378.82513550.304103891947600498 0
UltimateEliminator+MathSAT 0 4712640.8067743.004471433159185 0

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