Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
No abstract available.
Related papers
- Automating Bitvector and Finite Field Equivalence Proofs in Lean CAV 2026
- Bit-Precise Interpolation in Bitwuzla TACAS 2026
- High-Level Abstractions for Simplifying Extended String Constraints in SMT CAV 2019
- Clausal Proofs for Pseudo-Boolean Reasoning TACAS 2022
- Programming up to Congruence POPL 2015
- Integer Reasoning Modulo Different Constants in SMT CAV 2025
- SMTScope: Automated and Efficient Analysis of SMT Traces TACAS 2026
- Congruence Closure with Free Variables TACAS 2017