Fix bugs - refinement backtracking, state set reset, trace formula encoding branches