Strange State Machine Compilation - Compiler Bug?

True, the current state register necessarily feeds the control logic of the selector that likely implements the case. I'm arguing that the feedback in the data lines probably makes a difference. Even if the compiler collapses the select + muxes, you probably won't end up with "identical" logic - it all depends on the smarts behind the algorithm. What matters here isn't functional equivalence but structural equivalence. In many tools, you can get a totally different result simply by switching a couple gates around in a functionally equivalent way. It's just the undeniable nature of heuristic algorithms. Maybe if the compiler collapsed using BDDs...