Byron Cook, Andres Nötzli. Reasoning About Hilbert's Choice Operator in SMT. In Daniel Dietsch, Andrey Rybalchenko, Martin Schäf, Thomas Wies, editors, On the Pursuit of Insight and Elegance - Essays Dedicated to Andreas Podelski on the Occasion of His 65th Birthday. Volume 14765 of Lecture Notes in Computer Science, pages 107-120, Springer, 2026. [doi]
Abstract is missing.