High-level system diagram of Herbie. It highlights Herbie's core architecture, external libraries, and user interactions. Basic flow: Herbie passes user input (expression, precondition, etc.) to the mainloop (scheduler) which alternates between generate and test phases multiple times, maintaining and improving a set of accurate expressions at each iteration. Once the generate-and-test phase is complete, Herbie extracts either one or many output expressions using an algorithm called regime inference. Regime inference chooses the "best" (usually most accurate) generated candidate expression or combines multple candidates, each "best" on a smaller part of the input range, with a branch condition.