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

QF_NIA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 9031 3565990.911 3284622.51790316028300326502612 38
z3n 0 8661 4209068.947 4208914.64586615803285830203011 0
MathSAT5n 0 8189 4595124.761 4595104.92381895508268134923492 0
cvc5 0 8174 4356290.797 5121953.11581745681249335073507 0
cvc5 - fixedn 0 8143 4343734.101 5136735.44781435651249235383538 0
Yices2 0 7805 4826168.739 4826306.71878055113269238763875 0
AProVE 0 3996 7490983.286 9215732.79339963996076857419 0
SMT-RAT 0 2577 11164267.625 11165606.2582577228729091049068 12
2020-SMT-RATn 0 2568 11113579.401 11141524.2752568228528391139040 13

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 92233795805.1513162035.50992236190303324582420 38
z3n 0 86614209608.5174208784.01586615803285830203011 0
MathSAT5n 0 81894596009.8814594947.66381895508268134923492 0
cvc5 0 81745117319.155121766.25581745681249335073507 0
cvc5 - fixedn 0 81435131570.4265136531.07781435651249235383538 0
Yices2 0 78054826618.0994826178.68878055113269238763875 0
AProVE 0 39989229598.7139215415.01639983998076837417 0
SMT-RAT 0 257611165392.50511165255.4882576228629091059068 12
2020-SMT-RATn 0 256811140501.78111141154.5252568228528391139040 13

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2019-Par4n 0 61901203890.651731342.92461906190047250192420 38
z3n 0 58031451813.7231451305.57258035803085950193011 0
cvc5 0 56812005636.9182010126.24656815681098150193507 0
cvc5 - fixedn 0 56512019785.5032024780.945565156510101150193538 0
MathSAT5n 0 55081704489.6271703774.183550855080115450193492 0
Yices2 0 51131987386.621987044.035511351130154950193875 0
AProVE 0 39983485012.3523470915.682399839980266450197417 0
SMT-RAT 0 22865503988.3335503836.19228622860437650199068 12
2020-SMT-RATn 0 22855500494.6085500862.774228522850437750199040 13

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2019-Par4n 0 3033429391.37301159.15630330303321184372420 38
z3n 0 2858634491.884634175.2928580285838684373011 0
Yices2 0 2692710365.953710269.12326920269255284373875 0
MathSAT5n 0 2681761520.253761173.4826810268156384373492 0
cvc5 0 2493981682.233981640.00924930249375184373507 0
cvc5 - fixedn 0 2492981784.923981750.13224920249275284373538 0
SMT-RAT 0 2903531404.1723531419.2982900290295484379068 12
2020-SMT-RATn 0 2833510007.1733510291.7512830283296184379040 13
AProVE 0 03697345.8633697271.491000324484377417 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 8181159297.647105042.50681815397278435003462 38
Yices2 0 6825132140.927131930.87568254423240248564856 0
MathSAT5n 0 6319156446.657155965.32463194076224353625362 0
z3n 0 5974163396.976163018.92759743970200457075702 0
cvc5 0 5838163419.844162954.72858383746209258435843 0
cvc5 - fixedn 0 5837163363.229163034.79658373744209358445844 0
AProVE 0 3056218973.345211486.17330563056086258359 0
2020-SMT-RATn 0 1652248360.552248264.64316521405247100299994 13
SMT-RAT 0 1635248982.248248888.656163513912441004610021 12

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