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

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

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

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

Logics:

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 UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 9031 3565990.911 3284622.517903160283003265022612 38
z3n 0 8662 4210270.621 4210116.59866258032859302103012 0
MathSAT5n 0 8189 4597524.331 4597505.153818955082681349403494 0
cvc5 0 8175 4357530.002 5123192.635817556812494350803508 0
cvc5 - fixedn 0 8144 4344970.834 5137972.59814456512493353903539 0
Yices2 0 7805 4828568.419 4828706.758780551132692387803877 0
AProVE 0 3996 7490983.286 9215732.793399639960768527419 0
SMT-RAT 0 2579 11164558.249 11165896.94625792287292910409068 12
2020-SMT-RATn 0 2570 11113832.751 11141777.64325702285285911309040 13

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 92233795805.1513162035.509922361903033245822420 38
z3n 0 86624210810.4414209985.94866258032859302103012 0
MathSAT5n 0 81894598409.8814597347.663818955082681349403494 0
cvc5 0 81755118558.5755123005.685817556812494350803508 0
cvc5 - fixedn 0 81445132807.4695137768.16814456512493353903539 0
Yices2 0 78054829018.0994828578.688780551132692387803877 0
AProVE 0 39989229598.7139215415.016399839980768327417 0
SMT-RAT 0 257811165683.12911165546.17625782286292910509068 12
2020-SMT-RATn 0 257011140755.13111141407.89325702285285911309040 13

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 61901203890.651731342.92461906190047250212420 38
z3n 0 58031451813.7231451305.57258035803085950213012 0
cvc5 0 56812005636.9182010126.24656815681098150213508 0
cvc5 - fixedn 0 56512019785.5032024780.945565156510101150213539 0
MathSAT5n 0 55081704489.6271703774.183550855080115450213494 0
Yices2 0 51131987386.621987044.035511351130154950213877 0
AProVE 0 39983485012.3523470915.682399839980266450217417 0
SMT-RAT 0 22865503988.3335503836.19228622860437650219068 12
2020-SMT-RATn 0 22855500494.6085500862.774228522850437750219040 13

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 3033429391.37301159.15630330303321184392420 38
z3n 0 2859635693.808635377.21528590285938784373012 0
Yices2 0 2692712765.953712669.12326920269255484373877 0
MathSAT5n 0 2681763920.253763573.4826810268156584373494 0
cvc5 0 2494982921.657982879.43924940249475284373508 0
cvc5 - fixedn 0 2493983021.966982987.21424930249375384373539 0
SMT-RAT 0 2923531694.7963531709.9862920292295484379068 12
2020-SMT-RATn 0 2853510260.5233510545.1192850285296184379040 13
AProVE 0 03697345.8633697271.491000324484397417 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 8181159297.647105042.506818153972784350023462 38
Yices2 0 6825132188.927131978.875682544232402485804858 0
MathSAT5n 0 6319156494.657156013.324631940762243536405364 0
z3n 0 5975163422.9163044.852597539702005570805703 0
cvc5 0 5838163467.844163002.728583837462092584505845 0
cvc5 - fixedn 0 5837163411.229163082.796583737442093584605846 0
AProVE 0 3056218973.345211486.173305630560862528359 0
2020-SMT-RATn 0 1652248408.552248312.643165214052471003109996 13
SMT-RAT 0 1635249030.248248936.6561635139124410048010023 12

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.