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

AUFDTLIRA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
cvc5 - fixedn 0 4946 65830.062 65831.72849460494657453 0
cvc5 0 4946 65913.36 65917.81849460494657453 0
2020-CVC4n 0 4937 52107.636 52114.92449370493758343 0
2020-Vampiren 0 4645 1359830.738 1001861.123464504645875703 0
Vampire - fixedn 0 4456 1727186.881 1372133.97344560445610641021 0
Vampire 0 4445 1770017.162 1425263.39444450444510751075 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
cvc5 - fixedn 0 494665839.33265829.54849460494657453 0
cvc5 0 494665920.4565915.29849460494657453 0
2020-CVC4n 0 493752113.84652112.55449370493758343 0
2020-Vampiren 0 47031438531.558934262.223470304703817603 0
Vampire 0 46481921036.5121281645.076464804648872869 0
Vampire - fixedn 0 46131869645.3811269393.177461304613907861 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2020-Vampiren 0 00.00.000005520603 0
2020-CVC4n 0 00.00.00000552043 0
cvc5 0 00.00.00000552053 0
Vampire 0 00.00.000005520869 0
Vampire - fixedn 0 00.00.000005520861 0
cvc5 - fixedn 0 00.00.00000552053 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
cvc5 - fixedn 0 494643648.95843639.26549460494625032453 0
cvc5 0 494643713.58443708.0849460494625032453 0
2020-CVC4n 0 493734087.97134086.79449370493725932443 0
2020-Vampiren 0 47031054617.138551971.87470304703493324603 0
Vampire 0 46481528636.382892854.626464804648548324869 0
Vampire - fixedn 0 46131480845.381880593.177461304613583324861 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
cvc5 0 49442030.8582025.36549440494457662 0
cvc5 - fixedn 0 49432045.0312034.91449430494357763 0
2020-CVC4n 0 49371510.4261509.13549370493758344 0
Vampire 0 376251228.46846462.82237620376217581758 0
Vampire - fixedn 0 373751293.77146429.89837370373717831751 0
2020-Vampiren 0 334058750.26454966.44133400334021802148 0

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