SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2023

Rules
Benchmarks
Specs
Model Validation Track
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results

Equality+NonLinearArith (Single Query Track)

Competition results for the Equality+NonLinearArith division in the Single Query Track.

Page generated on 2023-07-06 16:04:54 +0000

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

Logics:

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 UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 6256 127760.327 131004.52762567455511329503137 0
2022-cvc5n 0 6219 142048.316 144583.562621974154783276563166 0
Vampire 0 4889 490858.535 124040.797488904889466204606 0
iProver 0 3620 230324.704 60301.76362003620593105931 0
iProver Fixedn 0 3591 209556.485 54960.03359103591596005960 0
UltimateEliminator+MathSAT 0 608 11637.288 10430.45460842618260302913531 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 6256127760.327131004.52762567455511329503137 0
2022-cvc5n 0 6219142048.316144583.562621974154783276563166 0
Vampire 0 52391252881.755315641.715523905239431204254 0
iProver 0 3856662175.104170035.179385603856569505695 0
iProver Fixedn 0 3828610036.105156538.001382803828572305723 0
UltimateEliminator+MathSAT 0 60811637.28810430.45460842618260302913531 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 74523882.18123928.2627457450787993137 0
2022-cvc5n 0 74129139.89929266.6397417410888023166 0
UltimateEliminator+MathSAT 0 42610386.5669536.19342642603268799531 0
Vampire 0 00.00.000075287994254 0
iProver 0 00.00.000075287995695 0
iProver Fixedn 0 00.00.000075287995723 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 5511103878.146107076.26555110551133237083137 0
2022-cvc5n 0 5478112908.417115316.92454780547836437093166 0
Vampire 0 52391252881.755315641.71552390523960437084254 0
iProver 0 3856662175.104170035.179385603856198737085695 0
iProver Fixedn 0 3828610036.105156538.001382803828201537085723 0
UltimateEliminator+MathSAT 0 1821250.723894.261182018230636306531 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 55973046.0153006.58855976914906395403804 0
2022-cvc5n 0 55243859.533801.6552467648483971563868 0
Vampire 0 350824421.96507.436350803508604305987 0
iProver Fixedn 0 315925007.1637676.112315903159639206392 0
iProver 0 315625530.0517772.705315603156639506395 0
UltimateEliminator+MathSAT 0 5694118.0923003.9856938918060692913639 0

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.