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

QF_LinearIntArith (Single Query Track)

Competition results for the QF_LinearIntArith division in the Single Query Track.

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

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
OpenSMTOpenSMTZ3++ cvc5 Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 7117 462337.315 400831.8117117455425633130304 9
OpenSMT 0 6828 1096967.146 1096616.5356828433124975957589 0
Z3++ 0 6805 1016387.29 1019736.7426805450223036187589 10
cvc5 0 6793 1157778.615 1157546.3476793429225016370636 0
Yices2 0 6768 889765.982 889746.7836768430124676620662 0
MathSATn 0 6705 1154937.613 1154708.7526705425424517250725 0
z3-4.8.17n 0 6667 1169666.322 1169276.3686667444022277630737 5
smtinterpol 0 6431 1573517.317 1481591.9016431400324289990999 0
veriT 0 5004 2577129.266 2577133.761500434461558242602014 1

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 7194575760.685363616.6497194459825962360227 9
OpenSMT 0 68281097021.2061096597.1656828433124975957589 0
Z3++ 0 68051016459.751019712.7826805450223036187589 10
cvc5 0 67931157879.9251157520.0676793429225016370636 0
Yices2 0 6768889821.582889725.9636768430124676620662 0
MathSATn 0 67051155036.3331154680.6826705425424517250725 0
z3-4.8.17n 0 66671169760.1421169246.8286667444022277630737 5
smtinterpol 0 64441576295.6371477864.1446444400324419860986 0
veriT 0 50042577291.4762577060.781500434461558242602014 1

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 4598269194.796150140.952459845980862746227 9
Z3++ 0 4502341428.12342762.7894502450201812747589 10
z3-4.8.17n 0 4440409731.554409494.4814440444002442746737 5
OpenSMT 0 4331695202.704695006.3094331433103522747589 0
Yices2 0 4301535460.096535420.0644301430103832746662 0
cvc5 0 4292678110.675677912.5644292429203922746636 0
MathSATn 0 4254651270.707651025.4174254425404302746725 0
smtinterpol 0 40031013459.724984273.3114003400306812746986 0
veriT 0 34461211097.5731210865.74344634460123827462014 1

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 2596196165.889103075.697259602596584776227 9
cvc5 0 2501369369.25369207.5032501025011534776636 0
OpenSMT 0 2497291418.502291190.8562497024971514782589 0
Yices2 0 2467243961.487243905.8992467024671874776662 0
MathSATn 0 2451393365.626393255.2652451024512034776725 0
smtinterpol 0 2441452435.913383190.8332441024412134776986 0
Z3++ 0 2303570369.464571265.1792303023033454782589 10
z3-4.8.17n 0 2227649628.588649352.3472227022274274776737 5
veriT 0 15581255793.9031255795.04155801558109647762014 1

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 692425294.28616684.1616924443224925060497 9
Yices2 0 642828914.14728902.855642840472381100201002 0
z3-4.8.17n 0 556554578.40354343.705556538531712186501839 5
Z3++ 0 550355820.58555732.865550338301673192071909 10
MathSATn 0 539656638.34556427.38539635771819203402034 0
OpenSMT 0 516764811.70164664.87516732601907225672250 0
cvc5 0 497968314.08868112.142497933311648245102451 0
smtinterpol 0 480492001.06975540.844480431381666262602626 0
veriT 0 445568576.83468499.743445530871368297502644 1

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.