Optimistic ground now uses path condition, IntInduction pushes case to path condition instead of formula