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

UFDT (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
cvc5cvc5cvc5 cvc5 cvc5

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-CVC4n 0 531 1292956.003 1306804.9553113239910211021 0
cvc5 0 449 667497.647 1367384.5354497237711031103 0
2020-Vampiren 0 351 1464937.16 1442165.199351035112011195 0
Vampire 0 350 1471901.193 1449816.068350035012021201 0
Vampire - fixedn 0 346 1471429.523 1447972.46346034612061199 0
iProver - fixed2n 0 268 1566743.987 1542072.156268026812841195 83
iProver - fixedn 0 263 1569473.41 1547240.177263026312891180 103
iProver 0 259 1571495.854 1550600.303259025912931195 91

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-CVC4n 0 5311304237.9631306758.1153113239910211021 0
cvc5 0 4491366163.7151367329.0854497237711031103 0
2020-Vampiren 0 3891544406.01425966.7633892036911631153 0
Vampire 0 3781521090.1531434289.007378137711741173 0
Vampire - fixedn 0 3751514940.0131431091.467375237311771168 0
iProver - fixed2n 0 2821590552.9371534913.039282028212701180 83
iProver - fixedn 0 2791594533.961539221.739279027912731164 103
iProver 0 2771596045.5341540077.02277027712751176 91

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-CVC4n 0 13262384.73364695.2681321320214181021 0
cvc5 0 72106581.715107622.998727206214181103 0
2020-Vampiren 0 20218534.53156827.7422020011414181153 0
Vampire - fixedn 0 2166612.86160558.01722013214181168 0
Vampire 0 1167282.27160659.2511013314181173 0
iProver - fixedn 0 0153618.758153607.26700013414181164 103
iProver 0 0153620.886153607.75400013414181176 91
iProver - fixed2n 0 0153620.777153607.75600013414181180 83

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-CVC4n 0 39980253.2380462.84239903995111021021 0
cvc5 0 37797982.098106.08737703777311021103 0
Vampire 0 377185001.523112031.83737703777311021173 0
Vampire - fixedn 0 373186727.153108933.4537303737711021168 0
2020-Vampiren 0 369164271.47107539.02136903698111021153 0
iProver - fixed2n 0 282275300.38220323.745282028216811021180 83
iProver - fixedn 0 279279315.202224014.472279027917111021164 103
iProver 0 277280825.008226192.82277027717311021176 91

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2020-CVC4n 0 32129873.14229871.066321431712311231 0
cvc5 0 31829905.61729905.614318431412341234 0
2020-Vampiren 0 28033832.86131304.922280028012721267 0
Vampire 0 27834256.63931540.318278027812741274 0
Vampire - fixedn 0 27434236.54731534.941274027412781274 0
iProver - fixed2n 0 20336583.75533403.865203020313491260 83
iProver 0 20036462.11333423.097200020013521255 91
iProver - fixedn 0 19836381.66733438.875198019813541245 103

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