Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding.

Published in: SMT (2020)

Keyphrases