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

LIA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 300 10.819 10.34430013716300 0
cvc5 0 300 78.318 78.21330013716300 0
2021-z3n 0 292 9608.617 9610.01229213715588 0
UltimateEliminator+MathSAT 0 228 95714.771 93819.912228721567272 0
YicesQS 0 182 141132.674 141155.15218210181118117 0
Vampire 0 157 172584.806 171862.5381573154143143 0
smtinterpol 0 97 130473.89 129603.09397889203100 0
veriT 0 75 24505.539 24482.2837507522519 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 30010.81910.34430013716300 0
cvc5 0 30078.31878.21330013716300 0
2021-z3n 0 2929609.6179609.66229213715588 0
UltimateEliminator+MathSAT 0 23095788.57193730.482230741567070 0
YicesQS 0 182141150.224141150.25218210181118117 0
Vampire 0 157197786.226171827.1881573154143143 0
smtinterpol 0 97130473.89129603.09397889203100 0
veriT 0 7524507.65924481.6837507522519 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
2021-z3n 0 1375.4575.477137137001638 0
z3-4.8.17n 0 1376.0895.867137137001630 0
cvc5 0 13760.41460.383137137001630 0
YicesQS 0 10142740.87142740.899101101036163117 0
UltimateEliminator+MathSAT 0 7484098.81182827.376747406316370 0
smtinterpol 0 8102026.547101460.228880129163100 0
Vampire 0 3186004.955160765.929330134163143 0
veriT 0 01196.0671186.71600013716319 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
z3-4.8.17n 0 1634.7314.477163016301370 0
cvc5 0 16317.90417.83163016301370 0
UltimateEliminator+MathSAT 0 15611689.7610903.1061560156713770 0
2021-z3n 0 1559604.169604.185155015581378 0
Vampire 0 15411781.27211061.25915401549137143 0
smtinterpol 0 8928447.34428142.8648908974137100 0
YicesQS 0 8198409.35398409.3538108182137117 0
veriT 0 7523311.59223294.968750758813719 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 30010.81910.34430013716300 0
cvc5 0 30078.31878.21330013716300 0
2021-z3n 0 292201.617201.66229213715588 0
UltimateEliminator+MathSAT 0 2064250.0793229.435206571499494 0
YicesQS 0 1743108.9243108.9381749381126125 0
Vampire 0 1533726.8063592.2311533150147147 0
smtinterpol 0 973725.5343440.23997889203134 0
veriT 0 75804.494778.2967507522524 0

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