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

UFNIA (Single Query Track)

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

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

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

Winners

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

Note: the division has disagreements

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 3027 2608159.954 2511037.6523027592243520092009 0
CVC4 0 2789 2655725.776 2729013.2772789571221822472178 0
z3n 0 2205 2256486.679 2258220.1762205510169528311618 4
Vampire 0 1742 4128912.762 3998009.6117420174232943294 0
2018-Vampiren 0 1584 4498882.787 4232338.45415840158434523452 0
Alt-Ergo 0 790 3462659.259 3268625.415790079042462518 124
UltimateEliminator+MathSAT 0 651 395863.993 392519.8486515081434385316 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 3040 2614010.284 2506403.8173040593244719961996 0
CVC4 0 2789 2725980.375 2728891.1772789571221822472178 0
z3n 0 2205 2258043.029 2258151.0062205510169528311618 4
Vampire 0 2153 4892770.572 3796663.41121530215328832883 0
Alt-Ergo 0 833 3733777.999 3097009.735833083342032195 124
UltimateEliminator+MathSAT 0 651 396710.433 392097.7256515081434385315 0
2018-Vampiren 1 2555 7191155.507 3798960.90525550255524812480 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 593 37654.343 24443.315593593044431996 0
CVC4 0 571 44280.363 44481.478571571044652178 0
z3n 0 510 93128.876 93106.596510510045261618 4
UltimateEliminator+MathSAT 0 508 38306.219 37643.39550850804528315 0
Alt-Ergo 0 0 122946.193 119344.30200050362195 124
Vampire 0 0 740402.4 722362.4400050362883 0
2018-Vampiren 1 41 1074213.89 714367.8554104149952480 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Vampiren 0 2555 4405103.327 1695717.59525550255524812480 0
2019-Par4n 0 2488 1143609.574 1049188.767248841244725481996 0
CVC4 0 2258 1273347.722 1276069.433225840221827782178 0
Vampire 0 2153 2721966.102 1690761.49121530215328832883 0
z3n 0 1732 1160160.209 1160253.836173237169533041618 4
Alt-Ergo 0 833 2629733.797 2099501.74833083342032195 124
UltimateEliminator+MathSAT 0 180 320946.424 318238.263180371434856315 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2577 64066.115 61782.5822577552202524592459 0
CVC4 0 2273 68490.195 68465.2462273513176027632756 0
z3n 0 2096 66464.07 66396.9362096487160929402569 4
Vampire 0 1221 100752.583 94032.37412210122138153815 0
2018-Vampiren 0 1185 98863.665 94174.30311850118538513851 0
Alt-Ergo 0 689 79759.32 75276.063689068943472936 124
UltimateEliminator+MathSAT 0 650 24380.144 19245.8986505071434386326 0

n Non-competing.