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_NIA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 7009 2941229.205 2714107.01970094808220121862169 17
CVC4 0 6345 4536468.213 4566379.55463454593175228502850 0
MathSAT5n 0 6330 3792550.67 3792733.763304377195328652865 0
Yices2 0 6074 3893392.826 3893617.25460744075199931213121 0
Yices2-fixedn 0 6073 3875730.091 3903442.24660734074199931223122 0
z3n 0 5955 3862190.848 3862125.19459554334162132402646 6
AProVE 0 3184 6032877.719 7377595.57231843184060115937 0
SMT-RAT 0 1996 8808232.926 8809398.7291996180119571997166 3

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 7183 3130972.535 2611375.01771834952223120121995 17
CVC4 0 6346 4564678.227 4565830.62663464594175228492849 0
MathSAT5n 0 6330 3793231.75 3792607.6263304377195328652865 0
Yices2 0 6074 3893742.976 3893513.49460744075199931213121 0
Yices2-fixedn 0 6073 3902022.371 3903316.01660734074199931223122 0
z3n 0 5955 3862486.788 3862034.65459554334162132402646 6
AProVE 0 3186 7388501.518 7377531.14231863186060095935 0
SMT-RAT 0 1996 8809200.426 8809104.3291996180119571997166 3

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 4952 1033463.156 640144.42749524952042431995 17
CVC4 0 4594 1940019.392 1941282.2945944594046012849 0
MathSAT5n 0 4377 1460777.563 1460296.1543774377048182865 0
z3n 0 4334 1400034.439 1399717.343344334048612646 6
Yices2 0 4075 1655800.327 1655601.04840754075051203121 0
Yices2-fixedn 0 4074 1661985.021 1662501.46140744074051213122 0
AProVE 0 3186 2850073.499 2839113.42931863186060095935 0
SMT-RAT 0 1801 4459454.693 4459259.79818011801073947166 3

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 2231 265108.628 160809.0722310223169641995 17
Yices2 0 1999 427142.649 427112.44719990199971963121 0
Yices2-fixedn 0 1999 429237.351 430014.55519990199971963122 0
MathSAT5n 0 1953 521654.187 521511.4719530195372422865 0
CVC4 0 1752 813858.835 813748.33617520175274432849 0
z3n 0 1621 908614.652 908527.48216210162175742646 6
SMT-RAT 0 195 2538945.733 2539044.531195019590007166 3
AProVE 0 0 2790001.676 2790001.08200091955935 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 6288 127657.453 86631.86562884279200929072890 17
Yices2 0 5345 104190.735 104002.70253453486185938503850 0
Yices2-fixedn 0 5337 104477.715 104357.87453373480185738583858 0
MathSAT5n 0 4687 129075.367 128734.01246873132155545084508 0
z3n 0 4232 139917.114 139670.71542323051118149634940 6
CVC4 0 3517 151428.081 151178.56735172359115856785678 0
AProVE 0 2404 175808.845 169727.71724042404067916717 0
SMT-RAT 0 1333 195190.621 195031.3771333116317078627855 3

n Non-competing.