SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

QF_NonLinearIntArith (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +0000

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

Logics:

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Z3++-fixedn 0 9982 3091737.894 3091312.854998267813201224722023 0
Yices-ismt-fixedn 0 9759 3619046.413 3618887.45997596904285524702968 1
2019-Par4n 0 9348 3858525.23 3576949.234934862983050288122847 34
z3-4.8.17n 0 9247 4149050.887 4148646.925924763112936298402978 0
MathSATn 0 8322 5121725.169 5121609.734832255732749390903910 0
cvc5 0 8302 6487122.646 6542536.51830257862516392903924 5
Yices2 0 7862 5445586.23 5445943.186786251002762436904367 0
Z3++ 1 10158 3077399.006 3076590.4891015869553203207122013 0
Yices-ismt 26 9817 3493483.962 3493344.451981769662851241221940 1

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Z3++-fixedn 0 99823091874.4343091240.024998267813201224722023 0
Yices-ismt-fixedn 0 97593619713.0133618838.61997596904285524702998 1
2019-Par4n 0 95674083392.353444119.982956764883079266222628 34
z3-4.8.17n 0 92474149427.3174148527.045924763112936298402978 0
MathSATn 0 83215122487.5995121439.054832155722749391003910 0
cvc5 0 83036536641.8486541929.025830357872516392803923 5
Yices2 0 78625446154.845445786.346786251002762436904367 0
Z3++ 1 101583077521.3563076521.2691015869553203207122013 0
Yices-ismt 26 98173493752.7523493131.591981769662851241221980 1

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices-ismt-fixedn 0 6904868968.315868585.7016904690403394988998 1
Z3++-fixedn 0 6781936525.524936024.34367816781046249882023 0
2019-Par4n 0 64881607830.8751103768.17864886488075549882628 34
z3-4.8.17n 0 63111511226.2461510555.55963116311093249882978 0
cvc5 0 57873470314.5593475681.333578757870145649883923 5
MathSATn 0 55722344987.8452344263.769557255720167149883910 0
Yices2 0 51002723709.6552723411.298510051000214349884367 0
Z3++ 1 6955925715.127925099.50469556955028849882013 0
Yices-ismt 26 6966776779.311776293.41369666966027749881980 1

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Z3++ 0 3203428617.763428231.15832030320333086982013 0
Z3++-fixedn 0 3201431179.084431045.37932010320133286982023 0
2019-Par4n 0 3079724761.244596837.57430790307945486982628 34
z3-4.8.17n 0 2936893401.071893171.48529360293659886972978 0
Yices-ismt-fixedn 0 28551007521.6381007157.3592855028556788698998 1
Yices-ismt 0 2851973500.001973334.78828510285168286981980 1
Yices2 0 2762977645.186977575.04827620276277286974367 0
MathSATn 0 27491032699.7541032375.28527490274978586973910 0
cvc5 0 25161321527.2881321447.692251602516101886973923 5

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 8410167165.287114362.001841055942816381923785 34
Yices2 0 6817144922.142144744.512681743492468541405414 0
Yices-ismt 0 6817145027.615144746.157681743492468541225411 1
Yices-ismt-fixedn 0 6815144951.618144754.431681543472468541425413 1
Z3++-fixedn 0 6569157870.651157583.735656938402729566025660 0
Z3++ 0 6569157966.231157612.653656938432726566025660 0
z3-4.8.17n 0 6518164496.384163983.261651844292089571305713 0
MathSATn 0 6340169236.477168881.149634040492291589105891 0
cvc5 0 4252210521.191210297.849425221942058797907974 5

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.