> For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt.
In general, this can happen, but not with this particular choice of example: If ZFC+CH proves that some machine halts, then so does ZFC (and, in fact, so do ZF and IZF). This is because a given Turing machine halting is a mere number-theoretic statement, such statements "are absolute between V and L" and CH holds in L.
In general, this can happen, but not with this particular choice of example: If ZFC+CH proves that some machine halts, then so does ZFC (and, in fact, so do ZF and IZF). This is because a given Turing machine halting is a mere number-theoretic statement, such statements "are absolute between V and L" and CH holds in L.