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+MachineArith (Single Query Track)

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

Page generated on 2021-07-18 17:29:05 +0000

Benchmarks: 2822
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 1165 998180.158 1854513.6941165242923165701422 0
cvc5 - fixedn 0 1153 962542.62 1859009.1541153235918166901424 0
2020-CVC4n 0 985 601599.311 617306.4369852587278081029432 0
z3n 0 310 825181.219 827144.5743101072037631749646 10
2020-z3n 0 147 164325.721 164347.25314760871652510131 0
2018-Z3n 0 106 45221.546 45229.165106347237267936 0
UltimateEliminator+MathSAT 0 31 1086812.502 1082236.83831201114141377861 6

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 11651849169.3841854430.5541165242923165701422 0
cvc5 - fixedn 0 11531853416.4041858923.3241153235918166901424 0
2020-CVC4n 0 985613497.101617284.7569852587278081029432 0
z3n 0 310826577.999827117.5743101072037631749646 10
2020-z3n 0 147164341.561164342.11314760871652510131 0
2018-Z3n 0 10645226.96645227.585106347237267936 0
UltimateEliminator+MathSAT 0 311086886.2921082219.40831201114141377859 6

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2020-CVC4n 0 25873263.6276389.4252582580842480432 0
cvc5 0 242186196.746188508.879242242017424061422 0
cvc5 - fixedn 0 235193349.477195478.458235235018124061424 0
z3n 0 10713159.48613159.9611071070112704646 10
2020-z3n 0 604789.4274788.8046060042758131 0
2018-Z3n 0 342971.382971.558343402278636 0
UltimateEliminator+MathSAT 0 2067144.91566091.64202001512651859 6

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 0 923135089.184136275.92692309239118081422 0
cvc5 - fixedn 0 918139953.789141077.65391809189618081424 0
2020-CVC4n 0 72737132.1537615.6867270727722023432 0
z3n 0 203118696.143118661.5052030203952524646 10
2020-z3n 0 8725581.37125581.4987087222713131 0
2018-Z3n 0 7214723.81514723.8387207212273836 0
UltimateEliminator+MathSAT 0 11210256.018209068.205110113192492859 6

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
cvc5 - fixedn 0 91545680.42545678.93291587828190701856 0
cvc5 0 91545688.71945683.93691587828190701856 0
2020-CVC4n 0 71718857.66918858.6067176665110761029765 0
z3n 0 24219953.14819952.279242911518311749784 10
2020-z3n 0 1344191.8244190.81913455791782510163 0
2018-Z3n 0 941257.6071257.62294266849267949 0
UltimateEliminator+MathSAT 0 2726532.02925376.1812718914181377970 6

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.