<p>Process discovery aims to generate models that capture behaviors recorded in event logs from information systems. While many approaches exist, few ensure key properties such as soundness and free-choice. Existing methods that provide these guarantees often rely on block-structured representations, which limit expressiveness. We propose Synthesis Miner, a discovery approach that constructs sound and free-choice workflow nets while supporting non-block structures. Drawing from free-choice net theory, Synthesis Miner incrementally builds or adjusts process models using predefined synthesis patterns and log-guided heuristics to narrow the search space. This ensures correctness by design while improving scalability. We evaluate the approach in two complementary experiments. The first compares the performance of our enhanced Synthesis Miner to its original version, demonstrating substantial reductions in computation time with consistent model quality. The second experiment compares the quality of Synthesis Miner’s models against those produced by state-of-the-art discovery algorithms. The results highlight that Synthesis Miner can generate models with competitive, and in some cases superior, quality while ensuring key formal guarantees.</p>