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

Equality+NonLinearArith (Single Query Track)

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

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

Benchmarks: 9493
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 6135 3919824.849 4011759.13361356945441335803227 0
2020-CVC4n 0 6055 3723112.023 3833254.760556925363343803064 0
z3-4.8.17n 0 5327 3477095.862 3482229.09953276274700416602486 15
Vampire 0 4804 6146543.518 5711815.808480404804468904635 2
UltimateEliminator+MathSAT 0 568 649256.294 630232.17956839717189250483 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 61364009250.8464011556.09361366945442335703226 0
2020-CVC4n 0 60553827621.7593833071.7160556925363343803064 0
z3-4.8.17n 0 53273478506.4923482130.41953276274700416602486 15
Vampire 0 51247107011.6385492638.325512405124436904310 2
UltimateEliminator+MathSAT 0 568649288.534630177.03956839717189250480 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 69459103.69659205.11869469404687533226 0
2020-CVC4n 0 69247700.6448095.22469269204887533064 0
z3-4.8.17n 0 627102098.653102088.04627627011387532486 15
UltimateEliminator+MathSAT 0 397328504.159327522.33439739703438753480 0
Vampire 0 0992404.87887899.4300074087534310 2

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 5442586128.77588333.52854420544241836333226 0
2020-CVC4n 0 5363688713.053693696.32953630536349736333064 0
Vampire 0 51242224514.1681134378.35751240512473636334310 2
z3-4.8.17n 0 4700874481.81874462.811470004700116036332486 15
UltimateEliminator+MathSAT 0 171194602.027181883.204171017156893633480 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 539699417.41499378.22953966254771409703973 0
2020-CVC4n 0 536895000.55794980.11753686014767412503827 0
z3-4.8.17n 0 516299359.60599251.151626054557433103878 15
Vampire 0 3429160477.643149260.373342903429606406034 2
UltimateEliminator+MathSAT 0 53458824.46340920.70253436417089590576 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.