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

Equality+LinearArith (Unsat Core Track)

Competition results for the Equality+LinearArith division in the Unsat Core Track.

Page generated on 2021-07-18 17:31:25 +0000

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

Logics:

Winners

Sequential PerformanceParallel Performance
cvc5-uccvc5-uc

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreAbstainedTimeout Memout
cvc5-uc 0 1407812 389756.63 389701.433304 0
2020-CVC4-ucn 0 1407110 407622.165 407692.789318 0
2020-z3n 0 1083727 400108.203 400350.49242 14
z3n 0 1082260 401077.391 404766.259243 4
SMTInterpol 0 778848 2439773.633 2422309.3711948 0
SMTInterpol-remus 0 676156 4754314.111 4513260.9722387 0
UltimateEliminator+MathSAT 3 13528 124169.242 89179.35525 4
Vampire 19 1092544 1782337.947 1218637.028832 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreAbstainedTimeout Memout
cvc5-uc 0 1407812389810.94389688.113304 0
2020-CVC4-ucn 0 1407110407702.695407678.379318 0
2020-z3n 0 1083727400434.713400339.28242 14
z3n 0 1082260404263.211404755.489243 4
SMTInterpol 0 7802402480065.7232403021.8051900 0
SMTInterpol-remus 0 7737104859431.4614461611.8851908 0
UltimateEliminator+MathSAT 3 13528124169.24289179.35525 4
Vampire 19 10970862016231.3471019077.325541 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.