VeriEQL is a novel SMT-based approach for bounded equivalence verification of complex SQL queries with integrity constraints. It addresses the challenge of verifying equivalence between SQL queries that involve advanced features like sorting, case statements, and rich integrity constraints. The approach models query semantics using symbolic tuples and the theory of integers with uninterpreted functions, enabling efficient reasoning about complex SQL features and integrity constraints. VeriEQL can prove or disprove bounded equivalence of queries, generate counterexamples, and support a wide range of SQL features not supported by previous techniques. The system has been evaluated on over 24,455 benchmarks, outperforming state-of-the-art techniques by more than one order of magnitude in terms of the number of benchmarks that can be verified. VeriEQL can also generate counterexamples that help identify bugs in real-world systems like MySQL and Apache Calcite. The paper presents a formal problem statement, a detailed description of the SQL query syntax and semantics, and an algorithm for bounded equivalence verification modulo integrity constraints. The approach is implemented in VeriEQL, which has been shown to be effective in verifying the equivalence of complex SQL queries with rich integrity constraints.VeriEQL is a novel SMT-based approach for bounded equivalence verification of complex SQL queries with integrity constraints. It addresses the challenge of verifying equivalence between SQL queries that involve advanced features like sorting, case statements, and rich integrity constraints. The approach models query semantics using symbolic tuples and the theory of integers with uninterpreted functions, enabling efficient reasoning about complex SQL features and integrity constraints. VeriEQL can prove or disprove bounded equivalence of queries, generate counterexamples, and support a wide range of SQL features not supported by previous techniques. The system has been evaluated on over 24,455 benchmarks, outperforming state-of-the-art techniques by more than one order of magnitude in terms of the number of benchmarks that can be verified. VeriEQL can also generate counterexamples that help identify bugs in real-world systems like MySQL and Apache Calcite. The paper presents a formal problem statement, a detailed description of the SQL query syntax and semantics, and an algorithm for bounded equivalence verification modulo integrity constraints. The approach is implemented in VeriEQL, which has been shown to be effective in verifying the equivalence of complex SQL queries with rich integrity constraints.