Reproducibility Report for ACM SIGMOD 2024 Paper: 'Proving Query Equivalence Using Linear Integer Arithmetic'

The reproducibility evaluation successfully replicated key functionalities of SQLSolver. During the review process, we found a discrepancy in the verification speed regarding SQLSolver, i.e., SQLSolver's reproduced verification latency is much higher than the result in the paper. Because after the paper was published, the authors of the paper further added some optimizations to SQLSolver, which aim at enhancing the verification capabilities and can help prove 4 more cases. However, these optimizations affect the speed of verification. After the authors of the paper provided the original version, we can successfully reproduce the main results.