Synthesizing Loop-Free Programs with Rust and Z3 (2020)

This post makes extensive use of math symbols, and uses MathJax.js to render them, therefore I recommend enabling JavaScript.