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

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3++ 0 1049 248709.844 248685.4071049656393155155 0
z3-4.8.17n 0 1000 282237.079 282212.1941000638362204183 0
2019-Par4n 0 980 322061.046 282368.236980619361224224 0
Yices2 0 968 314738.395 314707.26968625343236236 0
cvc5 0 904 441256.929 441148.777904527377300300 0
OpenSMT 0 884 444917.541 444861.438884561323320320 0
veriT 0 781 562839.517 562849.668781461320423423 0
MathSATn 0 742 599214.086 599224.487742421321462462 0
smtinterpol 0 693 689810.345 675508.638693422271511511 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3++ 0 1049248725.234248679.7371049656393155155 0
2019-Par4n 0 1039417767.476253638.1961039649390165165 0
z3-4.8.17n 0 1000282260.559282205.5141000638362204183 0
Yices2 0 968314757.895314699.5968625343236236 0
cvc5 0 904441319.109441134.397904527377300300 0
OpenSMT 0 884444942.761444851.008884561323320320 0
veriT 0 781562876.237562836.248781461320423423 0
MathSATn 0 742599280.276599206.987742421321462462 0
smtinterpol 0 701690908.345673145.867701422279503503 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Z3++ 0 656107725.386107679.737656656054494155 0
2019-Par4n 0 649181658.764100679.547649649061494165 0
z3-4.8.17n 0 638120621.346120622.643638638072494183 0
Yices2 0 625121762.697121753.644625625085494236 0
OpenSMT 0 561226566.6226527.5835615610149494320 0
cvc5 0 527274893.28274772.2995275270183494300 0
veriT 0 461346010.251345972.6224614610249494423 0
smtinterpol 0 422397409.442391532.2834224220288494503 0
MathSATn 0 421379024.804378955.2384214210289494462 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedN/ATimeout Memout
Z3++ 0 39365399.84865400.0393039338773155 0
2019-Par4n 0 390160508.71277358.649390039041773165 0
cvc5 0 37790825.82990762.098377037754773300 0
z3-4.8.17n 0 36286039.21385982.87362036269773183 0
Yices2 0 343117395.198117345.856343034388773236 0
OpenSMT 0 323142776.161142723.4253230323108773320 0
MathSATn 0 321144655.472144651.7493210321110773462 0
veriT 0 320141265.985141263.6263200320111773423 0
smtinterpol 0 279217898.903206013.5832790279152773503 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 86413108.5579509.514864559305340340 0
Yices2 0 8499737.7259725.129849551298355355 0
Z3++ 0 79212052.36312035.852792505287412412 0
z3-4.8.17n 0 77911761.17211727.728779504275425404 0
OpenSMT 0 60516739.43516702.467605333272599599 0
MathSATn 0 56717086.09617045.308567291276637637 0
cvc5 0 55718275.39718182.336557298259647647 0
veriT 0 54117447.1517438.712541261280663663 0
smtinterpol 0 41223872.15321112.615412222190792792 0

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