SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_ANIA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4CVC4 CVC4 CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-CVC4n 0 89 6884.769 6886.7728982755 0
CVC4 0 89 7275.399 7277.4038982755 0
MathSAT5n 0 87 617.902 617.9268780770 0
z3n 0 55 51092.496 51096.808554873939 0
Alt-Ergo 0 5 6288.931 3497.395505892 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-CVC4n 0 89 6886.349 6886.6128982755 0
CVC4 0 89 7276.739 7277.1738982755 0
MathSAT5n 0 87 617.902 617.9268780770 0
z3n 0 55 51098.086 51095.028554873939 0
Alt-Ergo 0 5 6288.931 3497.395505892 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-CVC4n 0 82 5182.32 5182.41682820125 0
CVC4 0 82 5706.432 5706.74882820125 0
MathSAT5n 0 80 22.1 22.10680800140 0
z3n 0 48 49869.038 49865.974484804639 0
Alt-Ergo 0 0 2551.6 762.06000942 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
MathSAT5n 0 7 595.803 595.82707870 0
z3n 0 7 1229.048 1229.0537078739 0
CVC4 0 7 1570.307 1570.425707875 0
2019-CVC4n 0 7 1704.028 1704.196707875 0
Alt-Ergo 0 5 3737.331 2735.335505892 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
MathSAT5n 0 83 129.641 129.64983803114 0
2019-CVC4n 0 81 451.572 451.569817831313 0
CVC4 0 81 465.638 465.71817831313 0
z3n 0 43 1278.686 1274.934433675151 0
Alt-Ergo 0 3 1015.337 395.973303916 0

n Non-competing.