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

Competition results for the QF_DT logic in the Single Query Track.

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
cvc5cvc5cvc5 cvc5 smtinterpol

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 106 173669.417 173688.97910641659595 0
2021-z3n 0 104 172881.246 172899.60810440649797 0
cvc5 0 85 188505.366 188535.286852164116116 0
smtinterpol 0 7 235702.976 235032.689707194194 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 106173680.147173686.11910641659595 0
2021-z3n 0 104172890.636172895.77810440649797 0
cvc5 0 85188523.986188530.246852164116116 0
smtinterpol 0 14236800.506233591.814014187187 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
z3-4.8.17n 0 4196276.62296278.905414105910195 0
2021-z3n 0 4095702.17195703.967404006010197 0
cvc5 0 21104497.477104498.9782121079101116 0
smtinterpol 0 0120000.0120000.0000100101187 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
z3-4.8.17n 0 6577403.52577407.214650653610095 0
2021-z3n 0 6477188.46577191.811640643710097 0
cvc5 0 6484026.50984031.2686406437100116 0
smtinterpol 0 14116800.506113591.81401487100187 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
z3-4.8.17n 0 44784.0324784.028413197197 0
2021-z3n 0 44784.1714784.174413197197 0
smtinterpol 0 14818.6884817.69101200200 0
cvc5 0 04824.04824.0000201201 0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.