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

BVFP (Single Query Track)

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

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

Benchmarks: 224
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-Z3n 0 181 33976.556 33925.24181169124324 0
CVC4 0 113 38475.375 38480.586113109411132 0
UltimateEliminator+MathSAT 0 27 1978.266 1731.256272341971 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Z3n 0 181 33982.226 33924.06181169124324 0
CVC4 0 113 38479.305 38479.356113109411132 0
UltimateEliminator+MathSAT 0 27 1978.266 1731.256272341971 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Z3n 0 169 22430.837 22430.00316916905524 0
CVC4 0 109 34834.837 34834.797109109011532 0
UltimateEliminator+MathSAT 0 23 660.79 450.771232302011 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Z3n 0 12 401.902 401.9311201221224 0
CVC4 0 4 4.888 4.88540422032 0
UltimateEliminator+MathSAT 0 4 44.144 30.3544042201 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Z3n 0 155 1797.934 1796.47715514696956 0
CVC4 0 113 847.305 847.356113109411132 0
UltimateEliminator+MathSAT 0 27 802.266 555.256272341971 0

n Non-competing.