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

AUFDTNIRA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
cvc5 0 205 44676.858 44686.76420502059537 0
cvc5 - fixedn 0 205 44680.152 44689.51920502059537 0
2020-CVC4n 0 201 48013.16 48030.15620102019940 0
2020-Vampiren 0 200 158158.235 117402.798200020010084 0
Vampire - fixedn 0 191 190305.972 147150.1771910191109108 0
Vampire 0 186 197380.078 153555.3351860186114114 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-Vampiren 0 238235896.34568009.8652380238625 0
Vampire 0 207205540.358137253.89520702079393 0
cvc5 0 20544684.45844684.91420502059537 0
cvc5 - fixedn 0 20544687.84244687.87920502059537 0
Vampire - fixedn 0 205196032.852136492.86820502059594 0
2020-CVC4n 0 20148028.4948028.45620102019940 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-Vampiren 0 00.00.000003005 0
2020-CVC4n 0 00.00.0000030040 0
cvc5 0 00.00.0000030037 0
Vampire 0 00.00.0000030093 0
Vampire - fixedn 0 00.00.0000030094 0
cvc5 - fixedn 0 00.00.0000030037 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-Vampiren 0 238173372.22551299.804238023829335 0
Vampire 0 207165940.35897653.8952070207603393 0
cvc5 0 20517071.65317071.6482050205623337 0
cvc5 - fixedn 0 20517075.13117075.1562050205623337 0
Vampire - fixedn 0 205156432.85296892.8682050205623394 0
2020-CVC4n 0 20119227.48619227.4552010201663340 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
cvc5 - fixedn 0 2031013.0571013.04720302039739 0
cvc5 0 2031012.751013.15620302039739 0
2020-CVC4n 0 201988.49988.45620102019940 0
Vampire - fixedn 0 1175036.2624690.4421170117183183 0
Vampire 0 1175150.2484748.8731170117183183 0
2020-Vampiren 0 1055187.9744876.3361050105195192 0

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